Whiskering pointed homotopies with respect to concatenation
Content created by Egbert Rijke.
Created on 2024-03-13.
Last modified on 2024-03-13.
module structured-types.whiskering-pointed-2-homotopies-concatenation where
Imports
open import foundation.action-on-identifications-functions open import foundation.commuting-triangles-of-identifications open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.path-algebra open import foundation.universe-levels open import foundation.whiskering-homotopies-concatenation open import foundation.whiskering-identifications-concatenation open import structured-types.pointed-2-homotopies open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-types
Idea
The whiskering operations of
pointed 2-homotopies with respect
to concatenation of pointed homotopies
are two operations that produce pointed 2-homotopies between concatenations of
pointed homotopies from either a pointed 2-homotopy on the left or on the right
of the concatenations.
-
The left whiskering¶ is an operation that takes a pointed homotopy
H : f ~∗ gand a pointed2-homotopyα : K ~²∗ Lbetween two pointed homotopiesK L : g ~∗ has indicated in the diagramK H -----> f -----> g -----> h, Land returns a pointed
2-homotopyH ∙h K ~²∗ H ∙h L. -
The right whiskering¶ is an operation that takes a pointed
2-homotopyα : H ~²∗ Kbetween two pointed homotopiesH K : f ~∗ gand a pointed homotopyL : g ~∗ has indicated in the diagramH -----> f -----> g -----> h, K Land returns a pointed
2-homotopyH ∙h L ~²∗ K ∙h L.
Definitions
Left whiskering of pointed 2-homotopies with respect to concatenation
Consider three pointed maps f := (f₀ , f₁), g := (g₀ , g₁), and
h := (h₀ , h₁) from A to B, a pointed homotopy H := (H₀ , H₁) : f ~∗ g
and a pointed 2-homotopy α := (α₀ , α₁) : K ~²∗ L between two pointed
homotopies K := (K₀ , K₁) and L := (L₀ , L₁) from g to h as indicated in
the diagram
K
H ----->
f -----> g -----> h.
L
The underlying homotopy of the left whiskering H ·l∗ α : H ∙h K ~²∗ H ∙h L is
the homotopy
H₀ ·l α₀ : H₀ ∙h K₀ ~ H₀ ∙h L₀.
The base point coherence of this homotopy is an identification witnessing that the triangle
(H ∙h K)₁
f₁ --------> ((H₀ *) ∙ (K₀ *)) ∙ h₁
\ /
(H ∙h L)₁ \ / right-whisker (left-whisker (H₀ *) (α₀ *)) h₁
\ /
∨ ∨
((H₀ *) ∙ (L₀ *)) ∙ h₁
commutes. Here, the identifications (H ∙h K)₁ and (H ∙h L)₁ are the
horizontal pastings of the
commuting triangles of identifications
H₀ * K₀ * H₀ * L₀ *
f₀ * ---> g₀ * ----> h₀ * f₀ * ---> g₀ * ----> h₀ *
\ | / \ | /
\ H₁ | K₁ / \ H₁ | L₁ /
f₁ \ |g₁ / h₁ f₁ \ |g₁ / h₁
\ | / \ | /
\ | / \ | /
∨ ∨ ∨ ∨ ∨ ∨
* *.
Then the triangle
horizontal-pasting H₁ K₁
f₁ --------> (H₀ * ∙ K₀ *) ∙ h₁
\ /
\ /
horizontal-pasting H₁ L₁ \ / right-whisker (left-whisker (H₀ *) (α₀ *)) h₁
\ /
∨ ∨
(H₀ * ∙ K₀ *) ∙ h₁
commutes by left whiskering of horizontal pasting of commuting triangles of identifications.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {f g h : A →∗ B} (H : f ~∗ g) (K L : g ~∗ h) (α : K ~²∗ L) where htpy-left-whisker-concat-pointed-2-htpy : unpointed-htpy-pointed-htpy ( concat-pointed-htpy H K) ( concat-pointed-htpy H L) htpy-left-whisker-concat-pointed-2-htpy = left-whisker-concat-htpy (htpy-pointed-htpy H) (htpy-pointed-2-htpy α) coherence-point-left-whisker-concat-pointed-2-htpy : coherence-point-unpointed-htpy-pointed-htpy ( concat-pointed-htpy H K) ( concat-pointed-htpy H L) ( htpy-left-whisker-concat-pointed-2-htpy) coherence-point-left-whisker-concat-pointed-2-htpy = left-whisker-horizontal-pasting-coherence-triangle-identifications ( preserves-point-pointed-map f) ( preserves-point-pointed-map g) ( preserves-point-pointed-map h) ( htpy-pointed-htpy H (point-Pointed-Type A)) ( htpy-pointed-htpy K (point-Pointed-Type A)) ( htpy-pointed-htpy L (point-Pointed-Type A)) ( coherence-point-pointed-htpy H) ( coherence-point-pointed-htpy K) ( coherence-point-pointed-htpy L) ( htpy-pointed-2-htpy α (point-Pointed-Type A)) ( coherence-point-pointed-2-htpy α) left-whisker-concat-pointed-2-htpy : concat-pointed-htpy H K ~²∗ concat-pointed-htpy H L pr1 left-whisker-concat-pointed-2-htpy = htpy-left-whisker-concat-pointed-2-htpy pr2 left-whisker-concat-pointed-2-htpy = coherence-point-left-whisker-concat-pointed-2-htpy
Right whiskering of pointed 2-homotopies with respect to concatenation
Consider three pointed maps f := (f₀ , f₁), g := (g₀ , g₁), and
h := (h₀ , h₁) from A to B, a pointed 2-homotopy
α := (α₀ , α₁) : H ~²∗ K between two pointed homotopies H := (H₀ , H₁) and
K := (K₀ , K₁) from f to g and a pointed homotopy
L := (L₀ , L₁) : g ~∗ h as indicated in the diagram
H
----->
f -----> g -----> h.
K L
The underlying homotopy of the right whiskering α ·r∗ L : H ∙h L ~²∗ K ∙h L is
the homotopy
α₀ ·r L₀ : H₀ ∙h L₀ ~ K₀ ∙h L₀.
The base point coherence of this homotopy is an identification witnessing that the triangle
(H ∙h L)₁
f₁ --------> ((H₀ *) ∙ (L₀ *)) ∙ h₁
\ /
(K ∙h L)₁ \ / right-whisker (right-whisker (α₀ *) (L₀ *)) h₁
\ /
∨ ∨
((K₀ *) ∙ (L₀ *)) ∙ h₁
commutes. Here, the identifications (H ∙h L)₁ and (K ∙h L)₁ are the
horizontal pastings of the
commuting triangles of identifications
H₀ * L₀ * K₀ * L₀ *
f₀ * ---> g₀ * ----> h₀ * f₀ * ---> g₀ * ----> h₀ *
\ | / \ | /
\ H₁ | L₁ / \ K₁ | L₁ /
f₁ \ |g₁ / h₁ f₁ \ |g₁ / h₁
\ | / \ | /
\ | / \ | /
∨ ∨ ∨ ∨ ∨ ∨
* *.
Then the triangle
horizontal-pasting H₁ L₁
f₁ --------> (H₀ * ∙ L₀ *) ∙ h₁
\ /
\ /
horizontal-pasting K₁ L₁ \ / right-whisker (right-whisker (α₀ *) (L₀ *)) h₁
\ /
∨ ∨
(K₀ * ∙ L₀ *) ∙ h₁
commutes by right whiskering of horizontal pasting of commuting triangles of identifications.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {f g h : A →∗ B} (H K : f ~∗ g) (α : H ~²∗ K) (L : g ~∗ h) where htpy-right-whisker-concat-pointed-2-htpy : unpointed-htpy-pointed-htpy ( concat-pointed-htpy H L) ( concat-pointed-htpy K L) htpy-right-whisker-concat-pointed-2-htpy = right-whisker-concat-htpy (htpy-pointed-2-htpy α) (htpy-pointed-htpy L) coherence-point-right-whisker-concat-pointed-2-htpy : coherence-point-unpointed-htpy-pointed-htpy ( concat-pointed-htpy H L) ( concat-pointed-htpy K L) ( htpy-right-whisker-concat-pointed-2-htpy) coherence-point-right-whisker-concat-pointed-2-htpy = right-whisker-horizontal-pasting-coherence-triangle-identifications ( preserves-point-pointed-map f) ( preserves-point-pointed-map g) ( preserves-point-pointed-map h) ( htpy-pointed-htpy H (point-Pointed-Type A)) ( htpy-pointed-htpy K (point-Pointed-Type A)) ( htpy-pointed-htpy L (point-Pointed-Type A)) ( coherence-point-pointed-htpy H) ( coherence-point-pointed-htpy K) ( coherence-point-pointed-htpy L) ( htpy-pointed-2-htpy α (point-Pointed-Type A)) ( coherence-point-pointed-2-htpy α) right-whisker-concat-pointed-2-htpy : concat-pointed-htpy H L ~²∗ concat-pointed-htpy K L pr1 right-whisker-concat-pointed-2-htpy = htpy-right-whisker-concat-pointed-2-htpy pr2 right-whisker-concat-pointed-2-htpy = coherence-point-right-whisker-concat-pointed-2-htpy
Recent changes
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).