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.
External links
- Cayley's Theorem at 1lab
- Cayley's theorem at Lab
- Cayley's theorem at Wikipedia
- Cayley's theorem at Wikidata
Recent changes
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2023-11-24. Fredrik Bakke. The orbit category of a group (#935).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-11-24. Fredrik Bakke. Indiscrete precategories (#896).