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 $G$ admits a representation as a subgroup of a symmetric group, specifically the symmetric group acting on the underlying set of $G.$

First, recall that we get a family of equivalences $GβG$ by multiplication on the left:

Cayley : β G β β β G β β β G β Cayley x = (Ξ» y β x β y) , β-equivl x

We then show that this map is a group homomorphism from $G$ to $Sym(G):$

Cayley-is-hom : is-group-hom (G .snd) (Sym G-set) Cayley Cayley-is-hom .is-group-hom.pres-β x y = ext Ξ» e β sym associative

Finally, we show that this map is injective; Thus,
$G$
embeds as a subgroup of
$Sym(G)$
(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 β