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

First, recall that we get a family of equivalences 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 to

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, 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                   β