The Mayer–Vietoris sequence of two pairs in singular cohomology

Let C ⊆ A and D ⊆ B be subsets of a topological space X, with A and B open in A ∪ B and C and D open in C ∪ D, and write Hⁿ(-) for relative singular cohomology Hⁿ(-; R, M), the cohomology of Hom(C(-; R), M). This file constructs the Mayer–Vietoris long exact sequence of the pairs (A, C) and (B, D), ⋯ ⟶ Hⁿ(A ∪ B, C ∪ D) ⟶ Hⁿ(A, C) ⊞ Hⁿ(B, D) ⟶ Hⁿ(A ∩ B, C ∩ D) ⟶ Hⁿ⁺¹(A ∪ B, C ∪ D) ⟶ ⋯, whose first map is (j_A^*, j_B^*) and whose second map is i_A^* - i_B^*, the i and j being the maps of pairs induced by the inclusions. These are the maps dual to the maps j_A + j_B and (i_A, -i_B) of the sequence in singular homology (TopCat.pairMayerVietorisδ).

For the restrictions (E|U, E₀|U) and (E|V, E₀|V) of the Thom pair of a vector bundle to two open sets U and V of its base, this is the sequence which glues classes of the Thom pairs over U and over V that agree over U ∩ V to a class of the Thom pair over U ∪ V, as in the construction of the Thom class by induction over trivializing open sets.

The construction dualizes the one in homology. 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 Mayer–Vietoris short exact sequence of chain complexes is split in each degree: its last map has the section obtained from a section of the absolute sequence of the ambient simplicial sets, since relative chains are a retract of ambient chains (SSetPair.isSplitEpi_mayerVietoris_g_f). So applying Hom(-, M) keeps it short exact (SSetPair.shortExact_mayerVietorisCochainShortComplex), and its cohomology sequence is the long exact sequence ⋯ ⟶ Hⁿ(P₄) ⟶ Hⁿ(P₂) ⊞ Hⁿ(P₃) ⟶ Hⁿ(P₁) ⟶ Hⁿ⁺¹(P₄) ⟶ ⋯. For the square of singular pairs of (A ∩ B, C ∩ D), (A, C), (B, D) and the singular simplices of X lying in A or in B, relative to those lying in C or in D (TopCat.smallSingularPair), the small-chain theorem identifies the cohomology of the last pair with Hⁿ(A ∪ B, C ∪ D): a map of pairs of simplicial sets inducing quasi-isomorphisms on the cochains of both components induces one on relative cochains (SSetPair.quasiIso_cochainComplexMap).

Main definitions and results

• SSetPair.shortExact_mayerVietorisCochainShortComplex: the relative cochain Mayer–Vietoris sequence of a square of pairs of simplicial sets is short exact.
• SSetPair.mayerVietorisCochainToBiprod, SSetPair.mayerVietorisCochainFromBiprod and SSetPair.mayerVietorisCochainδ: the maps of its long exact cohomology sequence, exact by SSetPair.mayerVietorisCochain_exact₁, SSetPair.mayerVietorisCochain_exact₂ and SSetPair.mayerVietorisCochain_exact₃.
• TopCat.singularCohomologyPairMayerVietorisToBiprod and TopCat.singularCohomologyPairMayerVietorisFromBiprod: the maps Hⁿ(A ∪ B, C ∪ D) ⟶ Hⁿ(A, C) ⊞ Hⁿ(B, D) and Hⁿ(A, C) ⊞ Hⁿ(B, D) ⟶ Hⁿ(A ∩ B, C ∩ D).
• TopCat.singularCohomologyPairMayerVietorisδ: the connecting morphism Hⁿ(A ∩ B, C ∩ D) ⟶ Hᵐ(A ∪ B, C ∪ D), n + 1 = m.
• TopCat.singularCohomologyPairMayerVietoris_exact₁, TopCat.singularCohomologyPairMayerVietoris_exact₂, TopCat.singularCohomologyPairMayerVietoris_exact₃: exactness at Hᵐ(A ∪ B, C ∪ D), at Hⁿ(A, C) ⊞ Hⁿ(B, D) and at Hⁿ(A ∩ B, C ∩ D).
• TopCat.mono_singularCohomologyPairMayerVietorisToBiprod_zero: injectivity at the degree-zero endpoint.
• SSetPair.mayerVietorisCochainδ_naturality: the relative cochain connecting morphism is natural in maps of squares of pairs of simplicial sets.
• TopCat.singularCohomologyPairMayerVietorisδ_naturality: the connecting morphism is natural in maps f : X ⟶ Y carrying A, B, C and D into A', B', C' and D', and TopCat.singularCohomologyPairMayerVietorisδ_naturality_of_subset is the case of the inclusions for A ⊆ A', B ⊆ B', C ⊆ C' and D ⊆ D' in X.
• TopCat.quasiIso_cochainComplexMap_smallSingularSubcomplexPairToUnion and TopCat.isIso_homologyMap_cochainComplexMap_smallSingularSubcomplexPairToUnion: for U and V open in U ∪ V, the cochains of X relative to its singular simplices lying in U or in V compute the cohomology of (X, U ∪ V).

