# Cayley's theorem

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

Created on 2022-03-17.

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.