The singular Mayer–Vietoris long exact sequence and connecting isomorphism

Building on the chain-level short exact sequence mvShortComplex_shortExact (file MayerVietorisSES.lean)

0 → C_*(U ∩ V) → C_*(U) ⊕ C_*(V) → C_*^{U,V}(X) → 0

and Mathlib's homology long exact sequence for a short exact sequence of homological complexes (ShortComplex.ShortExact.homology_exact₁/₂/₃ and the connecting map ShortComplex.ShortExact.δ), this file packages the singular Mayer–Vietoris exact sequence.

The key consequence used downstream (sphere homology, the project) is the connecting isomorphism: whenever the homology of C_*(U) and C_*(V) vanishes in the two relevant degrees (e.g. when U and V are contractible and the degrees are positive), the Mayer–Vietoris connecting map is an isomorphism

H_i(X) ≅ H_{i-1}(U ∩ V)

after using the small-simplices quasi-isomorphism of the project to replace the small-chain homology H_*(C_*^{U,V}(X)) by the singular homology H_*(X).

Main results

• SphereOddDegree.isIso_shortExact_δ — abstract homological-algebra input: for a short exact sequence of chain complexes, the connecting map δ : H_i(X₃) → H_j(X₁) is an isomorphism as soon as H_i(X₂) and H_j(X₂) both vanish.
• SphereOddDegree.mvHomology_exact_inter, mvHomology_exact_sum, mvHomology_exact_X — the three exactness statements of the Mayer–Vietoris sequence (re-exported from Mathlib for the two-set cover).
• SphereOddDegree.mvConnectingIso — the connecting isomorphism H_i(C_*^{U,V}(X)) ≅ H_j(U ∩ V) under the two vanishing hypotheses.
• SphereOddDegree.mvHomologyIso — the singular Mayer–Vietoris connecting isomorphism H_i(X) ≅ H_j(U ∩ V) (with i = j + 1), obtained by composing the small-simplices quasi-isomorphism with mvConnectingIso.
• SphereOddDegree.mvHomologyIsoSucc — the special case H_{n+1}(X) ≅ H_n(U ∩ V), the sphere-ready corollary.

Abstract homological-algebra inputs

theorem SphereOddDegree.isZero_biprod_of_isZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {A B : C} (hA : CategoryTheory.Limits.IsZero A) (hB : CategoryTheory.Limits.IsZero B) : CategoryTheory.Limits.IsZero (A ⊞ B)

A binary biproduct of two zero objects is a zero object.

theorem SphereOddDegree.isIso_shortExact_δ (R : Type) [CommRing R] {S : CategoryTheory.ShortComplex (ChainComplex (ModuleCat R) ℕ)} (hS : S.ShortExact) (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) (h2i : CategoryTheory.Limits.IsZero (HomologicalComplex.homology S.X₂ i)) (h2j : CategoryTheory.Limits.IsZero (HomologicalComplex.homology S.X₂ j)) : CategoryTheory.IsIso (hS.δ i j hij)

Connecting map is an isomorphism when the middle homology vanishes.

For a short exact sequence S of chain complexes (over ModuleCat R) and a relation c.Rel i j in the chain-complex shape, if the homology of the middle term S.X₂ vanishes in degrees i and j, then the Mayer–Vietoris-type connecting morphism S.δ i j : H_i(X₃) → H_j(X₁) is an isomorphism.

This is pure homological algebra: vanishing of H_i(X₂) forces δ to be a monomorphism (by exactness at H_i(X₃)), and vanishing of H_j(X₂) forces δ to be an epimorphism (by exactness at H_j(X₁)); ModuleCat R is balanced.

The Mayer–Vietoris short exact sequence and its homology

