Examples.Classical.Groups.CyclicGroup

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

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

The integers under addition form the canonical group — indeed the infinite cyclic group; built directly from stdlib's +-assoc, +-identityˡ, +-identityʳ, +-inverseˡ, +-inverseʳ.

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

module Examples.Classical.Groups.CyclicGroup where

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

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

import Classical.Structures.Group as Polymorphic

The group (ℤ, +, 0, -)

ℤ-group : Group
ℤ-group = eqsToGroup ℤ _+_ 0ℤ -_ +-assoc +-identityˡ +-identityʳ +-inverseˡ +-inverseʳ

open Polymorphic.Group-Op ℤ-group using ( _∙_ ; ε ; _⁻¹ )

Acceptance checks

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

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

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

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

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

open Polymorphic.Group-Op ⟪ ⟨ ℤ-group ⟩ᵍᵖ ⟫ᵍᵖ using () renaming ( _∙_ to _·_ ; ε to ε· ; _⁻¹ to _⁻¹· )

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

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

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