The Mayer–Vietoris sequence in singular cohomology

Let U and V be open subsets of a topological space X with U ∪ V = X, let R and M be objects of a k-linear abelian category with coproducts, and write Hⁿ(-) for singular cohomology Hⁿ(-; R, M), the cohomology of Hom(C(-; R), M). This file constructs the Mayer–Vietoris long exact sequence ⋯ ⟶ Hⁿ(X) ⟶ Hⁿ(U) ⊞ Hⁿ(V) ⟶ Hⁿ(U ∩ V) ⟶ Hⁿ⁺¹(X) ⟶ ⋯, whose first map is (j_U^*, j_V^*) and whose second map is i_U^* - i_V^*, the i and j being the inclusions. These are the maps dual to the maps j_U + j_V and (i_U, -i_V) of the Mayer–Vietoris sequence in singular homology. The connecting morphism is natural in maps of covered spaces.

The construction dualizes the one in homology. For a pushout square of simplicial sets

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

whose top map is a monomorphism, the Mayer–Vietoris short exact sequence of chain complexes is split in each degree, so applying Hom(-, M) keeps it short exact (SSet.shortExact_mayerVietorisCochainShortComplex). Its cohomology sequence is a long exact sequence ⋯ ⟶ Hⁿ(X₄) ⟶ Hⁿ(X₂) ⊞ Hⁿ(X₃) ⟶ Hⁿ(X₁) ⟶ Hⁿ⁺¹(X₄) ⟶ ⋯, natural in maps of pushout squares. For the singular simplicial sets of U ∩ V, U, V and the subcomplex of singular simplices of X lying in U or in V, the small-chain theorem identifies the cohomology of that subcomplex with the singular cohomology of X (TauCeti.smallSingularCohomologyIso).

Main definitions and results

• SSet.shortExact_mayerVietorisCochainShortComplex: the cochain Mayer–Vietoris sequence of a pushout square of simplicial sets is short exact.
• SSet.mayerVietorisCochainToBiprod, SSet.mayerVietorisCochainFromBiprod and SSet.mayerVietorisCochainδ: the maps of its long exact cohomology sequence, exact by SSet.mayerVietorisCochain_exact₁, SSet.mayerVietorisCochain_exact₂ and SSet.mayerVietorisCochain_exact₃, with connecting morphism natural in maps of pushout squares (SSet.mayerVietorisCochainδ_naturality); the other two maps are natural as well (SSet.mayerVietorisCochainToBiprod_naturality, SSet.mayerVietorisCochainFromBiprod_naturality).
• TauCeti.smallSingularCohomologyIso: restricting cochains to the chains subordinate to an open cover is an isomorphism on cohomology, natural in maps of covered spaces (TauCeti.smallSingularCohomologyIso_naturality); equivalently, that restriction is a quasi-isomorphism (TauCeti.quasiIso_cochainComplexMap_smallSingularSubcomplex_ι).
• TopCat.singularCohomologyMayerVietorisToBiprod and TopCat.singularCohomologyMayerVietorisFromBiprod: the maps Hⁿ(X) ⟶ Hⁿ(U) ⊞ Hⁿ(V) and Hⁿ(U) ⊞ Hⁿ(V) ⟶ Hⁿ(U ∩ V).
• TopCat.singularCohomologyMayerVietorisδ: the connecting morphism Hⁿ(U ∩ V) ⟶ Hᵐ(X), n + 1 = m, characterized by TopCat.singularCohomologyMayerVietorisδ_comp_homologyMap.
• TopCat.singularCohomologyMayerVietoris_exact₁, TopCat.singularCohomologyMayerVietoris_exact₂, TopCat.singularCohomologyMayerVietoris_exact₃: exactness at Hᵐ(X), at Hⁿ(U) ⊞ Hⁿ(V) and at Hⁿ(U ∩ V).
• TopCat.mono_singularCohomologyMayerVietorisToBiprod_zero: injectivity at the degree-zero endpoint.
• TopCat.singularCohomologyMayerVietorisδ_naturality: naturality of the connecting morphism.

