Cayley's theorem

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-03-17.
Last modified on 2024-04-11.

module group-theory.cayleys-theorem where
Imports 
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalence-extensionality
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.sets
open import foundation.universe-levels

open import group-theory.embeddings-groups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.symmetric-groups

Theorem

Direct proof of Cayley's theorem

module _
  {l1 : Level} (G : Group l1)
  where

  map-Cayleys-theorem :
    type-Group G → type-Group (symmetric-Group (set-Group G))
  map-Cayleys-theorem = equiv-mul-Group G

  preserves-mul-map-Cayleys-theorem :
    preserves-mul-Group G (symmetric-Group (set-Group G)) map-Cayleys-theorem
  preserves-mul-map-Cayleys-theorem {x} {y} =
    eq-htpy-equiv (associative-mul-Group G x y)

  hom-Cayleys-theorem : hom-Group G (symmetric-Group (set-Group G))
  pr1 hom-Cayleys-theorem = map-Cayleys-theorem
  pr2 hom-Cayleys-theorem = preserves-mul-map-Cayleys-theorem

  is-injective-map-Cayleys-theorem : is-injective map-Cayleys-theorem
  is-injective-map-Cayleys-theorem {x} {y} p =
    ( inv (right-unit-law-mul-Group G x)) ∙
    ( htpy-eq-equiv p (unit-Group G)) ∙
    ( right-unit-law-mul-Group G y)

  is-emb-map-Cayleys-theorem : is-emb map-Cayleys-theorem
  is-emb-map-Cayleys-theorem =
    is-emb-is-injective
      ( is-set-type-Group (symmetric-Group (set-Group G)))
      ( is-injective-map-Cayleys-theorem)

  Cayleys-theorem : emb-Group G (symmetric-Group (set-Group G))
  pr1 Cayleys-theorem = hom-Cayleys-theorem
  pr2 Cayleys-theorem = is-emb-map-Cayleys-theorem

Cayley's theorem as a corollary of the Yoneda lemma

This is Corollary 2.2.10 of [Rie17], and remains to be formalized.

References

[Rie17]
Emily Riehl. Category Theory in Context. Courier Dover Publications, 03 2017. ISBN 978-0-486-82080-4. URL: https://math.jhu.edu/~eriehl/context.pdf.

Recent changes