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 ; _β_) public
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 ; module HLevel-instance) 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 30 _β»ΒΉ _β»ΒΉ : 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 _ _ _ = Ξ£-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))