open import 1Lab.Prelude

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

To start with, we note that any element xx of GG determines a bijection on the underlying set of GG, by multiplication with xx on the left. The inverse of this bijection is given by multiplication with x1x^{-1}, and the proof that these are in fact inverse functions are given by the group laws:

Cayley : G .fst  G .fst  G .fst
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 
  bij .snd .is-iso.linv y =
    x ⁻¹  (x  y) ≡⟨ cancell inversel 

We then show that this map is a group homomorphism from GG to Sym(G)\id{Sym}(G):

Cayley-is-hom : Group-hom G (Sym G-set) Cayley
Cayley-is-hom .Group-hom.pres-⋆ x y = Σ-prop-path is-equiv-is-prop (funext lemma) where
  lemma : (e : G .fst)  (x  y)  e  x  (y  e)
  lemma e = sym associative

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