module Algebra.Group.Ab where

Abelian groups🔗

A very important class of groups (which includes most familiar examples of groups: the integers, all finite cyclic groups, etc) are those with a commutative group operation, that is, those for which Accordingly, these have a name reflecting their importance and ubiquity: They are called commutative groups. Just kidding! They’re named abelian groups, named after a person, because nothing can have self-explicative names in mathematics. It’s the law.

This module does the usual algebraic structure dance to set up the category of Abelian groups.

record is-abelian-group (_*_ : G → G → G) : Type (level-of G) where
  no-eta-equality
  field
    has-is-group : is-group _*_
    commutes     : ∀ {x y} → x * y ≡ y * x
  open is-group has-is-group renaming (unit to 1g) public
record Abelian-group-on (T : Type ℓ) : Type ℓ where
  no-eta-equality
  field
    _*_       : T → T → T
    has-is-ab : is-abelian-group _*_
  open is-abelian-group has-is-ab renaming (inverse to infixl 30 _⁻¹) public
Abelian-group-structure : ∀ ℓ → Thin-structure ℓ Abelian-group-on
∣ Abelian-group-structure ℓ .is-hom f G₁ G₂ ∣ =
  is-group-hom (Abelian→Group-on G₁) (Abelian→Group-on G₂) f
Abelian-group-structure ℓ .is-hom f G₁ G₂ .is-tr = hlevel 1
Abelian-group-structure ℓ .id-is-hom .is-group-hom.pres-⋆ x y = refl
Abelian-group-structure ℓ .∘-is-hom f g α β .is-group-hom.pres-⋆ x y =
  ap f (β .is-group-hom.pres-⋆ x y) ∙ α .is-group-hom.pres-⋆ (g x) (g y)
Abelian-group-structure ℓ .id-hom-unique {s = s} {t} α _ = p where
  open Abelian-group-on

  p : s ≡ t
  p i ._*_ x y = α .is-group-hom.pres-⋆ x y i
  p i .has-is-ab = is-prop→pathp
    (λ i → hlevel {T = is-abelian-group (λ x y → p i ._*_ x y)} 1)
    (s .has-is-ab) (t .has-is-ab) i

Ab : ∀ ℓ → Precategory (lsuc ℓ) ℓ
Ab ℓ = Structured-objects (Abelian-group-structure ℓ)

module Ab {ℓ} = Cat.Reasoning (Ab ℓ)

The fundamental example of abelian group is the integers, under addition. A type-theoretic interjection is necessary: the integers live on the zeroth universe, so to have an group of integers, we must lift it.

ℤ-ab : ∀ {ℓ} → Abelian-group ℓ
ℤ-ab = to-ab mk-ℤ where
  open make-abelian-group
  mk-ℤ : make-abelian-group (Lift _ Int)
  mk-ℤ .ab-is-set = hlevel 2
  mk-ℤ .mul (lift x) (lift y) = lift (x +ℤ y)
  mk-ℤ .inv (lift x) = lift (negℤ x)
  mk-ℤ .1g = lift 0
  mk-ℤ .idl (lift x) = ap lift (+ℤ-zerol x)
  mk-ℤ .assoc (lift x) (lift y) (lift z) = ap lift (+ℤ-assoc x y z)
  mk-ℤ .invl (lift x) = ap lift (+ℤ-invl x)
  mk-ℤ .comm (lift x) (lift y) = ap lift (+ℤ-commutative x y)

ℤ : ∀ {ℓ} → Group ℓ
ℤ = Abelian→Group ℤ-ab