theorem SphereOddDegree.mvShortExact (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : (mvShortComplex R U V hUV).ShortExact

The Mayer–Vietoris short exact sequence of chain complexes for the cover {U, V} (re-export of mvShortComplex_shortExact).

theorem SphereOddDegree.mvHomology_exact_inter (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) : { X₁ := (mvShortComplex R U V hUV).X₃.homology i, X₂ := (mvShortComplex R U V hUV).X₁.homology j, X₃ := HomologicalComplex.homology (mvShortComplex R U V hUV).X₂ j, f := ⋯.δ i j hij, g := HomologicalComplex.homologyMap (mvShortComplex R U V hUV).f j, zero := ⋯ }.Exact

Exactness at H_n(U ∩ V) in the Mayer–Vietoris sequence: H_n(C_*^{U,V}(X)) →(δ) H_{n-1}(U ∩ V) →(incl) H_{n-1}(U) ⊕ H_{n-1}(V).

theorem SphereOddDegree.mvHomology_exact_sum (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (i : ℕ) : { X₁ := HomologicalComplex.homology (mvShortComplex R U V hUV).X₁ i, X₂ := HomologicalComplex.homology (mvShortComplex R U V hUV).X₂ i, X₃ := HomologicalComplex.homology (mvShortComplex R U V hUV).X₃ i, f := HomologicalComplex.homologyMap (mvShortComplex R U V hUV).f i, g := HomologicalComplex.homologyMap (mvShortComplex R U V hUV).g i, zero := ⋯ }.Exact

Exactness at H_n(U) ⊕ H_n(V) in the Mayer–Vietoris sequence: H_n(U ∩ V) → H_n(U) ⊕ H_n(V) → H_n(C_*^{U,V}(X)).

theorem SphereOddDegree.mvHomology_exact_X (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) : { X₁ := HomologicalComplex.homology (mvShortComplex R U V hUV).X₂ i, X₂ := HomologicalComplex.homology (mvShortComplex R U V hUV).X₃ i, X₃ := (mvShortComplex R U V hUV).X₁.homology j, f := HomologicalComplex.homologyMap (mvShortComplex R U V hUV).g i, g := ⋯.δ i j hij, zero := ⋯ }.Exact

Exactness at H_n(C_*^{U,V}(X)) in the Mayer–Vietoris sequence: H_n(U) ⊕ H_n(V) → H_n(C_*^{U,V}(X)) →(δ) H_{n-1}(U ∩ V).

theorem SphereOddDegree.isZero_mvX₂_homology (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (i : ℕ) (hU : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) i)) (hV : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) i)) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (mvShortComplex R U V hUV).X₂ i)

Vanishing of H_i(C_*(U)) and H_i(C_*(V)) implies vanishing of the middle homology H_i(C_*(U) ⊕ C_*(V)) of the Mayer–Vietoris sequence.

The connecting isomorphism

noncomputable def SphereOddDegree.mvConnectingIso (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) (hUi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) i)) (hVi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) i)) (hUj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) j)) (hVj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) j)) : HomologicalComplex.homology (twoOpenCoverSmallChains R U V hUV) i ≅ HomologicalComplex.homology (subChainComplex R X (↑U ∩ ↑V)) j

The Mayer–Vietoris connecting isomorphism on small-chain homology.

If the homology of C_*(U) and C_*(V) vanishes in degrees i and j (with c.Rel i j), the connecting map gives an isomorphism H_i(C_*^{U,V}(X)) ≅ H_j(U ∩ V).

Equations

• SphereOddDegree.mvConnectingIso R U V hUV i j hij hUi hVi hUj hVj = CategoryTheory.asIso (⋯.δ i j hij)

noncomputable def SphereOddDegree.mvHomologyIso (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) (hUi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) i)) (hVi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) i)) (hUj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) j)) (hVj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) j)) : HomologicalComplex.homology (AffineBarycentricSubdivision.singularChainComplex R X) i ≅ HomologicalComplex.homology (subChainComplex R X (↑U ∩ ↑V)) j

The singular Mayer–Vietoris connecting isomorphism.

Using the small-simplices quasi-isomorphism to replace the homology of the small-chain complex C_*^{U,V}(X) by the singular homology of X, the connecting map yields an isomorphism H_i(X) ≅ H_j(U ∩ V) whenever the homology of C_*(U) and C_*(V) vanishes in degrees i and j.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SphereOddDegree.mvHomologyIsoSucc (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (n : ℕ) (hUi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) (n + 1))) (hVi : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) (n + 1))) (hUj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑U) n)) (hVj : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex R X ↑V) n)) : HomologicalComplex.homology (AffineBarycentricSubdivision.singularChainComplex R X) (n + 1) ≅ HomologicalComplex.homology (subChainComplex R X (↑U ∩ ↑V)) n

Sphere-ready corollary. H_{n+1}(X) ≅ H_n(U ∩ V) whenever the homology of open Classical in C_*(U) and C_*(V) vanishes in degrees n + 1 and n (which holds, for instance, when U and V are contractible and 1 ≤ n). This is the form used in the inductive computation of sphere homology.

Equations

• SphereOddDegree.mvHomologyIsoSucc R U V hUV n hUi hVi hUj hVj = SphereOddDegree.mvHomologyIso R U V hUV (n + 1) n ⋯ hUi hVi hUj hVj