module Algebra.Group.Cayley {β} (G : Group β) where open Group-on (G .snd) renaming (underlying-set to G-set)
Cayleyβs theoremπ
Cayleyβs theorem says that any group admits a representation as a subgroup of a symmetric group, specifically the symmetric group acting on the underlying set of .
To start with, we note that any element of determines a bijection on the underlying set of , by multiplication with on the left. 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:
Cayley : β G β β β G β β β G β Cayley x = IsoβEquiv bij where bij : Iso _ _ bij .fst y = x β y bij .snd .is-iso.inv y = x β»ΒΉ β y bij .snd .is-iso.rinv y = x β (x β»ΒΉ β y) β‘β¨ cancell inverser β©β‘ y β bij .snd .is-iso.linv y = x β»ΒΉ β (x β y) β‘β¨ cancell inversel β©β‘ y β
We then show that this map is a group homomorphism from to :
Cayley-is-hom : is-group-hom (G .snd) (Sym G-set) Cayley Cayley-is-hom .is-group-hom.pres-β x y = Ξ£-prop-path is-equiv-is-prop (funext lemma) where lemma : (e : β G β) β (x β y) β e β‘ x β (y β e) lemma e = sym associative
Finally, we show that this map is injective; Thus,
embeds as a subgroup of
(the image of Cayley
).
Cayley-injective : injective Cayley Cayley-injective {x} {y} eqvs-equal = x β‘β¨ sym idr β©β‘ x β unit β‘β¨β© Cayley x .fst unit β‘β¨ happly (ap fst eqvs-equal) unit β©β‘ Cayley y .fst unit β‘β¨β© y β unit β‘β¨ idr β©β‘ y β