The relative Mayer–Vietoris sequence of a square of pairs of simplicial sets

Consider a commutative square of pairs of simplicial sets

     t
 P₁  ⟶  P₂
l|       |r
 v       v
 P₃  ⟶  P₄
     b

whose square of subobjects and square of ambient simplicial sets are both pushouts with monomorphic top maps, and let R be an object of an abelian category with coproducts. The relative Mayer–Vietoris short complex C(P₁; R) ⟶ C(P₂; R) ⊞ C(P₃; R) ⟶ C(P₄; R) of relative chain complexes, with first map (t, -l) and second map r + b, is then short exact (SSetPair.shortExact_mayerVietoris). Its homology sequence is the relative Mayer–Vietoris long exact sequence ⋯ ⟶ Hₙ(P₁) ⟶ Hₙ(P₂) ⊞ Hₙ(P₃) ⟶ Hₙ(P₄) ⟶ Hₙ₋₁(P₁) ⟶ ⋯.

The relative chains of a pair are the cokernel of the chains of its subobject in those of its ambient simplicial set, so the relative short complex is the cokernel of the morphism from the absolute Mayer–Vietoris short exact sequence of the subobjects to that of the ambient simplicial sets. The ambient component of that morphism in the last term is a monomorphism, so the snake lemma (CategoryTheory.ShortComplex.ShortExact.of_isColimit_cokernelCofork) shows that the cokernel is short exact.

In the typical instance the four ambient simplicial sets are one simplicial set K with identity maps between them, and the subobjects are the intersection, the two members and the union of two subcomplexes of K. For the singular simplicial set of a space X and the singular simplices of open sets U ∩ V, U, V and of U or V, the small-chain theorem turns this into the sequence ⋯ ⟶ Hₙ(X, U ∩ V) ⟶ Hₙ(X, U) ⊞ Hₙ(X, V) ⟶ Hₙ(X, U ∪ V) ⟶ ⋯ (TopCat.relativeMayerVietorisδ).

Main definitions and results

• SSetPair.shortExact_mayerVietoris: the relative Mayer–Vietoris short complex is short exact.
• SSetPair.isSplitEpi_mayerVietoris_g_f: in each degree its last map is a split epimorphism.
• SSetPair.mayerVietorisToBiprod, SSetPair.mayerVietorisFromBiprod: the maps Hₙ(P₁) ⟶ Hₙ(P₂) ⊞ Hₙ(P₃) and Hₙ(P₂) ⊞ Hₙ(P₃) ⟶ Hₙ(P₄).
• SSetPair.mayerVietorisδ: the connecting morphism Hₙ(P₄) ⟶ Hₘ(P₁) for m + 1 = n.
• SSetPair.mayerVietoris_exact₁, SSetPair.mayerVietoris_exact₂, SSetPair.mayerVietoris_exact₃: exactness at Hₘ(P₁), at Hₙ(P₂) ⊞ Hₙ(P₃) and at Hₙ(P₄).
• SSetPair.epi_mayerVietorisFromBiprod_zero: surjectivity at the degree-zero endpoint.
• SSetPair.mayerVietorisToBiprod_naturality, SSetPair.mayerVietorisFromBiprod_naturality, SSetPair.mayerVietorisδ_naturality: the maps of the sequence are natural in maps of squares of pairs.

References

• A. Hatcher, Algebraic Topology, Section 2.2, the relative Mayer–Vietoris sequence.

The short exact sequence of relative chain complexes

theorem SSetPair.mayerVietoris_chainComplex_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} (t : P₁ ⟶ P₂) (l : P₁ ⟶ P₃) (r : P₂ ⟶ P₄) (b : P₃ ⟶ P₄) (w : CategoryTheory.CategoryStruct.comp t r = CategoryTheory.CategoryStruct.comp l b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (chainComplexMap t R) (-chainComplexMap l R)) (CategoryTheory.Limits.biprod.desc (chainComplexMap r R) (chainComplexMap b R)) = 0

The first map C(P₁) ⟶ C(P₂) ⊞ C(P₃) of relative chains followed by the second map C(P₂) ⊞ C(P₃) ⟶ C(P₄) vanishes for a commutative square of pairs.

