Conjugation of pointed types

Content created by Egbert Rijke.

Created on 2023-07-19.
Last modified on 2024-03-13.

module structured-types.conjugation-pointed-types where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-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 structured-types.pointed-types

open import synthetic-homotopy-theory.conjugation-loops
open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.loop-spaces


Conjugation on a pointed type (B,b) is defined as a family of pointed maps conj u p : (B,b) →∗ (B,u) indexed by u : B and p : b = u, such that conj b ω acts on the loop space Ω (B , b) by conjugation, i.e., it maps a loop α : b = b to the loop ω⁻¹αω.


module _
  {l : Level} (B : Pointed-Type l)

  map-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    type-Pointed-Type B  type-Pointed-Type B
  map-conjugation-Pointed-Type refl = id

  preserves-point-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    map-conjugation-Pointed-Type p (point-Pointed-Type B)  u
  preserves-point-conjugation-Pointed-Type refl = refl

  conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    B →∗ (type-Pointed-Type B , u)
  pr1 (conjugation-Pointed-Type p) = map-conjugation-Pointed-Type p
  pr2 (conjugation-Pointed-Type p) = preserves-point-conjugation-Pointed-Type p


The conjugation map on a pointed type acts on loop spaces by conjugation

module _
  {l : Level} {B : Pointed-Type l}

  action-on-loops-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    Ω B →∗ Ω (type-Pointed-Type B , u)
  action-on-loops-conjugation-Pointed-Type p =
    pointed-map-Ω (conjugation-Pointed-Type B p)

  map-action-on-loops-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    type-Ω B  type-Ω (type-Pointed-Type B , u)
  map-action-on-loops-conjugation-Pointed-Type p =
      ( action-on-loops-conjugation-Pointed-Type p)

  preserves-point-action-on-loops-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    map-action-on-loops-conjugation-Pointed-Type p refl  refl
  preserves-point-action-on-loops-conjugation-Pointed-Type p =
      ( action-on-loops-conjugation-Pointed-Type p)

  compute-action-on-loops-conjugation-Pointed-Type' :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    conjugation-Ω' p ~∗ action-on-loops-conjugation-Pointed-Type p
  pr1 (compute-action-on-loops-conjugation-Pointed-Type' refl) ω = inv (ap-id ω)
  pr2 (compute-action-on-loops-conjugation-Pointed-Type' refl) = refl

  compute-action-on-loops-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    conjugation-Ω p ~∗ action-on-loops-conjugation-Pointed-Type p
  compute-action-on-loops-conjugation-Pointed-Type p =
      ( compute-conjugation-Ω p)
      ( compute-action-on-loops-conjugation-Pointed-Type' p)

  htpy-compute-action-on-loops-conjugation-Pointed-Type :
    {u : type-Pointed-Type B} (p : point-Pointed-Type B  u) 
    map-conjugation-Ω p ~ map-action-on-loops-conjugation-Pointed-Type p
  htpy-compute-action-on-loops-conjugation-Pointed-Type p =
    pr1 (compute-action-on-loops-conjugation-Pointed-Type p)

Recent changes