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

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

import Algebra.Monoid.Reasoning as Mon

open is-monoid hiding (idl ; idr)

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

  infixr 20 _β_
_β_ : 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 Mon underlying-monoid 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 = Iso.injective 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 and inverses:

  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