Conjugation of loops
Content created by Egbert Rijke.
Created on 2023-07-19.
Last modified on 2024-03-13.
module synthetic-homotopy-theory.conjugation-loops where
Imports
open import foundation.dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import synthetic-homotopy-theory.loop-spaces
Idea
For any identification p : x = y
in a type
A
there is an conjugation action Ω (A , x) →∗ Ω (A , y)
on
loop spaces, which is the
pointed map given by ω ↦ p⁻¹ωp
.
Definition
The standard definition of conjugation on loop spaces
module _ {l : Level} {A : UU l} where map-conjugation-Ω : {x y : A} (p : x = y) → type-Ω (A , x) → type-Ω (A , y) map-conjugation-Ω p ω = inv p ∙ (ω ∙ p) preserves-point-conjugation-Ω : {x y : A} (p : x = y) → map-conjugation-Ω p refl = refl preserves-point-conjugation-Ω p = left-inv p conjugation-Ω : {x y : A} (p : x = y) → Ω (A , x) →∗ Ω (A , y) pr1 (conjugation-Ω p) = map-conjugation-Ω p pr2 (conjugation-Ω p) = preserves-point-conjugation-Ω p
A second definition of conjugation on loop spaces
module _ {l : Level} {A : UU l} where conjugation-Ω' : {x y : A} (p : x = y) → Ω (A , x) →∗ Ω (A , y) conjugation-Ω' refl = id-pointed-map map-conjugation-Ω' : {x y : A} (p : x = y) → type-Ω (A , x) → type-Ω (A , y) map-conjugation-Ω' p = map-pointed-map (conjugation-Ω' p) preserves-point-conjugation-Ω' : {x y : A} (p : x = y) → map-conjugation-Ω' p refl = refl preserves-point-conjugation-Ω' p = preserves-point-pointed-map (conjugation-Ω' p)
Properties
The two definitions of conjugation on loop spaces are pointed homotopic
module _ {l : Level} {A : UU l} where htpy-compute-conjugation-Ω : {x y : A} (p : x = y) → map-conjugation-Ω p ~ map-conjugation-Ω' p htpy-compute-conjugation-Ω refl ω = right-unit coherence-point-compute-conjugation-Ω : {x y : A} (p : x = y) → coherence-point-unpointed-htpy-pointed-Π ( conjugation-Ω p) ( conjugation-Ω' p) ( htpy-compute-conjugation-Ω p) coherence-point-compute-conjugation-Ω refl = refl compute-conjugation-Ω : {x y : A} (p : x = y) → conjugation-Ω p ~∗ conjugation-Ω' p pr1 (compute-conjugation-Ω p) = htpy-compute-conjugation-Ω p pr2 (compute-conjugation-Ω p) = coherence-point-compute-conjugation-Ω p
Recent changes
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).
- 2023-09-15. Egbert Rijke. update contributors, remove unused imports (#772).
- 2023-07-19. Egbert Rijke. refactoring pointed maps (#682).
- 2023-07-19. Egbert Rijke. Conjugation on higher groups (#681).