References

• A. Hatcher, Algebraic Topology, Section 3.1, the Mayer–Vietoris sequences in cohomology, including the relative ones.
• J. W. Milnor, J. D. Stasheff, Characteristic Classes, Annals of Mathematics Studies 76, Princeton (1974), §10, where the cohomological sequence of two pairs over open sets of a base is used to construct the Thom class.

The relative cochain Mayer–Vietoris sequence

@[reducible, inline]

noncomputable abbrev SSetPair.mayerVietorisCochainShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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.ShortComplex (CochainComplex (ModuleCat k) ℕ)

The relative cochain Mayer–Vietoris sequence Hom(C(P₄), M) ⟶ Hom(C(P₂), M) ⊞ Hom(C(P₃), M) ⟶ Hom(C(P₁), M) of a commutative square of pairs of simplicial sets, with first map (r^*, b^*) and second map t^* - l^*.

The maps of the sequence

noncomputable def SSetPair.mayerVietorisCochainToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₂ P₃ P₄ : SSetPair} (r : P₂ ⟶ P₄) (b : P₃ ⟶ P₄) (n : ℕ) : HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) n ⟶ HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) n

The first map Hⁿ(P₄) ⟶ Hⁿ(P₂) ⊞ Hⁿ(P₃) of the relative cochain Mayer–Vietoris sequence, with components r^* and b^*.

@[simp]

theorem SSetPair.mayerVietorisCochainToBiprod_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) CategoryTheory.Limits.biprod.fst = HomologicalComplex.homologyMap (cochainComplexMap r) n

@[simp]

theorem SSetPair.mayerVietorisCochainToBiprod_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap r) n) h

@[simp]

theorem SSetPair.mayerVietorisCochainToBiprod_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) CategoryTheory.Limits.biprod.snd = HomologicalComplex.homologyMap (cochainComplexMap b) n

@[simp]

theorem SSetPair.mayerVietorisCochainToBiprod_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₂ P₃ P₄ : SSetPair} {r : P₂ ⟶ P₄} {b : P₃ ⟶ P₄} (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap b) n) h

noncomputable def SSetPair.mayerVietorisCochainFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₁ P₂ P₃ : SSetPair} (t : P₁ ⟶ P₂) (l : P₁ ⟶ P₃) (n : ℕ) : HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) n ⟶ HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n

The second map Hⁿ(P₂) ⊞ Hⁿ(P₃) ⟶ Hⁿ(P₁) of the relative cochain Mayer–Vietoris sequence, the difference t^* - l^*.

@[simp]

theorem SSetPair.inl_mayerVietorisCochainFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (mayerVietorisCochainFromBiprod R k M t l n) = HomologicalComplex.homologyMap (cochainComplexMap t) n

@[simp]

theorem SSetPair.inl_mayerVietorisCochainFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap t) n) h

@[simp]

theorem SSetPair.inr_mayerVietorisCochainFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (mayerVietorisCochainFromBiprod R k M t l n) = -HomologicalComplex.homologyMap (cochainComplexMap l) n

@[simp]

theorem SSetPair.inr_mayerVietorisCochainFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {P₁ P₂ P₃ : SSetPair} {t : P₁ ⟶ P₂} {l : P₁ ⟶ P₃} (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) h) = CategoryTheory.CategoryStruct.comp (-HomologicalComplex.homologyMap (cochainComplexMap l) n) h

@[simp]

theorem SSetPair.mayerVietorisCochainToBiprod_fromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 (mayerVietorisCochainToBiprod R k M r b n) (mayerVietorisCochainFromBiprod R k M t l n) = 0

@[simp]

theorem SSetPair.mayerVietorisCochainToBiprod_fromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : ModuleCat k} (h : HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem SSetPair.shortExact_mayerVietorisCochainShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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] : (mayerVietorisCochainShortComplex R k M ⋯).ShortExact

