{-# OPTIONS -vtactic.hlevel:10 #-}
open import 1Lab.Prelude

open import Algebra.Magma.Unital hiding (idl ; idr)
open import Algebra.Semigroup
open import Algebra.Monoid hiding (idl ; idr)
open import Algebra.Magma

open import Cat.Instances.Delooping

import Cat.Reasoning

module Algebra.Group where


Groupsπ

A group is a monoid that has inverses for every element. The inverse for an element is necessarily, unique; Thus, to say that β is a groupβ is a statement about having a certain property (namely, being a group), not structure on

Furthermore, since group homomorphisms automatically preserve this structure, we are justified in calling this property rather than property-like structure.

In particular, for a binary operator to be a group operator, it has to be a monoid, meaning it must have a unit.

record is-group {β} {A : Type β} (_*_ : A β A β A) : Type β where
no-eta-equality
field
unit : A


There is also a map which assigns to each element its inverse and this inverse must multiply with to give the unit, both on the left and on the right:

    inverse : A β A

has-is-monoid : is-monoid unit _*_
inversel : {x : A} β inverse x * x β‘ unit
inverser : {x : A} β x * inverse x β‘ unit

open is-monoid has-is-monoid public

  _β_ : A β A β A
x β y = x * inverse y

abstract
inv-unit : inverse unit β‘ unit
inv-unit = monoid-inverse-unique
has-is-monoid unit _ _ inversel (has-is-monoid .is-monoid.idl)

inv-inv : β {x} β inverse (inverse x) β‘ x
inv-inv = monoid-inverse-unique
has-is-monoid _ _ _ inversel inversel

inv-comm : β {x y} β inverse (x * y) β‘ inverse y β x
inv-comm {x = x} {y} =
monoid-inverse-unique has-is-monoid _ _ _ inversel p
where
p : (x * y) * (inverse y β x) β‘ unit
p = associative has-is-monoid
Β·Β· apβ _*_
(  sym (associative has-is-monoid)
Β·Β· apβ _*_ refl inverser
Β·Β· has-is-monoid .is-monoid.idr)
refl
Β·Β· inverser

zero-diff : β {x y} β x β y β‘ unit β x β‘ y
zero-diff {x = x} {y = y} p =
monoid-inverse-unique has-is-monoid _ _ _ p inversel

underlying-monoid : Monoid β
underlying-monoid = A , record
{ identity = unit ; _β_ = _*_ ; has-is-monoid = has-is-monoid }

open Cat.Reasoning (B (underlying-monoid .snd))
hiding (id ; assoc ; idl ; idr ; invr ; invl ; to ; from ; inverses ; _β_ ; module HLevel-instance)
public


Note that any element of determines two bijections on the underlying set of by multiplication with on the left and on the right. The inverse of this bijection is given by multiplication with and the proof that these are in fact inverse functions are given by the group laws:

  β-equivl : β x β is-equiv (x *_)
β-equivl x = is-isoβis-equiv (iso (inverse x *_)
(Ξ» _ β cancell inverser) Ξ» _ β cancell inversel)

β-equivr : β y β is-equiv (_* y)
β-equivr y = is-isoβis-equiv (iso (_* inverse y)
(Ξ» _ β cancelr inversel) Ξ» _ β cancelr inverser)


is-group is propositionalπ

Showing that is-group takes values in propositions is straightforward, but, fortunately, very easy to automate: Our automation takes care of all the propositional components, and weβve already established that units and inverses (thus inverse-assigning maps) are unique in a monoid.

private unquoteDecl eqv = declare-record-iso eqv (quote is-group)

is-group-is-prop : β {β} {A : Type β} {_*_ : A β A β A}
β is-prop (is-group _*_)
is-group-is-prop {A = A} x y = Equiv.injective (IsoβEquiv eqv) \$
1x=1y
,β funext (Ξ» a β
monoid-inverse-unique x.has-is-monoid a _ _
x.inversel
(y.inverser β sym 1x=1y))
,β prop!
where
module x = is-group x
module y = is-group y hiding (magma-hlevel)
A-hl : β {n} β H-Level A (2 + n)
A-hl = basic-instance {T = A} 2 (x .is-group.has-is-set)
1x=1y = identities-equal _ _
(is-monoidβis-unital-magma x.has-is-monoid)
(is-monoidβis-unital-magma y.has-is-monoid)

instance
H-Level-is-group
: β {β} {G : Type β} {_+_ : G β G β G} {n}
β H-Level (is-group _+_) (suc n)
H-Level-is-group = prop-instance is-group-is-prop


Group homomorphismsπ

In contrast with monoid homomorphisms, for group homomorphisms, it is not necessary for the underlying map to explicitly preserve the unit (and the inverses); It is sufficient for the map to preserve the multiplication.

As a stepping stone, we define what it means to equip a type with a group structure: a group structure on a type.

record Group-on {β} (A : Type β) : Type β where
field
_β_ : A β A β A
has-is-group : is-group _β_

infixr 20 _β_
infixl 35 _β»ΒΉ

_β»ΒΉ : A β A
x β»ΒΉ = has-is-group .is-group.inverse x

open is-group has-is-group public


We have that a map is a group homomorphism if it preserves the multiplication.

record
is-group-hom
{β β'} {A : Type β} {B : Type β'}
(G : Group-on A) (G' : Group-on B) (e : A β B) : Type (β β β') where
private
module A = Group-on G
module B = Group-on G'

field
pres-β : (x y : A) β e (x A.β y) β‘ e x B.β e y


A tedious calculation shows that this is sufficient to preserve the identity:

  private
1A = A.unit
1B = B.unit

pres-id : e 1A β‘ 1B
pres-id =
e 1A                       β‘β¨ sym B.idr β©β‘
e 1A B.β β 1B β            β‘Λβ¨ apΒ‘ B.inverser β©β‘Λ
e 1A B.β (e 1A B.β e 1A)   β‘β¨ B.associative β©β‘
β e 1A B.β e 1A β B.β e 1A β‘β¨ ap! (sym (pres-β _ _) β ap e A.idl) β©β‘
e 1A B.β e 1A              β‘β¨ B.inverser β©β‘
1B                         β

pres-inv : β {x} β e (A.inverse x) β‘ B.inverse (e x)
pres-inv {x} =
monoid-inverse-unique B.has-is-monoid (e x) _ _
(sym (pres-β _ _) Β·Β· ap e A.inversel Β·Β· pres-id)
B.inverser

pres-diff : β {x y} β e (x A.β y) β‘ e x B.β e y
pres-diff {x} {y} =
e (x A.β y)                 β‘β¨ pres-β _ _ β©β‘
e x B.β β e (A.inverse y) β β‘β¨ ap! pres-inv β©β‘
e x B.β e y                 β

is-group-hom-is-prop
: β {β β'} {A : Type β} {B : Type β'}
{G : Group-on A} {H : Group-on B} {f}
β is-prop (is-group-hom G H f)
is-group-hom-is-prop {H = H} a b i .is-group-hom.pres-β x y =
Group-on.has-is-set H _ _ (a .is-group-hom.pres-β x y) (b .is-group-hom.pres-β x y) i

instance
H-Level-group-hom
: β {n} {β β'} {A : Type β} {B : Type β'}
{G : Group-on A} {H : Group-on B} {f}
β H-Level (is-group-hom G H f) (suc n)
H-Level-group-hom = prop-instance is-group-hom-is-prop


An equivalence is an equivalence of groups when its underlying map is a group homomorphism.

Groupβ
: β {β} (A B : Ξ£ (Type β) Group-on) (e : A .fst β B .fst) β Type β
Groupβ A B (f , _) = is-group-hom (A .snd) (B .snd) f

Group[_β_] : β {β} (A B : Ξ£ (Type β) Group-on) β Type β
Group[ A β B ] = Ξ£ (A .fst β B .fst) (is-group-hom (A .snd) (B .snd))


Making groupsπ

Since the interface of Group-on is very deeply nested, we introduce a helper function for arranging the data of a group into a record.

record make-group {β} (G : Type β) : Type β where
no-eta-equality
field
group-is-set : is-set G
unit : G
mul  : G β G β G
inv  : G β G

assoc : β x y z β mul x (mul y z) β‘ mul (mul x y) z
invl  : β x β mul (inv x) x β‘ unit
idl   : β x β mul unit x β‘ x

private
inverser : β x β mul x (inv x) β‘ unit
inverser x =
mul x (inv x)                                   β‘Λβ¨ idl _ β©β‘Λ
mul unit (mul x (inv x))                        β‘Λβ¨ apβ mul (invl _) refl β©β‘Λ
mul (mul (inv (inv x)) (inv x)) (mul x (inv x)) β‘Λβ¨ assoc _ _ _ β©β‘Λ
mul (inv (inv x)) (mul (inv x) (mul x (inv x))) β‘β¨ apβ mul refl (assoc _ _ _) β©β‘
mul (inv (inv x)) (mul (mul (inv x) x) (inv x)) β‘β¨ apβ mul refl (apβ mul (invl _) refl) β©β‘
mul (inv (inv x)) (mul unit (inv x))            β‘β¨ apβ mul refl (idl _) β©β‘
mul (inv (inv x)) (inv x)                       β‘β¨ invl _ β©β‘
unit                                            β

to-group-on : Group-on G
to-group-on .Group-on._β_ = mul
to-group-on .Group-on.has-is-group .is-group.unit = unit
to-group-on .Group-on.has-is-group .is-group.inverse = inv
to-group-on .Group-on.has-is-group .is-group.inversel = invl _
to-group-on .Group-on.has-is-group .is-group.inverser = inverser _
to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idr {x} =
mul x β unit β           β‘Λβ¨ apΒ‘ (invl x) β©β‘Λ
mul x (mul (inv x) x)    β‘β¨ assoc _ _ _ β©β‘
mul β mul x (inv x) β x  β‘β¨ ap! (inverser x) β©β‘
mul unit x               β‘β¨ idl x β©β‘
x                        β
to-group-on .Group-on.has-is-group .is-group.has-is-monoid .has-is-semigroup =
record { has-is-magma = record { has-is-set = group-is-set }
; associative = Ξ» {x y z} β assoc x y z
}

open make-group using (to-group-on) public


Symmetric groupsπ

If is a set, then the type of all bijections is also a set, and it forms the carrier for a group: The symmetric group on

Sym : β {β} (X : Set β) β Group-on (β£ X β£ β β£ X β£)
Sym X = to-group-on group-str where
open make-group
group-str : make-group (β£ X β£ β β£ X β£)
group-str .mul g f = f βe g


The group operation is composition of equivalences; The identity element is the identity equivalence.

  group-str .unit = id , id-equiv


This type is a set because is a set (because is a set by assumption), and being an equivalence is a proposition.

  group-str .group-is-set = hlevel!


The associativity and identity laws hold definitionally.

  group-str .assoc _ _ _ = trivial!
group-str .idl _ = trivial!


The inverse is given by the inverse equivalence, and the inverse equations hold by the fact that the inverse of an equivalence is both a section and a retraction.

  group-str .inv = _eβ»ΒΉ
group-str .invl (f , eqv) = ext (equivβunit eqv)