Whiskering of pointed homotopies with respect to composition of pointed maps

Content created by Egbert Rijke.

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

module structured-types.whiskering-pointed-homotopies-composition where
Imports 
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.commuting-triangles-of-identifications
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import structured-types.pointed-2-homotopies
open import structured-types.pointed-families-of-types
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

The whiskering operations of pointed homotopies with respect to composition of pointed maps are two operations that produce pointed homotopies between composites of pointed maps from either a pointed homotopy on the left or on the right of the composition.

  • Consider a pointed homotopy H : f ~∗ g between pointed maps f g : A →∗ B, and consider a pointed map h : B →∗ C, as indicated in the diagram

          f
    ----->     h
  A -----> B -----> C.
      g

    The left whiskering operation on pointed homotopies of h and H is a pointed homotopy

      h ·l∗ H : h ∘∗ f ~∗ h ∘∗ g.

  • Consider a pointed map f : A →∗ B and consider a pointed homotopy H : g ~∗ g between tw pointed maps g h : B →∗ C, as indicated in the diagram

                   g
      f      ----->
  A -----> B -----> C.
               h

    The right whiskering operation on pointed homotopies of H and f is a pointed homotopy

      H ·r∗ f : g ∘∗ f ~∗ h ∘∗ f.

Definitions

Left whiskering of pointed homotopies

Consider two pointed maps f := (f₀ , f₁) : A →∗ B and g := (g₀ , g₁) : A →∗ B equipped with a pointed homotopy H := (H₀ , H₁) : f ~∗ g, and consider furthermore a pointed map h := (h₀ , h₁) : B →∗ C. Then we construct a pointed homotopy

  h ·l∗ H : (h ∘∗ f) ~∗ (h ∘∗ g).

Construction. The underlying homotopy of h ·l∗ H is the whiskered homotpy

  h₀ ·l H₀.

For the coherence, we have to show that the triangle

            ap h₀ (H₀ *)
  h₀ (f₀ *) ------------> h₀ (g₀ *)
           \             /
   ap h₀ f₁ \           / ap h₀ g₁
             ∨         ∨
           h₀ *       h₀ *
               \     /
             h₁ \   / h₁
                 ∨ ∨
                  ∗

commutes. By right whiskering of commuting triangles of identifications with respect to concatenation it suffices to show that the triangle

           ap h₀ (H₀ *)
  h₀ (f₀ *) ---------> h₀ (g₀ *)
           \          /
   ap h₀ f₁ \        / ap h₀ g₁
             \      /
              ∨    ∨
               h₀ *

commutes. By functoriality of commuting triangles of identifications, this follows from the fact that the triangle

        H₀ *
  f₀ * ------> g₀ *
      \       /
    f₁ \     / g₁
        \   /
         ∨ ∨
          *

commutes.

module _
  {l1 l2 l3 : Level}
  {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3}
  (h : B →∗ C) (f g : A →∗ B) (H : f ~∗ g)
  where

  htpy-left-whisker-comp-pointed-htpy :
    map-comp-pointed-map h f ~ map-comp-pointed-map h g
  htpy-left-whisker-comp-pointed-htpy =
    map-pointed-map h ·l htpy-pointed-htpy H

  coherence-point-left-whisker-comp-pointed-htpy :
    coherence-point-unpointed-htpy-pointed-Π
      ( h ∘∗ f)
      ( h ∘∗ g)
      ( htpy-left-whisker-comp-pointed-htpy)
  coherence-point-left-whisker-comp-pointed-htpy =
    right-whisker-concat-coherence-triangle-identifications
      ( ap (map-pointed-map h) (preserves-point-pointed-map f))
      ( ap (map-pointed-map h) (preserves-point-pointed-map g))
      ( ap
        ( map-pointed-map h)
        ( htpy-pointed-htpy H (point-Pointed-Type A)))
      ( preserves-point-pointed-map h)
      ( map-coherence-triangle-identifications
        ( map-pointed-map h)
        ( preserves-point-pointed-map f)
        ( preserves-point-pointed-map g)
        ( htpy-pointed-htpy H (point-Pointed-Type A))
        ( coherence-point-pointed-htpy H))

  left-whisker-comp-pointed-htpy : h ∘∗ f ~∗ h ∘∗ g
  pr1 left-whisker-comp-pointed-htpy =
    htpy-left-whisker-comp-pointed-htpy
  pr2 left-whisker-comp-pointed-htpy =
    coherence-point-left-whisker-comp-pointed-htpy