The relative cochain 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 cochain Mayer–Vietoris sequence is short exact.

The long exact sequence

noncomputable def SSetPair.mayerVietorisCochainδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) : HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n ⟶ HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) m

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

theorem SSetPair.mayerVietorisCochainδ_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) : mayerVietorisCochainδ R k M sqL sqR n m h = ⋯.δ n m ⋯

The relative cochain Mayer–Vietoris connecting morphism is the connecting morphism of the relative cochain Mayer–Vietoris short exact sequence.

@[simp]

theorem SSetPair.mayerVietorisCochainδ_toBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sqL sqR n m h) (mayerVietorisCochainToBiprod R k M r b m) = 0

@[simp]

theorem SSetPair.mayerVietorisCochainδ_toBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) m ⊞ HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sqL sqR n m h) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem SSetPair.mayerVietorisCochainFromBiprod_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) (mayerVietorisCochainδ R k M sqL sqR n m h) = 0

@[simp]

theorem SSetPair.mayerVietorisCochainFromBiprod_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sqL sqR n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem SSetPair.mayerVietorisCochain_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) : { X₁ := HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n, X₂ := HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) m, X₃ := HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) m ⊞ HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) m, f := mayerVietorisCochainδ R k M sqL sqR n m h, g := mayerVietorisCochainToBiprod R k M r b m, zero := ⋯ }.Exact

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

theorem SSetPair.mayerVietorisCochain_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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₁ := HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) n, X₂ := HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) n, X₃ := HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n, f := mayerVietorisCochainToBiprod R k M r b n, g := mayerVietorisCochainFromBiprod R k M t l n, zero := ⋯ }.Exact

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

theorem SSetPair.mayerVietorisCochain_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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 : n + 1 = m := by lia) : { X₁ := HomologicalComplex.homology ((P₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((P₃.chainComplex R).linearYonedaObj k M) n, X₂ := HomologicalComplex.homology ((P₁.chainComplex R).linearYonedaObj k M) n, X₃ := HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) m, f := mayerVietorisCochainFromBiprod R k M t l n, g := mayerVietorisCochainδ R k M sqL sqR n m h, zero := ⋯ }.Exact

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

theorem SSetPair.mono_mayerVietorisCochainToBiprod_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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.Mono (mayerVietorisCochainToBiprod R k M r b 0)

The map H⁰(P₄) ⟶ H⁰(P₂) ⊞ H⁰(P₃) at the start of the relative cochain Mayer–Vietoris sequence is a monomorphism.

theorem SSetPair.mayerVietorisCochainδ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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] {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] (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 : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sqL' sqR' n m h) (HomologicalComplex.homologyMap (cochainComplexMap φ₄) m) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap φ₁) n) (mayerVietorisCochainδ R k M sqL sqR n m h)

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

theorem SSetPair.mayerVietorisCochainδ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : 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] {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] (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 : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((P₄.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sqL' sqR' n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap φ₄) m) h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap φ₁) n) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sqL sqR n m h) h✝)

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

The small-chain comparison on cochains

theorem TopCat.quasiIso_cochainComplexMap_smallSingularSubcomplexToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} (U V : Set ↑X) (hU : IsOpen (Subtype.val ⁻¹' U)) (hV : IsOpen (Subtype.val ⁻¹' V)) : QuasiIso (SSet.cochainComplexMap (smallSingularSubcomplexToUnion U V))

The singular simplices of X lying in U or in V compute the cohomology of U ∪ V, by the small-chain theorem for the cover of U ∪ V by U and V, which only needs to be open in U ∪ V.

theorem TopCat.quasiIso_cochainComplexMap_smallSingularSubcomplexPairToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} (U V : Set ↑X) (hU : IsOpen (Subtype.val ⁻¹' U)) (hV : IsOpen (Subtype.val ⁻¹' V)) : QuasiIso (SSetPair.cochainComplexMap (smallSingularSubcomplexPairToUnion U V))

The cohomology of X relative to its singular simplices lying in U or in V is that of (X, U ∪ V), by the small-chain theorem for the cover of U ∪ V by U and V, which only needs to be open in U ∪ V.

theorem TopCat.isIso_homologyMap_cochainComplexMap_smallSingularSubcomplexPairToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} (U V : Set ↑X) (hU : IsOpen (Subtype.val ⁻¹' U)) (hV : IsOpen (Subtype.val ⁻¹' V)) (n : ℕ) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (SSetPair.cochainComplexMap (smallSingularSubcomplexPairToUnion U V)) n)

