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 has-is-monoid : is-monoid unit _*_
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 inversel : {x : A} β inverse x * x β‘ unit inverser : {x : A} β x * inverse x β‘ unit open is-monoid has-is-monoid public
is-group is propositionalπ
Showing that is-group takes values in propositions is straightforward, but tedious. Suppose that are both witnesses of is-group for the same operator; Weβll build a path .
is-group-is-prop : β {β} {A : Type β} {_*_ : A β A β A} β is-prop (is-group _*_) is-group-is-prop {A = A} {_*_ = _*_} x y = path where open is-group
We begin by constructing a line showing that the underlying monoid structures are identical β but since these have different types, we must also show that the units are the same.
same-unit : x .unit β‘ y .unit same-unit = identities-equal (x .unit) (y .unit) (is-monoidβis-unital-magma (x .has-is-monoid)) (is-monoidβis-unital-magma (y .has-is-monoid))
We then use the fact that is-monoid is a proposition
to
conclude that the monoid structures underlying
and
are the same.
same-monoid : PathP (Ξ» i β is-monoid (same-unit i) _*_) (x .has-is-monoid) (y .has-is-monoid) same-monoid = is-propβpathp (Ξ» i β hlevel {T = is-monoid (same-unit i) _*_} 1) (x .has-is-monoid) (y .has-is-monoid)
Since inverses in monoids are unique (when they exist), it follows that the inverse-assigning maps are pointwise equal; By extensionality, they are the same map.
same-inverses : (e : A) β x .inverse e β‘ y .inverse e same-inverses e = monoid-inverse-unique (y .has-is-monoid) _ _ _ (x .inversel β same-unit) (y .inverser)
Since the underlying type of a group
is a set,
we have that any parallel paths are equal - even when the paths are
dependent! This gives us the equations between the
inversel
and
inverser
fields of x
and y
.
same-invl : (e : A) β Square _ _ _ _ same-invl e = is-setβsquarep (Ξ» _ _ β x .has-is-monoid .has-is-set) (apβ _*_ (same-inverses e) refl) (x .inversel) (y .inversel) same-unit same-invr : (e : A) β Square _ _ _ _ same-invr e = is-setβsquarep (Ξ» _ _ β x .has-is-monoid .has-is-set) (apβ _*_ refl (same-inverses e)) (x .inverser) (y .inverser) same-unit
Putting all of this together lets us conclude that x
and
y
are identical.
path : x β‘ y path i .unit = same-unit i path i .has-is-monoid = same-monoid i path i .inverse e = same-inverses e i path i .inversel {e} = same-invl e i path i .inverser {e} = same-invr e i 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 30 _β»ΒΉ _β»ΒΉ : A β A x β»ΒΉ = has-is-group .is-group.inverse x open is-group has-is-group public Group : (β : Level) β Type (lsuc β) Group β = Ξ£ (Type β) Group-on
We have that a map is a group homomorphism if it preserves the multiplication.
record Group-hom {β ββ²} (A : Group β) (B : Group ββ²) (e : A .fst β B .fst) : Type (β β ββ²) where private module A = Group-on (A .snd) module B = Group-on (B .snd) field pres-β : (x y : A .fst) β 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 β
An equivalence
is an equivalence of groups when its underlying map is a group
homomorphism.
Groupβ : β {β} (A B : Group β) (e : A .fst β B .fst) β Type β Groupβ A B (f , _) = Group-hom A B f Group[_β_] : β {β} (A B : Group β) β Type β Group[ A β B ] = Ξ£ (A .fst β B .fst) (Group-hom A B)
We automatically derive the proof that paths between groups are homomorphic equivalences:
Group-univalent : β {β} β is-univalent {β = β} (HomTβStr Groupβ) Group-univalent {β = β} = Derive-univalent-record (record-desc (Group-on {β = β}) Groupβ (record: field[ _β_ by pres-β ] axiom[ has-is-group by (Ξ» _ β is-group-is-prop) ])) where open Group-on open Group-hom
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 (mul x y) z β‘ mul x (mul y z) invl : β x β mul (inv x) x β‘ unit invr : β x β mul x (inv x) β‘ unit idl : β x β mul unit x β‘ x 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 = invr _ 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) β‘β¨ sym (assoc _ _ _) β©β‘ mul β mul x (inv x) β x β‘β¨ ap! (invr 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} β sym (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 : β {β} β Set β β Group β Sym X .fst = β£ X β£ β β£ X β£ Sym X .snd = to-group-on group-str where open make-group open n-Type X using (H-Level-n-type) 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 2
The associativity and identity laws hold definitionally.
group-str .assoc _ _ _ = Ξ£-prop-path is-equiv-is-prop refl group-str .idl _ = Ξ£-prop-path is-equiv-is-prop refl
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) = Ξ£-prop-path is-equiv-is-prop (funext (equivβunit eqv)) group-str .invr (f , eqv) = Ξ£-prop-path is-equiv-is-prop (funext (equivβcounit eqv))