theorem SSetPair.shortExact_mayerVietoris {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] : { X₁ := P₁.chainComplex R, X₂ := P₂.chainComplex R ⊞ P₃.chainComplex R, X₃ := P₄.chainComplex R, f := CategoryTheory.Limits.biprod.lift (chainComplexMap t R) (-chainComplexMap l R), g := CategoryTheory.Limits.biprod.desc (chainComplexMap r R) (chainComplexMap b R), zero := ⋯ }.ShortExact

The relative Mayer–Vietoris short exact sequence. For a commutative square of pairs of simplicial sets whose squares of subobjects and of ambient simplicial sets are pushouts with monomorphic top maps, the relative chain complexes form a short exact sequence C(P₁) ⟶ C(P₂) ⊞ C(P₃) ⟶ C(P₄) with first map (t, -l) and second map r + b.

theorem SSetPair.isSplitEpi_mayerVietoris_g_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (i : ℕ) : CategoryTheory.IsSplitEpi ((CategoryTheory.Limits.biprod.desc (chainComplexMap r R) (chainComplexMap b R)).f i)

In each degree, the last map C(P₂) ⊞ C(P₃) ⟶ C(P₄) of the relative Mayer–Vietoris sequence of a square of pairs of simplicial sets is a split epimorphism, when the square of ambient simplicial sets is a pushout with monomorphic top map. A section is the composite of a section C(P₄) ⟶ C(P₄.right) of the quotient map from ambient to relative chains, a section of the absolute Mayer–Vietoris sequence of the ambient simplicial sets, and the quotient maps to relative chains.

The long exact sequence

noncomputable def SSetPair.mayerVietorisToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} (t : P₁ ⟶ P₂) (l : P₁ ⟶ P₃) (n : ℕ) : P₁.homology R n ⟶ P₂.homology R n ⊞ P₃.homology R n

The first map Hₙ(P₁) ⟶ Hₙ(P₂) ⊞ Hₙ(P₃) of the relative Mayer–Vietoris sequence, with components t_* and -l_*.

@[simp]

theorem SSetPair.mayerVietorisToBiprod_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) CategoryTheory.Limits.biprod.fst = SSetPair.homologyMap t R n

@[simp]

theorem SSetPair.mayerVietorisToBiprod_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) {Z : C} (h : P₂.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap t R n) h

@[simp]

theorem SSetPair.mayerVietorisToBiprod_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) CategoryTheory.Limits.biprod.snd = -SSetPair.homologyMap l R n

@[simp]

theorem SSetPair.mayerVietorisToBiprod_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) {Z : C} (h : P₃.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (-SSetPair.homologyMap l R n) h

noncomputable def SSetPair.mayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} (r : P₂ ⟶ P₄) (b : P₃ ⟶ P₄) (n : ℕ) : P₂.homology R n ⊞ P₃.homology R n ⟶ P₄.homology R n

The second map Hₙ(P₂) ⊞ Hₙ(P₃) ⟶ Hₙ(P₄) of the relative Mayer–Vietoris sequence, the sum of r_* and b_*.

@[simp]

theorem SSetPair.inl_mayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (mayerVietorisFromBiprod R r b n) = SSetPair.homologyMap r R n

@[simp]

theorem SSetPair.inl_mayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) {Z : C} (h : P₄.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) h) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap r R n) h

@[simp]

theorem SSetPair.inr_mayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (mayerVietorisFromBiprod R r b n) = SSetPair.homologyMap b R n

@[simp]

theorem SSetPair.inr_mayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) {Z : C} (h : P₄.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) h) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap b R n) h

@[simp]

theorem SSetPair.mayerVietorisToBiprod_fromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (w : CategoryTheory.CategoryStruct.comp t r = CategoryTheory.CategoryStruct.comp l b) (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) (mayerVietorisFromBiprod R r b n) = 0

@[simp]