For U and V open in U ∪ V, restricting cochains of (X, U ∪ V) to the chains of X relative to its singular simplices lying in U or in V is an isomorphism on cohomology.

The Mayer–Vietoris sequence of two pairs

noncomputable def TopCat.singularCohomologyPairMayerVietorisToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : (TopPair.ofInclusion ⋯).singularCohomology R k M n ⟶ (TopPair.ofInclusion hCA).singularCohomology R k M n ⊞ (TopPair.ofInclusion hDB).singularCohomology R k M n

The first map Hⁿ(A ∪ B, C ∪ D) ⟶ Hⁿ(A, C) ⊞ Hⁿ(B, D) of the Mayer–Vietoris sequence of the pairs (A, C) and (B, D) in singular cohomology, with components the restrictions j_A^* and j_B^* along the maps of pairs induced by the inclusions.

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisToBiprod_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n) CategoryTheory.Limits.biprod.fst = TopPair.singularCohomologyMap (TopPair.ofInclusionMap hCA ⋯ (ContinuousMap.inclusion ⋯) ⋯) n

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisToBiprod_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : ModuleCat k} (h : (TopPair.ofInclusion hCA).singularCohomology R k M n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap hCA ⋯ (ContinuousMap.inclusion ⋯) ⋯) n) h

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisToBiprod_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n) CategoryTheory.Limits.biprod.snd = TopPair.singularCohomologyMap (TopPair.ofInclusionMap hDB ⋯ (ContinuousMap.inclusion ⋯) ⋯) n

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisToBiprod_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : ModuleCat k} (h : (TopPair.ofInclusion hDB).singularCohomology R k M n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap hDB ⋯ (ContinuousMap.inclusion ⋯) ⋯) n) h

noncomputable def TopCat.singularCohomologyPairMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : (TopPair.ofInclusion hCA).singularCohomology R k M n ⊞ (TopPair.ofInclusion hDB).singularCohomology R k M n ⟶ (TopPair.ofInclusion ⋯).singularCohomology R k M n

The second map Hⁿ(A, C) ⊞ Hⁿ(B, D) ⟶ Hⁿ(A ∩ B, C ∩ D) of the Mayer–Vietoris sequence of the pairs (A, C) and (B, D) in singular cohomology, the difference i_A^* - i_B^* of the restrictions along the maps of pairs induced by the inclusions.

@[simp]

theorem TopCat.inl_singularCohomologyPairMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) = TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ hCA (ContinuousMap.inclusion ⋯) ⋯) n

@[simp]

theorem TopCat.inl_singularCohomologyPairMayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : ModuleCat k} (h : (TopPair.ofInclusion ⋯).singularCohomology R k M n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ hCA (ContinuousMap.inclusion ⋯) ⋯) n) h

@[simp]

theorem TopCat.inr_singularCohomologyPairMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) = -TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ hDB (ContinuousMap.inclusion ⋯) ⋯) n

@[simp]

theorem TopCat.inr_singularCohomologyPairMayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : ModuleCat k} (h : (TopPair.ofInclusion ⋯).singularCohomology R k M n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) h) = CategoryTheory.CategoryStruct.comp (-TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ hDB (ContinuousMap.inclusion ⋯) ⋯) n) h

Comparison with the square of singular pairs

theorem TopCat.isIso_homologyMap_cochainComplexMap_smallSingularPairToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n : ℕ) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (SSetPair.cochainComplexMap (smallSingularPairToUnion hCA hDB)) n)

The cohomology of TopCat.smallSingularPair hCA hDB is identified with that of (A ∪ B, C ∪ D) by TopCat.smallSingularPairToUnion.

The long exact sequence

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisToBiprod_fromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n) (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) = 0

The first two maps of the Mayer–Vietoris sequence of two pairs in singular cohomology compose to zero.

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisToBiprod_fromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : ModuleCat k} (h : (TopPair.ofInclusion ⋯).singularCohomology R k M n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n) (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) h) = CategoryTheory.CategoryStruct.comp 0 h

The first two maps of the Mayer–Vietoris sequence of two pairs in singular cohomology compose to zero.

noncomputable def TopCat.singularCohomologyPairMayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) : (TopPair.ofInclusion ⋯).singularCohomology R k M n ⟶ (TopPair.ofInclusion ⋯).singularCohomology R k M m

