Zigzags between sequential diagrams
Content created by Vojtěch Štěpančík.
Created on 2024-05-23.
Last modified on 2024-05-23.
module synthetic-homotopy-theory.zigzags-sequential-diagrams where
Imports
open import elementary-number-theory.natural-numbers open import foundation.cartesian-product-types open import foundation.commuting-squares-of-homotopies open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-maps open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.retractions open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import synthetic-homotopy-theory.cocones-under-sequential-diagrams open import synthetic-homotopy-theory.functoriality-sequential-colimits open import synthetic-homotopy-theory.morphisms-sequential-diagrams open import synthetic-homotopy-theory.sequential-diagrams open import synthetic-homotopy-theory.shifts-sequential-diagrams open import synthetic-homotopy-theory.universal-property-sequential-colimits
Idea
A
zigzag¶
between sequential diagrams
(A, a) and (B, b) is a pair of families of maps
fₙ : Aₙ → Bₙ
gₙ : Bₙ → Aₙ₊₁
and coherences between them, such that they fit in the following diagram:
a₀ a₁
A₀ -----> A₁ -----> A₂ -----> ⋯
\ ∧ \ ∧
\ / \ f₁ /
f₀ \ / g₀ \ / g₁
∨ / ∨ /
B₀ -----> B₁ -----> ⋯ .
b₀
Given colimits X of A
and Y of B, the zigzag induces maps f∞ : X → Y and g∞ : Y → X, which we
show to be mutually inverse equivalences.
Definitions
A zigzag between sequential diagrams
module _ {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2) where module _ (f : (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n) (g : (n : ℕ) → family-sequential-diagram B n → family-sequential-diagram A (succ-ℕ n)) where coherence-upper-triangle-zigzag-sequential-diagram : UU l1 coherence-upper-triangle-zigzag-sequential-diagram = (n : ℕ) → coherence-triangle-maps ( map-sequential-diagram A n) ( g n) ( f n) coherence-lower-triangle-zigzag-sequential-diagram : UU l2 coherence-lower-triangle-zigzag-sequential-diagram = (n : ℕ) → coherence-triangle-maps ( map-sequential-diagram B n) ( f (succ-ℕ n)) ( g n) zigzag-sequential-diagram : UU (l1 ⊔ l2) zigzag-sequential-diagram = Σ ( (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n) ( λ f → Σ ( (n : ℕ) → family-sequential-diagram B n → family-sequential-diagram A (succ-ℕ n)) ( λ g → coherence-upper-triangle-zigzag-sequential-diagram f g × coherence-lower-triangle-zigzag-sequential-diagram f g))
Components of a zigzag of sequential diagrams
module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B) where map-zigzag-sequential-diagram : (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n map-zigzag-sequential-diagram = pr1 z inv-map-zigzag-sequential-diagram : (n : ℕ) → family-sequential-diagram B n → family-sequential-diagram A (succ-ℕ n) inv-map-zigzag-sequential-diagram = pr1 (pr2 z) upper-triangle-zigzag-sequential-diagram : coherence-upper-triangle-zigzag-sequential-diagram A B ( map-zigzag-sequential-diagram) ( inv-map-zigzag-sequential-diagram) upper-triangle-zigzag-sequential-diagram = pr1 (pr2 (pr2 z)) lower-triangle-zigzag-sequential-diagram : coherence-lower-triangle-zigzag-sequential-diagram A B ( map-zigzag-sequential-diagram) ( inv-map-zigzag-sequential-diagram) lower-triangle-zigzag-sequential-diagram = pr2 (pr2 (pr2 z))
Half-shifts of zigzags of sequential diagrams
We can forget the first triangle of a zigzag between (A, a) and (B, b) to
get a zigzag between (B, b) and the
shift (A[1], a[1])
b₀ b₁
B₀ -----> B₁ -----> B₂ -----> ⋯
\ ∧ \ ∧
\ / \ g₁ /
g₀ \ / f₁ \ / f₂
∨ / ∨ /
A₁ -----> A₂ -----> ⋯ .
a₁
We call this a half-shift of the original zigzag, and it provides a symmetry
between the downward-going f maps and upward-going g maps. We exploit this
symmetry in the proceeding constructions by formulating the definitions and
lemmas for the downwards directions, and then applying them to the half-shift of
a zigzag to get the constructions for the upward direction.
Repeating a half-shift twice gets us a shift of a zigzag.
module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B) where half-shift-zigzag-sequential-diagram : zigzag-sequential-diagram B (shift-once-sequential-diagram A) pr1 half-shift-zigzag-sequential-diagram = inv-map-zigzag-sequential-diagram z pr1 (pr2 half-shift-zigzag-sequential-diagram) n = map-zigzag-sequential-diagram z (succ-ℕ n) pr1 (pr2 (pr2 half-shift-zigzag-sequential-diagram)) = lower-triangle-zigzag-sequential-diagram z pr2 (pr2 (pr2 half-shift-zigzag-sequential-diagram)) n = upper-triangle-zigzag-sequential-diagram z (succ-ℕ n) module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B) where shift-zigzag-sequential-diagram : zigzag-sequential-diagram ( shift-once-sequential-diagram A) ( shift-once-sequential-diagram B) shift-zigzag-sequential-diagram = half-shift-zigzag-sequential-diagram ( half-shift-zigzag-sequential-diagram z)
Morphisms of sequential diagrams induced by zigzags of sequential diagrams
We can realign a zigzag
a₀ a₁
A₀ -----> A₁ -----> A₂ -----> ⋯
\ ∧ \ ∧
\ / \ f₁ /
f₀ \ / g₀ \ / g₁
∨ / ∨ /
B₀ -----> B₁ -----> ⋯
b₀
into a morphism
f : A → B
a₀ a₁
A₀ -----> A₁ -----> A₂ -----> ⋯
| ∧| ∧|
f₀ | g₀ / | f₁ / | f₂
| / | / g₁ |
∨ / ∨ / ∨
B₀ -----> B₁ -----> B₂ -----> ⋯ .
b₀ b₁
Similarly, we can realign the half-shift of a zigzag to get the morphism
g : B → A[1]:
b₀ b₁
B₀ -----> B₁ -----> B₂ -----> ⋯
| ∧| ∧|
g₀ | f₁ / | g₁ / | g₂
| / | / f₂ |
∨ / ∨ / ∨
A₁ -----> A₂ -----> A₃ -----> ⋯ ,
a₁ a₂
which should be thought of as an inverse of f — and we show that it indeed
induces an inverse in the colimit further down.
module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B) where hom-diagram-zigzag-sequential-diagram : hom-sequential-diagram A B pr1 hom-diagram-zigzag-sequential-diagram = map-zigzag-sequential-diagram z pr2 hom-diagram-zigzag-sequential-diagram n = horizontal-pasting-up-diagonal-coherence-triangle-maps ( map-sequential-diagram A n) ( map-zigzag-sequential-diagram z n) ( map-zigzag-sequential-diagram z (succ-ℕ n)) ( map-sequential-diagram B n) ( inv-htpy (upper-triangle-zigzag-sequential-diagram z n)) ( lower-triangle-zigzag-sequential-diagram z n) module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B) where inv-hom-diagram-zigzag-sequential-diagram : hom-sequential-diagram B (shift-once-sequential-diagram A) inv-hom-diagram-zigzag-sequential-diagram = hom-diagram-zigzag-sequential-diagram ( half-shift-zigzag-sequential-diagram z)
Zigzags of sequential diagrams unfold to the shifting morphism of sequential diagrams
After composing the morphisms induced by a zigzag, we get a morphism
g ∘ f : A → A[1]
a₀ a₁
A₀ -----> A₁ -----> A₂ -----> ⋯
| ∧| ∧|
f₀ | g₀ / | f₁ / | f₂
| / | / g₁ |
∨ / b₀ ∨ / b₁ ∨
B₀ -----> B₁ -----> B₂ -----> ⋯
| ∧| ∧|
g₀ | f₁ / | g₁ / | g₂
| / | / f₂ |
∨ / ∨ / ∨
A₁ -----> A₂ -----> A₃ -----> ⋯ .
a₁ a₂
We show that there is a
homotopy between
this morphism and the
shift inclusion morphism
a : A → A[1]
a₀ a₁
A₀ ---> A₁ ---> A₂ ---> ⋯
| | |
a₀ | | a₁ | a₂
∨ ∨ ∨
A₁ ---> A₂ ---> A₃ ---> ⋯ .
a₁ a₂
Proof: Component-wise the homotopies aₙ ~ gₙ ∘ fₙ are given by the upper
triangles in the zigzag. The coherence of a homotopy requires us to show that
the compositions
aₙ
Aₙ ----> Aₙ₊₁
| \ fₙ₊₁
| ∨
aₙ₊₁ | Bₙ₊₁
| /
∨ ∨ gₙ₊₁
Aₙ₊₂
and
aₙ
Aₙ -----> Aₙ₊₁
/ | ∧|
/ fₙ | gₙ / | fₙ₊₁
| | / |
| ∨ / ∨
aₙ | Bₙ -----> Bₙ₊₁
| | ∧|
| gₙ | fₙ₊₁ / | gₙ₊₁
\ | / |
∨ ∨ / ∨
Aₙ₊₁ ---> Aₙ₊₂
aₙ₊₁
are homotopic. Since the skewed square
gₙ
Bₙ -----> Aₙ₊₁
| |
gₙ | | fₙ₊₁
∨ ∨
Aₙ₊₁ ---> Bₙ₊₁
fₙ₊₁
in the middle is composed of inverse triangles, it is homotopic to the reflexivity homotopy, which makes the second diagram collapse to
aₙ
--------
/ \
/ ∨
Aₙ ----> Bₙ ----> Aₙ₊₁
\ fₙ gₙ ∧ | \ fₙ₊₁
\ / | ∨
-------- | aₙ₊₁ Bₙ₊₁
aₙ | /
∨ ∨ gₙ₊₁
Aₙ₊₂ ,
where the globe is again composed of inverse triangles, so the diagram collapses to
aₙ
Aₙ ----> Aₙ₊₁
| \ fₙ₊₁
| ∨
aₙ₊₁ | Bₙ₊₁
| /
∨ ∨ gₙ₊₁
Aₙ₊₂ ,
which is what we needed to show.
module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B) where htpy-hom-shift-hom-zigzag-sequential-diagram : htpy-hom-sequential-diagram ( shift-once-sequential-diagram A) ( hom-shift-once-sequential-diagram A) ( comp-hom-sequential-diagram A B ( shift-once-sequential-diagram A) ( inv-hom-diagram-zigzag-sequential-diagram z) ( hom-diagram-zigzag-sequential-diagram z)) pr1 htpy-hom-shift-hom-zigzag-sequential-diagram = upper-triangle-zigzag-sequential-diagram z pr2 htpy-hom-shift-hom-zigzag-sequential-diagram n = inv-concat-right-homotopy-coherence-square-homotopies ( ( map-sequential-diagram A (succ-ℕ n)) ·l ( upper-triangle-zigzag-sequential-diagram z n)) ( refl-htpy) ( naturality-comp-hom-sequential-diagram A B ( shift-once-sequential-diagram A) ( inv-hom-diagram-zigzag-sequential-diagram z) ( hom-diagram-zigzag-sequential-diagram z) ( n)) ( ( upper-triangle-zigzag-sequential-diagram z (succ-ℕ n)) ·r ( map-sequential-diagram A n)) ( pasting-coherence-squares-collapse-triangles ( map-sequential-diagram A n) ( map-zigzag-sequential-diagram z n) ( map-zigzag-sequential-diagram z (succ-ℕ n)) ( map-sequential-diagram B n) ( inv-map-zigzag-sequential-diagram z n) ( inv-map-zigzag-sequential-diagram z (succ-ℕ n)) ( map-sequential-diagram A (succ-ℕ n)) ( inv-htpy (upper-triangle-zigzag-sequential-diagram z n)) ( lower-triangle-zigzag-sequential-diagram z n) ( inv-htpy (lower-triangle-zigzag-sequential-diagram z n)) ( upper-triangle-zigzag-sequential-diagram z (succ-ℕ n)) ( left-inv-htpy (lower-triangle-zigzag-sequential-diagram z n))) ( right-whisker-concat-coherence-square-homotopies ( ( map-sequential-diagram A (succ-ℕ n)) ·l ( upper-triangle-zigzag-sequential-diagram z n)) ( refl-htpy) ( ( map-sequential-diagram A (succ-ℕ n)) ·l ( inv-htpy (upper-triangle-zigzag-sequential-diagram z n))) ( refl-htpy) ( inv-htpy ( right-inv-htpy-left-whisker ( map-sequential-diagram A (succ-ℕ n)) ( upper-triangle-zigzag-sequential-diagram z n))) ( ( upper-triangle-zigzag-sequential-diagram z (succ-ℕ n)) ·r ( map-sequential-diagram A n)))
Properties
Zigzags of sequential diagrams induce equivalences of sequential colimits
By
functoriality
of sequential colimits, the morphism f : A → B induced by a zigzag then
induces a map of colimits A∞ → B∞. We show that this induced map is an
equivalence.
Proof: Given a colimit X of (A, a) and a colimit Y of (B, b), we get
a map f∞ : X → Y. Since X is also a colimit of (A[1], a[1]), the morphism
g : B → A[1] induces a map g∞ : Y → X. Composing the two, we get
g∞ ∘ f∞ : X → X. By functoriality, this map is homotopic to (g ∘ f)∞, and
taking a colimit preserves homotopies, so g ∘ f ~ a implies (g ∘ f)∞ ~ a∞.
In
shifts-sequential-diagrams
we show that a∞ ~ id, so we get a commuting triangle
id
X ---> X
| ∧
f∞ | / g∞
∨ /
Y .
Applying this construction to the half-shift of the zigzag, we get a commuting triangle
id
Y ---> Y
| ∧
g∞ | / f[1]∞
∨ /
X .
These triangles compose to the commuting square
id
X -----> X
| ∧|
f∞ | g∞ / | f[1]∞
| / |
∨ / ∨
Y -----> Y .
id
Since the horizontal maps are identities, we get that g∞ is by definition an
equivalence, because we just presented its section f∞ and its retraction
f[1]∞. Since f∞ is a section of an equivalence, it is itself an equivalence.
Additionally we get the judgmental equalities f∞⁻¹ ≐ g∞ and g∞⁻¹ ≐ f∞.
module _ {l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} {X : UU l3} {c : cocone-sequential-diagram A X} (up-c : universal-property-sequential-colimit c) {Y : UU l4} {c' : cocone-sequential-diagram B Y} (up-c' : universal-property-sequential-colimit c') (z : zigzag-sequential-diagram A B) where map-colimit-zigzag-sequential-diagram : X → Y map-colimit-zigzag-sequential-diagram = map-sequential-colimit-hom-sequential-diagram ( up-c) ( c') ( hom-diagram-zigzag-sequential-diagram z) inv-map-colimit-zigzag-sequential-diagram : Y → X inv-map-colimit-zigzag-sequential-diagram = map-sequential-colimit-hom-sequential-diagram ( up-c') ( shift-once-cocone-sequential-diagram c) ( inv-hom-diagram-zigzag-sequential-diagram z) upper-triangle-colimit-zigzag-sequential-diagram : coherence-triangle-maps ( id) ( inv-map-colimit-zigzag-sequential-diagram) ( map-colimit-zigzag-sequential-diagram) upper-triangle-colimit-zigzag-sequential-diagram = ( inv-htpy (compute-map-colimit-hom-shift-once-sequential-diagram up-c)) ∙h ( htpy-map-sequential-colimit-htpy-hom-sequential-diagram up-c ( shift-once-cocone-sequential-diagram c) ( htpy-hom-shift-hom-zigzag-sequential-diagram z)) ∙h ( preserves-comp-map-sequential-colimit-hom-sequential-diagram ( up-c) ( up-c') ( shift-once-cocone-sequential-diagram c) ( inv-hom-diagram-zigzag-sequential-diagram z) ( hom-diagram-zigzag-sequential-diagram z)) is-retraction-inv-map-colimit-zigzag-sequential-diagram : is-retraction ( map-colimit-zigzag-sequential-diagram) ( inv-map-colimit-zigzag-sequential-diagram) is-retraction-inv-map-colimit-zigzag-sequential-diagram = inv-htpy upper-triangle-colimit-zigzag-sequential-diagram module _ {l1 l2 l3 l4 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2) {X : UU l3} {c : cocone-sequential-diagram A X} (up-c : universal-property-sequential-colimit c) {Y : UU l4} {c' : cocone-sequential-diagram B Y} (up-c' : universal-property-sequential-colimit c') (z : zigzag-sequential-diagram A B) where lower-triangle-colimit-zigzag-sequential-diagram : coherence-triangle-maps ( id) ( map-colimit-zigzag-sequential-diagram ( up-shift-cocone-sequential-diagram 1 up-c) ( up-shift-cocone-sequential-diagram 1 up-c') ( shift-zigzag-sequential-diagram z)) ( map-colimit-zigzag-sequential-diagram up-c' ( up-shift-cocone-sequential-diagram 1 up-c) ( half-shift-zigzag-sequential-diagram z)) lower-triangle-colimit-zigzag-sequential-diagram = upper-triangle-colimit-zigzag-sequential-diagram ( up-c') ( up-shift-cocone-sequential-diagram 1 up-c) ( half-shift-zigzag-sequential-diagram z) is-equiv-inv-map-colimit-zigzag-sequential-diagram : is-equiv (inv-map-colimit-zigzag-sequential-diagram up-c up-c' z) pr1 is-equiv-inv-map-colimit-zigzag-sequential-diagram = ( map-colimit-zigzag-sequential-diagram up-c up-c' z) , ( is-retraction-inv-map-colimit-zigzag-sequential-diagram up-c up-c' z) pr2 is-equiv-inv-map-colimit-zigzag-sequential-diagram = ( map-colimit-zigzag-sequential-diagram ( up-shift-cocone-sequential-diagram 1 up-c) ( up-shift-cocone-sequential-diagram 1 up-c') ( shift-zigzag-sequential-diagram z)) , ( is-retraction-inv-map-colimit-zigzag-sequential-diagram ( up-c') ( up-shift-cocone-sequential-diagram 1 up-c) ( half-shift-zigzag-sequential-diagram z)) inv-equiv-colimit-zigzag-sequential-diagram : Y ≃ X pr1 inv-equiv-colimit-zigzag-sequential-diagram = inv-map-colimit-zigzag-sequential-diagram up-c up-c' z pr2 inv-equiv-colimit-zigzag-sequential-diagram = is-equiv-inv-map-colimit-zigzag-sequential-diagram equiv-colimit-zigzag-sequential-diagram : X ≃ Y pr1 equiv-colimit-zigzag-sequential-diagram = map-colimit-zigzag-sequential-diagram up-c up-c' z pr2 equiv-colimit-zigzag-sequential-diagram = is-equiv-map-inv-equiv inv-equiv-colimit-zigzag-sequential-diagram
Recent changes
- 2024-05-23. Vojtěch Štěpančík. Zigzags of sequential diagrams (#1129).