References

• A. Hatcher, Algebraic Topology, Section 3.1, the Mayer–Vietoris sequences in cohomology.

@[reducible, inline]

noncomputable abbrev SSet.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) {X₁ X₂ X₃ X₄ : SSet} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq t l r b) : CategoryTheory.ShortComplex (CochainComplex (ModuleCat k) ℕ)

The cochain Mayer–Vietoris sequence Hom(C(X₄), M) ⟶ Hom(C(X₂), M) ⊞ Hom(C(X₃), M) ⟶ Hom(C(X₁), M) of a commutative square of simplicial sets, with first map (r^*, b^*) and second map t^* - l^*. It is the image under Hom(-, M) of the chain Mayer–Vietoris sequence, once Hom(C(X₂) ⊞ C(X₃), M) is identified with Hom(C(X₂), M) ⊞ Hom(C(X₃), M).

theorem SSet.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) {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] : (mayerVietorisCochainShortComplex R k M ⋯).ShortExact

The cochain Mayer–Vietoris short exact sequence. For a pushout square of simplicial sets whose top map is a monomorphism, the cochain Mayer–Vietoris sequence is short exact.

The long exact sequence of a pushout square

noncomputable def SSet.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) {X₂ X₃ X₄ : SSet} (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄) (n : ℕ) : HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) n ⟶ HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) n

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

@[simp]

theorem SSet.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) {X₂ X₃ X₄ : SSet} (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄) (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) CategoryTheory.Limits.biprod.fst = HomologicalComplex.homologyMap (cochainComplexMap r) n

@[simp]

theorem SSet.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) {X₂ X₃ X₄ : SSet} (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((X₂.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 SSet.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) {X₂ X₃ X₄ : SSet} (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄) (n : ℕ) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) CategoryTheory.Limits.biprod.snd = HomologicalComplex.homologyMap (cochainComplexMap b) n

@[simp]

theorem SSet.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) {X₂ X₃ X₄ : SSet} (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((X₃.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 SSet.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) {X₁ X₂ X₃ : SSet} (t : X₁ ⟶ X₂) (l : X₁ ⟶ X₃) (n : ℕ) : HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) n ⟶ HomologicalComplex.homology ((X₁.chainComplex R).linearYonedaObj k M) n

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

@[simp]

theorem SSet.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) {X₁ X₂ X₃ : SSet} (t : X₁ ⟶ X₂) (l : X₁ ⟶ X₃) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (mayerVietorisCochainFromBiprod R k M t l n) = HomologicalComplex.homologyMap (cochainComplexMap t) n

@[simp]

theorem SSet.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) {X₁ X₂ X₃ : SSet} (t : X₁ ⟶ X₂) (l : X₁ ⟶ X₃) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((X₁.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 SSet.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) {X₁ X₂ X₃ : SSet} (t : X₁ ⟶ X₂) (l : X₁ ⟶ X₃) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (mayerVietorisCochainFromBiprod R k M t l n) = -HomologicalComplex.homologyMap (cochainComplexMap l) n

@[simp]

theorem SSet.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) {X₁ X₂ X₃ : SSet} (t : X₁ ⟶ X₂) (l : X₁ ⟶ X₃) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((X₁.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 SSet.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) {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 (mayerVietorisCochainToBiprod R k M r b n) (mayerVietorisCochainFromBiprod R k M t l n) = 0

@[simp]

theorem SSet.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) {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 : ModuleCat k} (h : HomologicalComplex.homology ((X₁.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 SSet.mayerVietorisCochainToBiprod_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₂ 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 (HomologicalComplex.homologyMap (cochainComplexMap φ₄) n) (mayerVietorisCochainToBiprod R k M r b n) = CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r' b' n) (CategoryTheory.Limits.biprod.map (HomologicalComplex.homologyMap (cochainComplexMap φ₂) n) (HomologicalComplex.homologyMap (cochainComplexMap φ₃) n))

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

theorem SSet.mayerVietorisCochainToBiprod_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₂ 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 : ModuleCat k} (h : HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap φ₄) n) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b n) h) = CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r' b' n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (HomologicalComplex.homologyMap (cochainComplexMap φ₂) n) (HomologicalComplex.homologyMap (cochainComplexMap φ₃) n)) h)

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