The connecting morphism Hⁿ(A ∩ B, C ∩ D) ⟶ Hᵐ(A ∪ B, C ∪ D), n + 1 = m, of the Mayer–Vietoris sequence of the pairs (A, C) and (B, D) in singular cohomology, for A and B open in A ∪ B and C and D open in C ∪ D. It is the connecting morphism of the relative cochain Mayer–Vietoris sequence of the singular pairs of A ∩ B, A, B and of the singular simplices of X lying in A or in B (relative to those lying in C or in D), followed by the inverse of the small-chain isomorphism identifying the cohomology of the last of these with Hᵐ(A ∪ B, C ∪ D).

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisδ_comp_homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) (HomologicalComplex.homologyMap (SSetPair.cochainComplexMap (smallSingularPairToUnion hCA hDB)) m) = SSetPair.mayerVietorisCochainδ R k M ⋯ ⋯ n m h

Followed by restriction to the singular simplices lying in A or in B, the connecting morphism of the Mayer–Vietoris sequence of two pairs is the connecting morphism of the relative cochain Mayer–Vietoris sequence of the square of singular pairs. Since that restriction is an isomorphism on cohomology, this characterizes it.

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisδ_comp_homologyMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology (((smallSingularPair hCA hDB).chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (SSetPair.cochainComplexMap (smallSingularPairToUnion hCA hDB)) m) h✝) = CategoryTheory.CategoryStruct.comp (SSetPair.mayerVietorisCochainδ R k M ⋯ ⋯ n m h) h✝

Followed by restriction to the singular simplices lying in A or in B, the connecting morphism of the Mayer–Vietoris sequence of two pairs is the connecting morphism of the relative cochain Mayer–Vietoris sequence of the square of singular pairs. Since that restriction is an isomorphism on cohomology, this characterizes it.

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisδ_toBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB m) = 0

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisδ_toBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : (TopPair.ofInclusion hCA).singularCohomology R k M m ⊞ (TopPair.ofInclusion hDB).singularCohomology R k M m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisFromBiprod_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) = 0

@[simp]

theorem TopCat.singularCohomologyPairMayerVietorisFromBiprod_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : (TopPair.ofInclusion ⋯).singularCohomology R k M m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n) (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopCat.singularCohomologyPairMayerVietoris_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := (TopPair.ofInclusion ⋯).singularCohomology R k M n, X₂ := (TopPair.ofInclusion ⋯).singularCohomology R k M m, X₃ := (TopPair.ofInclusion hCA).singularCohomology R k M m ⊞ (TopPair.ofInclusion hDB).singularCohomology R k M m, f := singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h, g := singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB m, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence of two pairs at Hᵐ(A ∪ B, C ∪ D).

theorem TopCat.singularCohomologyPairMayerVietoris_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n : ℕ) : { X₁ := (TopPair.ofInclusion ⋯).singularCohomology R k M n, X₂ := (TopPair.ofInclusion hCA).singularCohomology R k M n ⊞ (TopPair.ofInclusion hDB).singularCohomology R k M n, X₃ := (TopPair.ofInclusion ⋯).singularCohomology R k M n, f := singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB n, g := singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence of two pairs at Hⁿ(A, C) ⊞ Hⁿ(B, D).

theorem TopCat.singularCohomologyPairMayerVietoris_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := (TopPair.ofInclusion hCA).singularCohomology R k M n ⊞ (TopPair.ofInclusion hDB).singularCohomology R k M n, X₂ := (TopPair.ofInclusion ⋯).singularCohomology R k M n, X₃ := (TopPair.ofInclusion ⋯).singularCohomology R k M m, f := singularCohomologyPairMayerVietorisFromBiprod R k M hCA hDB n, g := singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence of two pairs at Hⁿ(A ∩ B, C ∩ D).

theorem TopCat.mono_singularCohomologyPairMayerVietorisToBiprod_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) : CategoryTheory.Mono (singularCohomologyPairMayerVietorisToBiprod R k M hCA hDB 0)

The map H⁰(A ∪ B, C ∪ D) ⟶ H⁰(A, C) ⊞ H⁰(B, D) at the start of the Mayer–Vietoris sequence of two pairs in singular cohomology is a monomorphism.

Naturality of the connecting morphism