Right whiskering of pointed homotopies

Consider a pointed map f := (f₀ , f₁) : A →∗ B and two pointed maps g := (g₀ , g₁) : B →∗ C and h := (h₀ , h₁) : B →∗ C equipped with a pointed homotopy H := (H₀ , H₁) : g ~∗ h. Then we construct a pointed homotopy

  H ·r∗ f : (g ∘∗ f) ~∗ (h ∘∗ f).

Construction. The underlying homotopy of H ·r∗ f is the homotopy

  H₀ ·r f₀ : (g₀ ∘ f₀) ~ (h₀ ∘ f₀).

Then we have to show that the outer triangle in the diagram

              H₀ (f₀ *)
  g₀ (f₀ *) ------------> h₀ (f₀ *)
           \             /
   ap g₀ f₁ \           / ap h₀ f₁
             ∨  H₀ *   ∨
           g₀ * ----> h₀ *
               \     /
             g₁ \   / h₁
                 ∨ ∨
                  ∗

commutes. This is done by vertically pasting the upper square and the lower triangle. The upper square commutes by inverse naturality of the homotopy H₀. The lower triangle is the base point coherence H₁ of the pointed homotopy H ≐ (H₀ , H₁).

module _
  {l1 l2 l3 : Level}
  {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3}
  (g1 g2 : B →∗ C) (H : g1 ~∗ g2) (f : A →∗ B)
  where

  htpy-right-whisker-comp-pointed-htpy :
    unpointed-htpy-pointed-Π (g1 ∘∗ f) (g2 ∘∗ f)
  htpy-right-whisker-comp-pointed-htpy =
    htpy-pointed-htpy H ·r map-pointed-map f

  coherence-point-right-whisker-comp-pointed-htpy :
    coherence-point-unpointed-htpy-pointed-Π
      ( g1 ∘∗ f)
      ( g2 ∘∗ f)
      ( htpy-right-whisker-comp-pointed-htpy)
  coherence-point-right-whisker-comp-pointed-htpy =
    vertical-pasting-coherence-square-coherence-triangle-identifications
      ( htpy-pointed-htpy H _)
      ( ap (map-pointed-map g1) _)
      ( ap (map-pointed-map g2) _)
      ( htpy-pointed-htpy H _)
      ( preserves-point-pointed-map g1)
      ( preserves-point-pointed-map g2)
      ( inv-nat-htpy (htpy-pointed-htpy H) _)
      ( coherence-point-pointed-htpy H)

  right-whisker-comp-pointed-htpy : g1 ∘∗ f ~∗ g2 ∘∗ f
  pr1 right-whisker-comp-pointed-htpy =
    htpy-right-whisker-comp-pointed-htpy
  pr2 right-whisker-comp-pointed-htpy =
    coherence-point-right-whisker-comp-pointed-htpy

Properties

Computing the left whiskering of the reflexive pointed homotopy

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

  compute-refl-left-whisker-comp-pointed-htpy :
    pointed-2-htpy
      ( left-whisker-comp-pointed-htpy h f f (refl-pointed-htpy f))
      ( refl-pointed-htpy (h ∘∗ f))
  compute-refl-left-whisker-comp-pointed-htpy =
    refl-pointed-2-htpy (refl-pointed-htpy (h ∘∗ f))

