open import 1Lab.Prelude

open import Algebra.Group.Instances.Symmetric
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 .$

First, recall that we get a family of equivalences $G ≃ G$ by multiplication on the left, the principal action of $G$ on itself:

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                   ∎