{-# 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
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 β
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 (mul x y) z β‘ mul x (mul 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) β‘β¨ sym (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} β 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 : β {β} (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))