theorem SSetPair.mayerVietorisToBiprod_fromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (w : CategoryTheory.CategoryStruct.comp t r = CategoryTheory.CategoryStruct.comp l b) (n : ℕ) {Z : C} (h : P₄.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) (CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem SSetPair.mayerVietorisToBiprod_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {Q₁ Q₂ Q₃ : SSetPair} {t' : Q₁ ⟶ Q₂} {l' : Q₁ ⟶ Q₃} (φ₁ : P₁ ⟶ Q₁) (φ₂ : P₂ ⟶ Q₂) (φ₃ : P₃ ⟶ Q₃) (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 (SSetPair.homologyMap φ₂ R n) (SSetPair.homologyMap φ₃ R n)) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap φ₁ R n) (mayerVietorisToBiprod R t' l' n)

The first map of the relative Mayer–Vietoris sequence is natural in maps of squares of pairs.

theorem SSetPair.mayerVietorisToBiprod_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {Q₁ Q₂ Q₃ : SSetPair} {t' : Q₁ ⟶ Q₂} {l' : Q₁ ⟶ Q₃} (φ₁ : P₁ ⟶ Q₁) (φ₂ : P₂ ⟶ Q₂) (φ₃ : P₃ ⟶ Q₃) (ht : CategoryTheory.CategoryStruct.comp t φ₂ = CategoryTheory.CategoryStruct.comp φ₁ t') (hl : CategoryTheory.CategoryStruct.comp l φ₃ = CategoryTheory.CategoryStruct.comp φ₁ l') (n : ℕ) {Z : C} (h : Q₂.homology R n ⊞ Q₃.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (SSetPair.homologyMap φ₂ R n) (SSetPair.homologyMap φ₃ R n)) h) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap φ₁ R n) (CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t' l' n) h)

The first map of the relative Mayer–Vietoris sequence is natural in maps of squares of pairs.

theorem SSetPair.mayerVietorisFromBiprod_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} {Q₂ Q₃ Q₄ : SSetPair} {r' : Q₂ ⟶ Q₄} {b' : Q₃ ⟶ Q₄} (φ₂ : P₂ ⟶ Q₂) (φ₃ : P₃ ⟶ Q₃) (φ₄ : P₄ ⟶ Q₄) (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) (SSetPair.homologyMap φ₄ R n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (SSetPair.homologyMap φ₂ R n) (SSetPair.homologyMap φ₃ R n)) (mayerVietorisFromBiprod R r' b' n)

The second map of the relative Mayer–Vietoris sequence is natural in maps of squares of pairs.

theorem SSetPair.mayerVietorisFromBiprod_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} {Q₂ Q₃ Q₄ : SSetPair} {r' : Q₂ ⟶ Q₄} {b' : Q₃ ⟶ Q₄} (φ₂ : P₂ ⟶ Q₂) (φ₃ : P₃ ⟶ Q₃) (φ₄ : P₄ ⟶ Q₄) (hr : CategoryTheory.CategoryStruct.comp r φ₄ = CategoryTheory.CategoryStruct.comp φ₂ r') (hb : CategoryTheory.CategoryStruct.comp b φ₄ = CategoryTheory.CategoryStruct.comp φ₃ b') (n : ℕ) {Z : C} (h : Q₄.homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) (CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap φ₄ R n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (SSetPair.homologyMap φ₂ R n) (SSetPair.homologyMap φ₃ R n)) (CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r' b' n) h)

The second map of the relative Mayer–Vietoris sequence is natural in maps of squares of pairs.

noncomputable def SSetPair.mayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) : P₄.homology R n ⟶ P₁.homology R m

The relative Mayer–Vietoris connecting morphism Hₙ(P₄) ⟶ Hₘ(P₁), where m + 1 = n: the connecting morphism of the relative Mayer–Vietoris short exact sequence of chain complexes.

theorem SSetPair.mayerVietorisδ_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) : mayerVietorisδ R sqL sqR n m h = ⋯.δ n m ⋯

@[simp]

theorem SSetPair.mayerVietorisδ_toBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sqL sqR n m h) (mayerVietorisToBiprod R t l m) = 0

@[simp]

theorem SSetPair.mayerVietorisδ_toBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : P₂.homology R m ⊞ P₃.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sqL sqR n m h) (CategoryTheory.CategoryStruct.comp (mayerVietorisToBiprod R t l m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem SSetPair.mayerVietorisFromBiprod_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) (mayerVietorisδ R sqL sqR n m h) = 0

@[simp]

theorem SSetPair.mayerVietorisFromBiprod_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : P₁.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisFromBiprod R r b n) (CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sqL sqR n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem SSetPair.mayerVietoris_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := P₄.homology R n, X₂ := P₁.homology R m, X₃ := P₂.homology R m ⊞ P₃.homology R m, f := mayerVietorisδ R sqL sqR n m h, g := mayerVietorisToBiprod R t l m, zero := ⋯ }.Exact

