The Mayer–Vietoris sequence of a pushout of simplicial sets #
Consider a commutative square of simplicial sets
t
X₁ ⟶ X₂
l| |r
v v
X₃ ⟶ X₄
b
and an object R of an abelian category with coproducts. Its Mayer–Vietoris short complex of
chain complexes is C(X₁; R) ⟶ C(X₂; R) ⊞ C(X₃; R) ⟶ C(X₄; R), with first map (t, -l) and
second map r + b. When the square is a pushout and t is a monomorphism, this short complex is
short exact: the chain complex functor preserves pushouts, and a pushout square in an abelian
category is right exact in this form. The homology sequence of this short exact sequence is the
Mayer–Vietoris long exact sequence
⋯ ⟶ Hₙ(X₁) ⟶ Hₙ(X₂) ⊞ Hₙ(X₃) ⟶ Hₙ(X₄) ⟶ Hₙ₋₁(X₁) ⟶ ⋯,
whose first two maps are (t_*, -l_*) and r_* + b_*.
The typical pushout square is that of two subcomplexes A and B of a simplicial set, their
intersection and their union (SSet.Subcomplex.BicartSq.isPushout). The Mayer–Vietoris sequence
of singular homology for an open cover by two sets is obtained from such a square.
Main definitions and results #
SSet.shortExact_mayerVietorisShortComplex: it is short exact for a pushout square whose top map is a monomorphism.SSet.mayerVietorisToBiprod,SSet.mayerVietorisFromBiprod: the mapsHₙ(X₁) ⟶ Hₙ(X₂) ⊞ Hₙ(X₃)andHₙ(X₂) ⊞ Hₙ(X₃) ⟶ Hₙ(X₄).SSet.mayerVietorisδ: the connecting morphismHₙ(X₄) ⟶ Hₘ(X₁)form + 1 = n.SSet.mayerVietoris_exact₁,SSet.mayerVietoris_exact₂,SSet.mayerVietoris_exact₃: exactness atHₘ(X₁), atHₙ(X₂) ⊞ Hₙ(X₃)and atHₙ(X₄).SSet.epi_mayerVietorisFromBiprod_zero: surjectivity at the degree-zero endpoint.SSet.mayerVietorisδ_naturality: the connecting morphism is natural in maps of pushout squares.
References #
- A. Hatcher, Algebraic Topology, Section 2.2, the Mayer–Vietoris sequences.
theorem
SSet.shortExact_mayerVietorisShortComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
:
The Mayer–Vietoris short exact sequence of chain complexes. For a pushout square of simplicial sets whose top map is a monomorphism, the Mayer–Vietoris short complex is short exact.
The long exact sequence #
noncomputable def
SSet.mayerVietorisToBiprod
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
(t : X₁ ⟶ X₂)
(l : X₁ ⟶ X₃)
(n : ℕ)
:
The first map Hₙ(X₁) ⟶ Hₙ(X₂) ⊞ Hₙ(X₃) of the Mayer–Vietoris sequence, with components
t_* and -l_*.
Equations
- SSet.mayerVietorisToBiprod R t l n = CategoryTheory.Limits.biprod.lift (SSet.homologyMap t R n) (-SSet.homologyMap l R n)
Instances For
@[simp]
theorem
SSet.mayerVietorisToBiprod_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
(t : X₁ ⟶ X₂)
(l : X₁ ⟶ X₃)
(n : ℕ)
:
@[simp]
theorem
SSet.mayerVietorisToBiprod_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
(t : X₁ ⟶ X₂)
(l : X₁ ⟶ X₃)
(n : ℕ)
{Z : C}
(h : X₂.homology R n ⟶ Z)
:
@[simp]
theorem
SSet.mayerVietorisToBiprod_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
(t : X₁ ⟶ X₂)
(l : X₁ ⟶ X₃)
(n : ℕ)
:
@[simp]
theorem
SSet.mayerVietorisToBiprod_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
(t : X₁ ⟶ X₂)
(l : X₁ ⟶ X₃)
(n : ℕ)
{Z : C}
(h : X₃.homology R n ⟶ Z)
:
noncomputable def
SSet.mayerVietorisFromBiprod
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
(r : X₂ ⟶ X₄)
(b : X₃ ⟶ X₄)
(n : ℕ)
:
The second map Hₙ(X₂) ⊞ Hₙ(X₃) ⟶ Hₙ(X₄) of the Mayer–Vietoris sequence, the sum of r_*
and b_*.
Equations
- SSet.mayerVietorisFromBiprod R r b n = CategoryTheory.Limits.biprod.desc (SSet.homologyMap r R n) (SSet.homologyMap b R n)
Instances For
@[simp]
theorem
SSet.inl_mayerVietorisFromBiprod
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
(r : X₂ ⟶ X₄)
(b : X₃ ⟶ X₄)
(n : ℕ)
:
@[simp]
theorem
SSet.inl_mayerVietorisFromBiprod_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
(r : X₂ ⟶ X₄)
(b : X₃ ⟶ X₄)
(n : ℕ)
{Z : C}
(h : X₄.homology R n ⟶ Z)
:
@[simp]
theorem
SSet.inr_mayerVietorisFromBiprod
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
(r : X₂ ⟶ X₄)
(b : X₃ ⟶ X₄)
(n : ℕ)
:
@[simp]
theorem
SSet.inr_mayerVietorisFromBiprod_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
(r : X₂ ⟶ X₄)
(b : X₃ ⟶ X₄)
(n : ℕ)
{Z : C}
(h : X₄.homology R n ⟶ Z)
:
@[simp]
theorem
SSet.mayerVietorisToBiprod_fromBiprod
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.CommSq t l r b)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) (mayerVietorisFromBiprod R r b n) = 0
@[simp]
theorem
SSet.mayerVietorisToBiprod_fromBiprod_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.CommSq t l r b)
(n : ℕ)
{Z : C}
(h : X₄.homology R n ⟶ Z)
:
theorem
SSet.mayerVietorisToBiprod_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{Y₁ Y₂ Y₃ : SSet}
{t' : Y₁ ⟶ Y₂}
{l' : Y₁ ⟶ Y₃}
(φ₁ : X₁ ⟶ Y₁)
(φ₂ : X₂ ⟶ Y₂)
(φ₃ : X₃ ⟶ Y₃)
(ht : CategoryTheory.CategoryStruct.comp t φ₂ = CategoryTheory.CategoryStruct.comp φ₁ t')
(hl : CategoryTheory.CategoryStruct.comp l φ₃ = CategoryTheory.CategoryStruct.comp φ₁ l')
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n)
(CategoryTheory.Limits.biprod.map (SSet.homologyMap φ₂ R n) (SSet.homologyMap φ₃ R n)) = CategoryTheory.CategoryStruct.comp (SSet.homologyMap φ₁ R n) (mayerVietorisToBiprod R t' l' n)
The first map of the Mayer–Vietoris sequence is natural in maps of squares.
theorem
SSet.mayerVietorisToBiprod_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{Y₁ Y₂ Y₃ : SSet}
{t' : Y₁ ⟶ Y₂}
{l' : Y₁ ⟶ Y₃}
(φ₁ : X₁ ⟶ Y₁)
(φ₂ : X₂ ⟶ Y₂)
(φ₃ : X₃ ⟶ Y₃)
(ht : CategoryTheory.CategoryStruct.comp t φ₂ = CategoryTheory.CategoryStruct.comp φ₁ t')
(hl : CategoryTheory.CategoryStruct.comp l φ₃ = CategoryTheory.CategoryStruct.comp φ₁ l')
(n : ℕ)
{Z : C}
(h : Y₂.homology R n ⊞ Y₃.homology R n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biprod.map (SSet.homologyMap φ₂ R n) (SSet.homologyMap φ₃ R n)) h) = CategoryTheory.CategoryStruct.comp (SSet.homologyMap φ₁ R n)
(CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t' l' n) h)
The first map of the Mayer–Vietoris sequence is natural in maps of squares.
theorem
SSet.mayerVietorisFromBiprod_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
{Y₂ Y₃ Y₄ : SSet}
{r' : Y₂ ⟶ Y₄}
{b' : Y₃ ⟶ Y₄}
(φ₂ : X₂ ⟶ Y₂)
(φ₃ : X₃ ⟶ Y₃)
(φ₄ : X₄ ⟶ Y₄)
(hr : CategoryTheory.CategoryStruct.comp r φ₄ = CategoryTheory.CategoryStruct.comp φ₂ r')
(hb : CategoryTheory.CategoryStruct.comp b φ₄ = CategoryTheory.CategoryStruct.comp φ₃ b')
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) (SSet.homologyMap φ₄ R n) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biprod.map (SSet.homologyMap φ₂ R n) (SSet.homologyMap φ₃ R n))
(mayerVietorisFromBiprod R r' b' n)
The second map of the Mayer–Vietoris sequence is natural in maps of squares.
theorem
SSet.mayerVietorisFromBiprod_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₂ X₃ X₄ : SSet}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
{Y₂ Y₃ Y₄ : SSet}
{r' : Y₂ ⟶ Y₄}
{b' : Y₃ ⟶ Y₄}
(φ₂ : X₂ ⟶ Y₂)
(φ₃ : X₃ ⟶ Y₃)
(φ₄ : X₄ ⟶ Y₄)
(hr : CategoryTheory.CategoryStruct.comp r φ₄ = CategoryTheory.CategoryStruct.comp φ₂ r')
(hb : CategoryTheory.CategoryStruct.comp b φ₄ = CategoryTheory.CategoryStruct.comp φ₃ b')
(n : ℕ)
{Z : C}
(h : Y₄.homology R n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n)
(CategoryTheory.CategoryStruct.comp (SSet.homologyMap φ₄ R n) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biprod.map (SSet.homologyMap φ₂ R n) (SSet.homologyMap φ₃ R n))
(CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r' b' n) h)
The second map of the Mayer–Vietoris sequence is natural in maps of squares.
noncomputable def
SSet.mayerVietorisδ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
:
The Mayer–Vietoris connecting morphism Hₙ(X₄) ⟶ Hₘ(X₁), where m + 1 = n: the connecting
morphism of the Mayer–Vietoris short exact sequence of chain complexes.
Equations
- SSet.mayerVietorisδ R sq n m h = ⋯.δ n m h
Instances For
theorem
SSet.mayerVietorisδ_def
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
:
@[simp]
theorem
SSet.mayerVietorisδ_toBiprod
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
:
@[simp]
theorem
SSet.mayerVietorisδ_toBiprod_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
{Z : C}
(h✝ : X₂.homology R m ⊞ X₃.homology R m ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sq n m h)
(CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
@[simp]
theorem
SSet.mayerVietorisFromBiprod_δ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) (mayerVietorisδ R sq n m h) = 0
@[simp]
theorem
SSet.mayerVietorisFromBiprod_δ_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
{Z : C}
(h✝ : X₁.homology R m ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n)
(CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sq n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
theorem
SSet.mayerVietoris_exact₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
:
{ X₁ := X₄.homology R n, X₂ := X₁.homology R m, X₃ := X₂.homology R m ⊞ X₃.homology R m, f := mayerVietorisδ R sq n m h,
g := mayerVietorisToBiprod R t l m, zero := ⋯ }.Exact
Exactness of the Mayer–Vietoris sequence at Hₘ(X₁).
theorem
SSet.mayerVietoris_exact₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n : ℕ)
:
{ X₁ := X₁.homology R n, X₂ := X₂.homology R n ⊞ X₃.homology R n, X₃ := X₄.homology R n,
f := mayerVietorisToBiprod R t l n, g := mayerVietorisFromBiprod R r b n, zero := ⋯ }.Exact
Exactness of the Mayer–Vietoris sequence at Hₙ(X₂) ⊞ Hₙ(X₃).
theorem
SSet.mayerVietoris_exact₃
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(n m : ℕ)
(h : m + 1 = n := by lia)
:
{ X₁ := X₂.homology R n ⊞ X₃.homology R n, X₂ := X₄.homology R n, X₃ := X₁.homology R m,
f := mayerVietorisFromBiprod R r b n, g := mayerVietorisδ R sq n m h, zero := ⋯ }.Exact
Exactness of the Mayer–Vietoris sequence at Hₙ(X₄).
theorem
SSet.epi_mayerVietorisFromBiprod_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
:
CategoryTheory.Epi (mayerVietorisFromBiprod R r b 0)
The map H₀(X₂) ⊞ H₀(X₃) ⟶ H₀(X₄) at the end of the Mayer–Vietoris sequence is an
epimorphism.
theorem
SSet.mayerVietorisδ_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
{Y₁ Y₂ Y₃ Y₄ : SSet}
{t' : Y₁ ⟶ Y₂}
{l' : Y₁ ⟶ Y₃}
{r' : Y₂ ⟶ Y₄}
{b' : Y₃ ⟶ Y₄}
(φ₁ : X₁ ⟶ Y₁)
(φ₂ : X₂ ⟶ Y₂)
(φ₃ : X₃ ⟶ Y₃)
(φ₄ : X₄ ⟶ Y₄)
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(sq' : CategoryTheory.IsPushout t' l' r' b')
[CategoryTheory.Mono t']
(ht : CategoryTheory.CategoryStruct.comp t φ₂ = CategoryTheory.CategoryStruct.comp φ₁ t')
(hl : CategoryTheory.CategoryStruct.comp l φ₃ = CategoryTheory.CategoryStruct.comp φ₁ l')
(hr : CategoryTheory.CategoryStruct.comp r φ₄ = CategoryTheory.CategoryStruct.comp φ₂ r')
(hb : CategoryTheory.CategoryStruct.comp b φ₄ = CategoryTheory.CategoryStruct.comp φ₃ b')
(n m : ℕ)
(h : m + 1 = n := by lia)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sq n m h) (SSet.homologyMap φ₁ R m) = CategoryTheory.CategoryStruct.comp (SSet.homologyMap φ₄ R n) (mayerVietorisδ R sq' n m h)
Naturality of the Mayer–Vietoris connecting morphism in maps of pushout squares.
theorem
SSet.mayerVietorisδ_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C]
(R : C)
{X₁ X₂ X₃ X₄ : SSet}
{t : X₁ ⟶ X₂}
{l : X₁ ⟶ X₃}
{r : X₂ ⟶ X₄}
{b : X₃ ⟶ X₄}
{Y₁ Y₂ Y₃ Y₄ : SSet}
{t' : Y₁ ⟶ Y₂}
{l' : Y₁ ⟶ Y₃}
{r' : Y₂ ⟶ Y₄}
{b' : Y₃ ⟶ Y₄}
(φ₁ : X₁ ⟶ Y₁)
(φ₂ : X₂ ⟶ Y₂)
(φ₃ : X₃ ⟶ Y₃)
(φ₄ : X₄ ⟶ Y₄)
(sq : CategoryTheory.IsPushout t l r b)
[CategoryTheory.Mono t]
(sq' : CategoryTheory.IsPushout t' l' r' b')
[CategoryTheory.Mono t']
(ht : CategoryTheory.CategoryStruct.comp t φ₂ = CategoryTheory.CategoryStruct.comp φ₁ t')
(hl : CategoryTheory.CategoryStruct.comp l φ₃ = CategoryTheory.CategoryStruct.comp φ₁ l')
(hr : CategoryTheory.CategoryStruct.comp r φ₄ = CategoryTheory.CategoryStruct.comp φ₂ r')
(hb : CategoryTheory.CategoryStruct.comp b φ₄ = CategoryTheory.CategoryStruct.comp φ₃ b')
(n m : ℕ)
(h : m + 1 = n := by lia)
{Z : C}
(h✝ : Y₁.homology R m ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sq n m h)
(CategoryTheory.CategoryStruct.comp (SSet.homologyMap φ₁ R m) h✝) = CategoryTheory.CategoryStruct.comp (SSet.homologyMap φ₄ R n)
(CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sq' n m h) h✝)
Naturality of the Mayer–Vietoris connecting morphism in maps of pushout squares.