Examples.Classical.Groups.AbelianGroup

Worked example: (ℤ, +, 0, -) as an abelian group

This is the Examples.Classical.Groups.AbelianGroup module of the Agda Universal Algebra Library.

The integers under addition are the canonical abelian group — the same carrier and operations as the CyclicGroup example, now additionally witnessing commutativity via stdlib's +-comm.

{-# OPTIONS --without-K --exact-split --safe #-}

module Examples.Classical.Groups.AbelianGroup where

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Integer             using ( ℤ ; _+_ ; 0ℤ ; -_ )
open import Data.Integer.Properties  using ( +-assoc ; +-identityˡ ; +-identityʳ
                                           ; +-inverseˡ ; +-inverseʳ ; +-comm )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Bundles.AbelianGroup           using ( ⟨_⟩ᵃᵍ ; ⟪_⟫ᵃᵍ )
open import Classical.Small.Structures.AbelianGroup  using ( AbelianGroup ; eqsToAbelianGroup )

import Classical.Structures.Group.AbelianGroup as Polymorphic

The abelian group (ℤ, +, 0, -)

ℤ-abelianGroup : AbelianGroup
ℤ-abelianGroup =
  eqsToAbelianGroup ℤ _+_ 0ℤ -_ +-assoc +-identityˡ +-identityʳ +-inverseˡ +-inverseʳ +-comm

open Polymorphic.AbelianGroup-Op ℤ-abelianGroup using ( _∙_ ; ε ; _⁻¹ )

Acceptance checks

∙-is-+-ag, ε-is-0-ag, and ⁻¹-is-neg-ag record that the accessors interpret to _+_, 0ℤ, and negation on the nose, each discharged by refl.

∙-is-+-ag : ∀ (a b : ℤ) → a ∙ b ≡ a + b
∙-is-+-ag a b = refl

ε-is-0-ag : ε ≡ 0ℤ
ε-is-0-ag = refl

⁻¹-is-neg-ag : ∀ (a : ℤ) → a ⁻¹ ≡ - a
⁻¹-is-neg-ag a = refl

The bundle round-trips pointwise on the operation, the identity, and the inverse.

open Polymorphic.AbelianGroup-Op ⟪ ⟨ ℤ-abelianGroup ⟩ᵃᵍ ⟫ᵃᵍ using ()
  renaming ( _∙_ to _·_ ; ε to ε· ; _⁻¹ to _⁻¹· )

roundtrip-∙-ag : ∀ (a b : ℤ) → a · b ≡ a + b
roundtrip-∙-ag a b = refl

roundtrip-ε-ag : ε· ≡ 0ℤ
roundtrip-ε-ag = refl

roundtrip-⁻¹-ag : ∀ (a : ℤ) → a ⁻¹· ≡ - a
roundtrip-⁻¹-ag a = refl