theorem TopCat.singularCohomologyPairMayerVietorisδ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (hA' : IsOpen (Subtype.val ⁻¹' A')) (hB' : IsOpen (Subtype.val ⁻¹' B')) (hC' : IsOpen (Subtype.val ⁻¹' C')) (hD' : IsOpen (Subtype.val ⁻¹' D')) (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C✝ C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA' hDB' hA' hB' hC' hD' n m h) (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (A ∪ B) (A' ∪ B') ⋯, continuous_toFun := ⋯ } ⋯) m) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (A ∩ B) (A' ∩ B') ⋯, continuous_toFun := ⋯ } ⋯) n) (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h)

Naturality of the connecting morphism of the Mayer–Vietoris sequence of two pairs. A map f : X ⟶ Y carrying A, B, C and D into A', B', C' and D' commutes with the connecting morphisms, where (A ∩ B, C ∩ D) ⟶ (A' ∩ B', C' ∩ D') and (A ∪ B, C ∪ D) ⟶ (A' ∪ B', C' ∪ D') are the maps of pairs given by the restrictions of f.

theorem TopCat.singularCohomologyPairMayerVietorisδ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (hA' : IsOpen (Subtype.val ⁻¹' A')) (hB' : IsOpen (Subtype.val ⁻¹' B')) (hC' : IsOpen (Subtype.val ⁻¹' C')) (hD' : IsOpen (Subtype.val ⁻¹' D')) (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C✝ C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : (TopPair.ofInclusion ⋯).singularCohomology R k M m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA' hDB' hA' hB' hC' hD' n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (A ∪ B) (A' ∪ B') ⋯, continuous_toFun := ⋯ } ⋯) m) h✝) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (A ∩ B) (A' ∩ B') ⋯, continuous_toFun := ⋯ } ⋯) n) (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) h✝)

Naturality of the connecting morphism of the Mayer–Vietoris sequence of two pairs. A map f : X ⟶ Y carrying A, B, C and D into A', B', C' and D' commutes with the connecting morphisms, where (A ∩ B, C ∩ D) ⟶ (A' ∩ B', C' ∩ D') and (A ∪ B, C ∪ D) ⟶ (A' ∪ B', C' ∪ D') are the maps of pairs given by the restrictions of f.

theorem TopCat.singularCohomologyPairMayerVietorisδ_naturality_of_subset {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) {A' B' C' D' : Set ↑X} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (hA' : IsOpen (Subtype.val ⁻¹' A')) (hB' : IsOpen (Subtype.val ⁻¹' B')) (hC' : IsOpen (Subtype.val ⁻¹' C')) (hD' : IsOpen (Subtype.val ⁻¹' D')) (hAA' : A ⊆ A') (hBB' : B ⊆ B') (hCC' : C✝ ⊆ C') (hDD' : D ⊆ D') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA' hDB' hA' hB' hC' hD' n m h) (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.inclusion ⋯) ⋯) m) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.inclusion ⋯) ⋯) n) (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h)

Naturality of the connecting morphism of the Mayer–Vietoris sequence of two pairs in inclusions. For A ⊆ A', B ⊆ B', C ⊆ C' and D ⊆ D', the connecting morphisms commute with the restrictions along the inclusions (A ∩ B, C ∩ D) ⟶ (A' ∩ B', C' ∩ D') and (A ∪ B, C ∪ D) ⟶ (A' ∪ B', C' ∪ D').

theorem TopCat.singularCohomologyPairMayerVietorisδ_naturality_of_subset_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) {A' B' C' D' : Set ↑X} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (hA' : IsOpen (Subtype.val ⁻¹' A')) (hB' : IsOpen (Subtype.val ⁻¹' B')) (hC' : IsOpen (Subtype.val ⁻¹' C')) (hD' : IsOpen (Subtype.val ⁻¹' D')) (hAA' : A ⊆ A') (hBB' : B ⊆ B') (hCC' : C✝ ⊆ C') (hDD' : D ⊆ D') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : (TopPair.ofInclusion ⋯).singularCohomology R k M m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA' hDB' hA' hB' hC' hD' n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.inclusion ⋯) ⋯) m) h✝) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.inclusion ⋯) ⋯) n) (CategoryTheory.CategoryStruct.comp (singularCohomologyPairMayerVietorisδ R k M hCA hDB hA hB hC hD n m h) h✝)

Naturality of the connecting morphism of the Mayer–Vietoris sequence of two pairs in inclusions. For A ⊆ A', B ⊆ B', C ⊆ C' and D ⊆ D', the connecting morphisms commute with the restrictions along the inclusions (A ∩ B, C ∩ D) ⟶ (A' ∩ B', C' ∩ D') and (A ∪ B, C ∪ D) ⟶ (A' ∪ B', C' ∪ D').