open import 1Lab.Prelude

open import Algebra.Group.Cat.Base
open import Algebra.Group

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$.

To start with, we note that any element $x$ of $G$ determines a bijection on the underlying set of $G$, by multiplication with $x$ on the left. The inverse of this bijection is given by multiplication with $x^{-1}$, 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 $G$ to $\mathrm{Sym}(G)$:

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, $G$ embeds as a subgroup of $\mathrm{Sym}(G)$ (the image of Cayley).

Cayley-injective : injective Cayley
Cayley-injective {x} {y} eqvs-equal =