Exactness of the relative Mayer–Vietoris sequence at Hₘ(P₁).

theorem SSetPair.mayerVietoris_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n : ℕ) : { X₁ := P₁.homology R n, X₂ := P₂.homology R n ⊞ P₃.homology R n, X₃ := P₄.homology R n, f := mayerVietorisToBiprod R t l n, g := mayerVietorisFromBiprod R r b n, zero := ⋯ }.Exact

Exactness of the relative Mayer–Vietoris sequence at Hₙ(P₂) ⊞ Hₙ(P₃).

theorem SSetPair.mayerVietoris_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := P₂.homology R n ⊞ P₃.homology R n, X₂ := P₄.homology R n, X₃ := P₁.homology R m, f := mayerVietorisFromBiprod R r b n, g := mayerVietorisδ R sqL sqR n m h, zero := ⋯ }.Exact

Exactness of the relative Mayer–Vietoris sequence at Hₙ(P₄).

theorem SSetPair.epi_mayerVietorisFromBiprod_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] : CategoryTheory.Epi (mayerVietorisFromBiprod R r b 0)

The map H₀(P₂) ⊞ H₀(P₃) ⟶ H₀(P₄) at the end of the relative Mayer–Vietoris sequence is an epimorphism.

theorem SSetPair.mayerVietorisδ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} {Q₁ Q₂ Q₃ Q₄ : SSetPair} {t' : Q₁ ⟶ Q₂} {l' : Q₁ ⟶ Q₃} {r' : Q₂ ⟶ Q₄} {b' : Q₃ ⟶ Q₄} (φ₁ : P₁ ⟶ Q₁) (φ₂ : P₂ ⟶ Q₂) (φ₃ : P₃ ⟶ Q₃) (φ₄ : P₄ ⟶ Q₄) (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (sqL' : CategoryTheory.IsPushout t'.left l'.left r'.left b'.left) [CategoryTheory.Mono t'.left] (sqR' : CategoryTheory.IsPushout t'.right l'.right r'.right b'.right) [CategoryTheory.Mono t'.right] (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 sqL sqR n m h) (SSetPair.homologyMap φ₁ R m) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap φ₄ R n) (mayerVietorisδ R sqL' sqR' n m h)

Naturality of the relative Mayer–Vietoris connecting morphism in maps of squares of pairs.

theorem SSetPair.mayerVietorisδ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {P₁ P₂ P₃ P₄ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} {Q₁ Q₂ Q₃ Q₄ : SSetPair} {t' : Q₁ ⟶ Q₂} {l' : Q₁ ⟶ Q₃} {r' : Q₂ ⟶ Q₄} {b' : Q₃ ⟶ Q₄} (φ₁ : P₁ ⟶ Q₁) (φ₂ : P₂ ⟶ Q₂) (φ₃ : P₃ ⟶ Q₃) (φ₄ : P₄ ⟶ Q₄) (sqL : CategoryTheory.IsPushout t.left l.left r.left b.left) [CategoryTheory.Mono t.left] (sqR : CategoryTheory.IsPushout t.right l.right r.right b.right) [CategoryTheory.Mono t.right] (sqL' : CategoryTheory.IsPushout t'.left l'.left r'.left b'.left) [CategoryTheory.Mono t'.left] (sqR' : CategoryTheory.IsPushout t'.right l'.right r'.right b'.right) [CategoryTheory.Mono t'.right] (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✝ : Q₁.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sqL sqR n m h) (CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap φ₁ R m) h✝) = CategoryTheory.CategoryStruct.comp (SSetPair.homologyMap φ₄ R n) (CategoryTheory.CategoryStruct.comp (mayerVietorisδ R sqL' sqR' n m h) h✝)

Naturality of the relative Mayer–Vietoris connecting morphism in maps of squares of pairs.