open import Algebra.Group.Cat.Base
open import Algebra.Group

open import Cat.Displayed.Univalence.Thin
open import Cat.Displayed.Total
open import Cat.Prelude hiding (_*_ ; _+_)

open import Data.Int.Properties
open import Data.Int.Base

import Cat.Reasoning

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.

private variable
β : Level
G : Type β

Group-on-is-abelian : Group-on G β Type _
Group-on-is-abelian G = β x y β Group-on._β_ G x y β‘ Group-on._β_ G y x

Group-on-is-abelian-is-prop : (g : Group-on G) β is-prop (Group-on-is-abelian g)
Group-on-is-abelian-is-prop g = Ξ -is-hlevelΒ² 1 Ξ» _ _ β g .Group-on.has-is-set _ _


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

private unquoteDecl eqv = declare-record-iso eqv (quote is-abelian-group)
instance
H-Level-is-abelian-group
: β {n} {* : G β G β G} β H-Level (is-abelian-group *) (suc n)
H-Level-is-abelian-group = prop-instance $Isoβis-hlevel 1 eqv$
Ξ£-is-hlevel 1 (hlevel 1) Ξ» x β Ξ -is-hlevelΒ²' 1 Ξ» _ _ β
is-group.has-is-set x _ _

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-on : Group-on T
AbelianβGroup-on .Group-on._β_ = _*_
AbelianβGroup-on .Group-on.has-is-group = has-is-group

AbelianβGroup-on-abelian : Group-on-is-abelian AbelianβGroup-on
AbelianβGroup-on-abelian _ _ = commutes

infixr 20 _*_

open Abelian-group-on using (AbelianβGroup-on; AbelianβGroup-on-abelian) 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 β)

Abelian-group : (β : Level) β Type (lsuc β)
Abelian-group _ = Ab.Ob

AbelianβGroup : β {β} β Abelian-group β β Group β
AbelianβGroup G = G .fst , AbelianβGroup-on (G .snd)

record make-abelian-group (T : Type β) : Type β where
no-eta-equality
field
ab-is-set : is-set T
mul   : T β T β T
inv   : T β T
1g    : T
idl   : β x β mul 1g x β‘ x
assoc : β x y z β mul x (mul y z) β‘ mul (mul x y) z
invl  : β x β mul (inv x) x β‘ 1g
comm  : β x y β mul x y β‘ mul y x

make-abelian-groupβmake-group : make-group T
make-abelian-groupβmake-group = mg where
mg : make-group T
mg .make-group.group-is-set = ab-is-set
mg .make-group.unit   = 1g
mg .make-group.mul    = mul
mg .make-group.inv    = inv
mg .make-group.assoc  = assoc
mg .make-group.invl   = invl
mg .make-group.idl    = idl

to-group-on-ab : Group-on T
to-group-on-ab = to-group-on make-abelian-groupβmake-group

to-abelian-group-on : Abelian-group-on T
to-abelian-group-on .Abelian-group-on._*_ = mul
to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group =
Group-on.has-is-group to-group-on-ab
to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
comm _ _

to-ab : Abelian-group β
β£ to-ab .fst β£ = T
to-ab .fst .is-tr = ab-is-set
to-ab .snd = to-abelian-group-on

is-commutative-group : β {β} β Group β β Type β
is-commutative-group G = Group-on-is-abelian (G .snd)

from-commutative-group
: β {β} (G : Group β)
β is-commutative-group G
β Abelian-group β
from-commutative-group G comm .fst = G .fst
from-commutative-group G comm .snd .Abelian-group-on._*_ =
Group-on._β_ (G .snd)
from-commutative-group G comm .snd .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group =
Group-on.has-is-group (G .snd)
from-commutative-group G comm .snd .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
comm _ _

open make-abelian-group using (make-abelian-groupβmake-group ; to-group-on-ab ; to-abelian-group-on ; to-ab) public

open Functor

AbβͺGrp : β {β} β Functor (Ab β) (Groups β)
AbβͺGrp .Fβ = AbelianβGroup
AbβͺGrp .Fβ f .hom = f .hom
AbβͺGrp .Fβ f .preserves = f .preserves
AbβͺGrp .F-id = trivial!
AbβͺGrp .F-β f g = trivial!

AbβͺSets : β {β} β Functor (Ab β) (Sets β)
AbβͺSets = GrpβͺSets Fβ AbβͺGrp


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