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                   ∎