Computing the right whiskering of the reflexive pointed homotopy

Consider two pointed maps f := (f₀ , f₁) : A →∗ B and g := (g₀ , g₁) : B →∗ C. We are constructing a pointed 2-homotopy

  right-whisker-comp-pointed-htpy (refl-pointed-htpy h) f ~∗
  refl-pointed-htpy (g ∘∗ f)

The underlying homotopy of this pointed 2-homotopy is refl-htpy. The base point coherence of this homotopy is an identification witnessing that the triangle

                   H₁
  ap g₀ f₁ ∙ g₁ ------> refl ∙ (ap g₀ f₁ ∙ g₁)
               \       /
           refl \     / right-whisker-concat refl (ap g₀ f₁ ∙ g₁) ≐ refl
                 \   /
                  ∨ ∨
       refl ∙ (ap g₀ f₁ ∙ g₁)

commutes. Here, the identification H₁ is the vertical pasting of the upper square and the lower triangle in the diagram

                refl
  g₀ (f₀ *) ------------> g₀ (f₀ *)
           \             /
   ap g₀ f₁ \           / ap g₀ f₁
             ∨  refl   ∨
           g₀ * ----> g₀ *
               \     /
             g₁ \   / g₁
                 ∨ ∨
                  ∗.

The upper square in this diagram is the inverse naturality of the reflexive homotopy refl-htpy and the lower triangle in this diagram is the reflexive identification.

Recall that the inverse naturality of the reflexive homotopy inv-nat-htpy refl-htpy f₁ computes to the horizontally constant square of identifications. Furthermore, the vertical pasting of the horizontally constant square right-unit and any commuting triangle refl computes to refl. Therefore it follows that the identification H₁ above is equal to refl, as was required to show.

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

  htpy-compute-refl-right-whisker-comp-pointed-htpy :
    unpointed-htpy-pointed-htpy
      ( right-whisker-comp-pointed-htpy h h (refl-pointed-htpy h) f)
      ( refl-pointed-htpy (h ∘∗ f))
  htpy-compute-refl-right-whisker-comp-pointed-htpy = refl-htpy

  coherence-point-compute-refl-right-whisker-comp-pointed-htpy :
    coherence-point-unpointed-htpy-pointed-htpy
      ( right-whisker-comp-pointed-htpy h h (refl-pointed-htpy h) f)
      ( refl-pointed-htpy (h ∘∗ f))
      ( htpy-compute-refl-right-whisker-comp-pointed-htpy)
  coherence-point-compute-refl-right-whisker-comp-pointed-htpy =
    inv
      ( ( right-unit) ∙
        ( ( ap
            ( λ t →
              vertical-pasting-coherence-square-coherence-triangle-identifications
                ( refl)
                ( ap (map-pointed-map h) (preserves-point-pointed-map f))
                ( ap (map-pointed-map h) (preserves-point-pointed-map f))
                ( refl)
                ( preserves-point-pointed-map h)
                ( preserves-point-pointed-map h)
                ( t)
                ( refl))
            ( inv-nat-refl-htpy
              ( map-pointed-map h)
              ( preserves-point-pointed-map f))) ∙
          ( right-whisker-concat-horizontal-refl-coherence-square-identifications
            ( ap (map-pointed-map h) (preserves-point-pointed-map f))
            ( preserves-point-pointed-map h))))

  compute-refl-right-whisker-comp-pointed-htpy :
    pointed-2-htpy
      ( right-whisker-comp-pointed-htpy h h (refl-pointed-htpy h) f)
      ( refl-pointed-htpy (h ∘∗ f))
  pr1 compute-refl-right-whisker-comp-pointed-htpy =
    htpy-compute-refl-right-whisker-comp-pointed-htpy
  pr2 compute-refl-right-whisker-comp-pointed-htpy =
    coherence-point-compute-refl-right-whisker-comp-pointed-htpy

Recent changes