theorem SSet.mayerVietorisCochainFromBiprod_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₁ 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 (CategoryTheory.Limits.biprod.map (HomologicalComplex.homologyMap (cochainComplexMap φ₂) n) (HomologicalComplex.homologyMap (cochainComplexMap φ₃) n)) (mayerVietorisCochainFromBiprod R k M t l n) = CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t' l' n) (HomologicalComplex.homologyMap (cochainComplexMap φ₁) n)

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

theorem SSet.mayerVietorisCochainFromBiprod_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₁ 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 : ModuleCat k} (h : HomologicalComplex.homology ((X₁.chainComplex R).linearYonedaObj k M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (HomologicalComplex.homologyMap (cochainComplexMap φ₂) n) (HomologicalComplex.homologyMap (cochainComplexMap φ₃) n)) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) h) = CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t' l' n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap φ₁) n) h)

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

noncomputable def SSet.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) {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 : n + 1 = m := by lia) : HomologicalComplex.homology ((X₁.chainComplex R).linearYonedaObj k M) n ⟶ HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) m

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

theorem SSet.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) {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 : n + 1 = m := by lia) : mayerVietorisCochainδ R k M sq n m h = ⋯.δ n m ⋯

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

@[simp]

theorem SSet.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) {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 : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sq n m h) (mayerVietorisCochainToBiprod R k M r b m) = 0

@[simp]

theorem SSet.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) {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 : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) m ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sq n m h) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainToBiprod R k M r b m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem SSet.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) {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 : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) (mayerVietorisCochainδ R k M sq n m h) = 0

@[simp]

theorem SSet.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) {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 : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainFromBiprod R k M t l n) (CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sq n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem SSet.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) {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 : n + 1 = m := by lia) : { X₁ := HomologicalComplex.homology ((X₁.chainComplex R).linearYonedaObj k M) n, X₂ := HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) m, X₃ := HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) m ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) m, f := mayerVietorisCochainδ R k M sq n m h, g := mayerVietorisCochainToBiprod R k M r b m, zero := ⋯ }.Exact

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

theorem SSet.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) {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₁ := HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) n, X₂ := HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) n, X₃ := HomologicalComplex.homology ((X₁.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 cochain Mayer–Vietoris sequence at Hⁿ(X₂) ⊞ Hⁿ(X₃).

theorem SSet.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) {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 : n + 1 = m := by lia) : { X₁ := HomologicalComplex.homology ((X₂.chainComplex R).linearYonedaObj k M) n ⊞ HomologicalComplex.homology ((X₃.chainComplex R).linearYonedaObj k M) n, X₂ := HomologicalComplex.homology ((X₁.chainComplex R).linearYonedaObj k M) n, X₃ := HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) m, f := mayerVietorisCochainFromBiprod R k M t l n, g := mayerVietorisCochainδ R k M sq n m h, zero := ⋯ }.Exact

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

