Pointed retractions of pointed maps

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-03-13.

module structured-types.pointed-retractions where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.retractions

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

A pointed retraction of a pointed map f : A →∗ B consists of a pointed map g : B →∗ A equipped with a pointed homotopy H : g ∘∗ f ~∗ id.

Definitions

The predicate of being a pointed retraction of a pointed map

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  is-pointed-retraction : (B →∗ A) → UU l1
  is-pointed-retraction g = g ∘∗ f ~∗ id-pointed-map

The type of pointed retractions of a pointed map

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  pointed-retraction : UU (l1 ⊔ l2)
  pointed-retraction =
    Σ (B →∗ A) (is-pointed-retraction f)

  module _
    (r : pointed-retraction)
    where

    pointed-map-pointed-retraction : B →∗ A
    pointed-map-pointed-retraction = pr1 r

    is-pointed-retraction-pointed-retraction :
      is-pointed-retraction f pointed-map-pointed-retraction
    is-pointed-retraction-pointed-retraction = pr2 r

    map-pointed-retraction : type-Pointed-Type B → type-Pointed-Type A
    map-pointed-retraction = map-pointed-map pointed-map-pointed-retraction

    preserves-point-pointed-map-pointed-retraction :
      map-pointed-retraction (point-Pointed-Type B) ＝ point-Pointed-Type A
    preserves-point-pointed-map-pointed-retraction =
      preserves-point-pointed-map pointed-map-pointed-retraction

    is-retraction-pointed-retraction :
      is-retraction (map-pointed-map f) map-pointed-retraction
    is-retraction-pointed-retraction =
      htpy-pointed-htpy is-pointed-retraction-pointed-retraction

    retraction-pointed-retraction : retraction (map-pointed-map f)
    pr1 retraction-pointed-retraction = map-pointed-retraction
    pr2 retraction-pointed-retraction = is-retraction-pointed-retraction

    coherence-point-is-retraction-pointed-retraction :
      coherence-point-unpointed-htpy-pointed-Π
        ( pointed-map-pointed-retraction ∘∗ f)
        ( id-pointed-map)
        ( is-retraction-pointed-retraction)
    coherence-point-is-retraction-pointed-retraction =
      coherence-point-pointed-htpy is-pointed-retraction-pointed-retraction

Properties

Any retraction of a pointed map preserves the base point in a unique way making the retracting homotopy pointed

Consider a retraction g : B → A of a pointed map f := (f₀ , f₁) : A →∗ B. Then g is base point preserving.

Proof. Our goal is to show that g * ＝ *. Since f is pointed, we have f * ＝ * and hence

       (ap g f₁)⁻¹              H *
  g * -------------> g (f₀ *) -------> *.

In order to show that the retracting homotopy H : g ∘ f₀ ~ id is pointed, we have to show that the triangle of identifications

                                   H *
                         g (f₀ *) -----> *
                                \       /
  ap g f₁ ∙ ((ap g f₁)⁻¹ ∙ H *)  \     / refl
                                  \   /
                                   ∨ ∨
                                    *

commutes. This follows by the fact that concatenating with an inverse identification is inverse to concatenating with the original identification, and the right unit law of concatenation.

Note that the pointing of g chosen above is the unique way making the retracting homotopy pointed, because the map p ↦ ap g f₁ ∙ p is an equivalence with a contractible fiber at H * ∙ refl.

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  (g : type-Pointed-Type B → type-Pointed-Type A)
  (H : is-retraction (map-pointed-map f) g)
  where

  abstract
    uniquely-preserves-point-is-retraction-pointed-map :
      is-contr
        ( Σ ( g (point-Pointed-Type B) ＝ point-Pointed-Type A)
            ( coherence-square-identifications
              ( H (point-Pointed-Type A))
              ( ap g (preserves-point-pointed-map f))
              ( refl)))
    uniquely-preserves-point-is-retraction-pointed-map =
      is-contr-map-is-equiv
        ( is-equiv-concat (ap g (preserves-point-pointed-map f)) _)
        ( H (point-Pointed-Type A) ∙ refl)

  preserves-point-is-retraction-pointed-map :
    g (point-Pointed-Type B) ＝ point-Pointed-Type A
  preserves-point-is-retraction-pointed-map =
    inv (ap g (preserves-point-pointed-map f)) ∙ H (point-Pointed-Type A)

  pointed-map-is-retraction-pointed-map :
    B →∗ A
  pr1 pointed-map-is-retraction-pointed-map = g
  pr2 pointed-map-is-retraction-pointed-map =
    preserves-point-is-retraction-pointed-map

  coherence-point-is-retraction-pointed-map :
    coherence-point-unpointed-htpy-pointed-Π
      ( pointed-map-is-retraction-pointed-map ∘∗ f)
      ( id-pointed-map)
      ( H)
  coherence-point-is-retraction-pointed-map =
    ( is-section-inv-concat (ap g (preserves-point-pointed-map f)) _) ∙
    ( inv right-unit)

  is-pointed-retraction-is-retraction-pointed-map :
    is-pointed-retraction f pointed-map-is-retraction-pointed-map
  pr1 is-pointed-retraction-is-retraction-pointed-map =
    H
  pr2 is-pointed-retraction-is-retraction-pointed-map =
    coherence-point-is-retraction-pointed-map

Recent changes