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 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 xβˆ’1x^{-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 GG to Sym(G)\id{Sym}(G):

Cayley-is-hom : Group-hom (G .snd) (Sym G-set) Cayley
Cayley-is-hom .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, 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 βŸ©β‰‘
  y                   ∎