theorem SSet.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) {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.Mono (mayerVietorisCochainToBiprod R k M r b 0)

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

theorem SSet.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) {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 : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sq' n m h) (HomologicalComplex.homologyMap (cochainComplexMap φ₄) m) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (cochainComplexMap φ₁) n) (mayerVietorisCochainδ R k M sq n m h)

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

theorem SSet.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) {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 : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology ((X₄.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisCochainδ R k M sq' 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 sq n m h) h✝)

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

noncomputable def TauCeti.smallSingularCohomologyIso {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} {ι : Type u_2} (U : ι → Set ↑X) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (n : ℕ) : TopCat.singularCohomology R k M X n ≅ HomologicalComplex.homology (((X.smallSingularSubcomplex U).toSSet.chainComplex R).linearYonedaObj k M) n

The isomorphism on singular cohomology induced by restricting cochains to the chains subordinate to an open cover. It is dual to TauCeti.smallSingularHomologyIso.

@[simp]

theorem TauCeti.smallSingularCohomologyIso_hom {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} {ι : Type u_2} (U : ι → Set ↑X) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (n : ℕ) : (smallSingularCohomologyIso R k M U hU hcov n).hom = HomologicalComplex.homologyMap (SSet.cochainComplexMap (X.smallSingularSubcomplex U).ι) n

The small-chain cohomology isomorphism is the map induced by the inclusion of the singular simplices subordinate to the cover.

theorem TauCeti.quasiIso_cochainComplexMap_smallSingularSubcomplex_ι {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} {ι : Type u_2} (U : ι → Set ↑X) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) : QuasiIso (SSet.cochainComplexMap (X.smallSingularSubcomplex U).ι)

Restricting singular cochains to the chains subordinate to an open cover is a quasi-isomorphism, since the inclusion of those chains is a chain homotopy equivalence.

theorem TauCeti.smallSingularCohomologyIso_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} {ι : Type u_2} (U : ι → Set ↑X) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) {κ : Type u_3} {Y : TopCat} (V : κ → Set ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i))) (hV : ∀ (j : κ), IsOpen (V j)) (hcovV : ⋃ (j : κ), V j = Set.univ) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f n) (smallSingularCohomologyIso R k M U hU hcov n).hom = CategoryTheory.CategoryStruct.comp (smallSingularCohomologyIso R k M V hV hcovV n).hom (HomologicalComplex.homologyMap (SSet.cochainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf)) n)

The small-chain cohomology isomorphism is natural under maps carrying members of one cover into members of another.

noncomputable def TopCat.singularCohomologyMayerVietorisToBiprod {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) (n : ℕ) : TopCat.singularCohomology R k M X n ⟶ TopCat.singularCohomology R k M (↧↑U) n ⊞ TopCat.singularCohomology R k M (↧↑V) n

The first map Hⁿ(X) ⟶ Hⁿ(U) ⊞ Hⁿ(V) of the Mayer–Vietoris sequence in singular cohomology, with components the restrictions j_U^* and j_V^* along the inclusions.

@[simp]

theorem TopCat.singularCohomologyMayerVietorisToBiprod_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} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V n) CategoryTheory.Limits.biprod.fst = TopCat.singularCohomologyMap (ofHom (ContinuousMap.subtypeVal U)) n

@[simp]

theorem TopCat.singularCohomologyMayerVietorisToBiprod_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} (U V : Set ↑X) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M (↧↑U) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (ofHom (ContinuousMap.subtypeVal U)) n) h

@[simp]

theorem TopCat.singularCohomologyMayerVietorisToBiprod_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} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V n) CategoryTheory.Limits.biprod.snd = TopCat.singularCohomologyMap (ofHom (ContinuousMap.subtypeVal V)) n

@[simp]

theorem TopCat.singularCohomologyMayerVietorisToBiprod_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} (U V : Set ↑X) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M (↧↑V) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (ofHom (ContinuousMap.subtypeVal V)) n) h

noncomputable def TopCat.singularCohomologyMayerVietorisFromBiprod {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) (n : ℕ) : TopCat.singularCohomology R k M (↧↑U) n ⊞ TopCat.singularCohomology R k M (↧↑V) n ⟶ TopCat.singularCohomology R k M (↧↑(U ∩ V)) n

The second map Hⁿ(U) ⊞ Hⁿ(V) ⟶ Hⁿ(U ∩ V) of the Mayer–Vietoris sequence in singular cohomology, the difference i_U^* - i_V^* of the restrictions along the inclusions of U ∩ V. It is dual to the map (i_U, -i_V) of the homology sequence.

