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