@[simp]

theorem TopCat.inl_singularCohomologyMayerVietorisFromBiprod {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (singularCohomologyMayerVietorisFromBiprod R k M U V n) = TopCat.singularCohomologyMap (ofHom (ContinuousMap.inclusion ⋯)) n

@[simp]

theorem TopCat.inl_singularCohomologyMayerVietorisFromBiprod_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} (U V : Set ↑X) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M (↧↑(U ∩ V)) n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisFromBiprod R k M U V n) h) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (ofHom (ContinuousMap.inclusion ⋯)) n) h

@[simp]

theorem TopCat.inr_singularCohomologyMayerVietorisFromBiprod {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (singularCohomologyMayerVietorisFromBiprod R k M U V n) = -TopCat.singularCohomologyMap (ofHom (ContinuousMap.inclusion ⋯)) n

@[simp]

theorem TopCat.inr_singularCohomologyMayerVietorisFromBiprod_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} (U V : Set ↑X) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M (↧↑(U ∩ V)) n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisFromBiprod R k M U V n) h) = CategoryTheory.CategoryStruct.comp (-TopCat.singularCohomologyMap (ofHom (ContinuousMap.inclusion ⋯)) n) h

@[simp]

theorem TopCat.singularCohomologyMayerVietorisToBiprod_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} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V n) (singularCohomologyMayerVietorisFromBiprod R k M U V n) = 0

@[simp]

theorem TopCat.singularCohomologyMayerVietorisToBiprod_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} (U V : Set ↑X) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M (↧↑(U ∩ V)) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V n) (CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisFromBiprod R k M U V n) h) = CategoryTheory.CategoryStruct.comp 0 h

The long exact sequence of an open cover by two sets

noncomputable def TopCat.singularCohomologyMayerVietorisδ {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 U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) : TopCat.singularCohomology R k M (↧↑(U ∩ V)) n ⟶ TopCat.singularCohomology R k M X m

The Mayer–Vietoris connecting morphism Hⁿ(U ∩ V) ⟶ Hᵐ(X) in singular cohomology, where n + 1 = m, for an open cover of X by U and V. It is the connecting morphism of the cochain Mayer–Vietoris sequence of the singular simplices lying in U, in V and in U or V, followed by the inverse of the restriction isomorphism from the cohomology of X.

@[simp]

theorem TopCat.singularCohomologyMayerVietorisδ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) (HomologicalComplex.homologyMap (SSet.cochainComplexMap (X.smallSingularSubcomplex ![U, V]).ι) m) = SSet.mayerVietorisCochainδ R k M ⋯ n m h

Followed by restriction to the singular simplices lying in U or in V, the Mayer–Vietoris connecting morphism is the connecting morphism of the cochain Mayer–Vietoris sequence of those simplices. Since that restriction is an isomorphism on cohomology, this characterizes it.

@[simp]

theorem TopCat.singularCohomologyMayerVietorisδ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : HomologicalComplex.homology (((X.smallSingularSubcomplex ![U, V]).toSSet.chainComplex R).linearYonedaObj k M) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (SSet.cochainComplexMap (X.smallSingularSubcomplex ![U, V]).ι) m) h✝) = CategoryTheory.CategoryStruct.comp (SSet.mayerVietorisCochainδ R k M ⋯ n m h) h✝

Followed by restriction to the singular simplices lying in U or in V, the Mayer–Vietoris connecting morphism is the connecting morphism of the cochain Mayer–Vietoris sequence of those simplices. Since that restriction is an isomorphism on cohomology, this characterizes it.

@[simp]

theorem TopCat.singularCohomologyMayerVietorisδ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) (singularCohomologyMayerVietorisToBiprod R k M U V m) = 0

@[simp]

theorem TopCat.singularCohomologyMayerVietorisδ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : TopCat.singularCohomology R k M (↧↑U) m ⊞ TopCat.singularCohomology R k M (↧↑V) m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) (CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisToBiprod R k M U V m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopCat.singularCohomologyMayerVietorisFromBiprod_δ {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 U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisFromBiprod R k M U V n) (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) = 0

@[simp]

theorem TopCat.singularCohomologyMayerVietorisFromBiprod_δ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : TopCat.singularCohomology R k M X m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisFromBiprod R k M U V n) (CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopCat.singularCohomologyMayerVietoris_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := TopCat.singularCohomology R k M (↧↑(U ∩ V)) n, X₂ := TopCat.singularCohomology R k M X m, X₃ := TopCat.singularCohomology R k M (↧↑U) m ⊞ TopCat.singularCohomology R k M (↧↑V) m, f := singularCohomologyMayerVietorisδ R k M hU hV hUV n m h, g := singularCohomologyMayerVietorisToBiprod R k M U V m, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence at Hᵐ(X).

theorem TopCat.singularCohomologyMayerVietoris_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n : ℕ) : { X₁ := TopCat.singularCohomology R k M X n, X₂ := TopCat.singularCohomology R k M (↧↑U) n ⊞ TopCat.singularCohomology R k M (↧↑V) n, X₃ := TopCat.singularCohomology R k M (↧↑(U ∩ V)) n, f := singularCohomologyMayerVietorisToBiprod R k M U V n, g := singularCohomologyMayerVietorisFromBiprod R k M U V n, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence at Hⁿ(U) ⊞ Hⁿ(V).

theorem TopCat.singularCohomologyMayerVietoris_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := TopCat.singularCohomology R k M (↧↑U) n ⊞ TopCat.singularCohomology R k M (↧↑V) n, X₂ := TopCat.singularCohomology R k M (↧↑(U ∩ V)) n, X₃ := TopCat.singularCohomology R k M X m, f := singularCohomologyMayerVietorisFromBiprod R k M U V n, g := singularCohomologyMayerVietorisδ R k M hU hV hUV n m h, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence at Hⁿ(U ∩ V).

theorem TopCat.mono_singularCohomologyMayerVietorisToBiprod_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) : CategoryTheory.Mono (singularCohomologyMayerVietorisToBiprod R k M U V 0)

The map H⁰(X) ⟶ H⁰(U) ⊞ H⁰(V) at the start of the Mayer–Vietoris sequence is a monomorphism.

theorem TopCat.singularCohomologyMayerVietorisδ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) {Y : TopCat} {U' V' : Set ↑Y} (hU' : IsOpen U') (hV' : IsOpen V') (hUV' : U' ∪ V' = Set.univ) (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU' hV' hUV' n m h) (TopCat.singularCohomologyMap f m) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (U ∩ V) (U' ∩ V') ⋯, continuous_toFun := ⋯ }) n) (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h)

Naturality of the Mayer–Vietoris connecting morphism. A map f : X ⟶ Y carrying U into U' and V into V' commutes with the connecting morphisms, where U ∩ V ⟶ U' ∩ V' is the restriction of f.

theorem TopCat.singularCohomologyMayerVietorisδ_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} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) {Y : TopCat} {U' V' : Set ↑Y} (hU' : IsOpen U') (hV' : IsOpen V') (hUV' : U' ∪ V' = Set.univ) (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : TopCat.singularCohomology R k M X m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU' hV' hUV' n m h) (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f m) h✝) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (U ∩ V) (U' ∩ V') ⋯, continuous_toFun := ⋯ }) n) (CategoryTheory.CategoryStruct.comp (singularCohomologyMayerVietorisδ R k M hU hV hUV n m h) h✝)

Naturality of the Mayer–Vietoris connecting morphism. A map f : X ⟶ Y carrying U into U' and V into V' commutes with the connecting morphisms, where U ∩ V ⟶ U' ∩ V' is the restriction of f.