The reduced Mayer–Vietoris connecting morphism

Let U and V be open subsets of a topological space X with U ∪ V = X. The Mayer–Vietoris connecting morphism Hₖ₊₁(X) ⟶ Hₖ(U ∩ V) lands in the reduced homology of U ∩ V: in degree zero, it is killed by the map to H₀(U), which commutes with the augmentations. The resulting morphism TopCat.reducedMayerVietorisδ is natural in maps of covered spaces, and it is an isomorphism as soon as the reduced homology of U and of V vanishes in degrees k and k + 1, in particular when U and V are contractible.

This is the form in which the Mayer–Vietoris sequence computes the homology of a sphere from its cover by the complements of two antipodal points.

Coefficients are an object R of an abelian category with coproducts.

Main definitions and results

• TopCat.reducedMayerVietorisδ: the connecting morphism Hₖ₊₁(X) ⟶ H_redₖ(U ∩ V).
• TopCat.reducedMayerVietorisδ_comp_ι: it lifts the Mayer–Vietoris connecting morphism.
• TopCat.reducedMayerVietorisδ_naturality: naturality in maps of covered spaces.
• TopCat.isIso_reducedMayerVietorisδ: it is an isomorphism when U and V have vanishing reduced homology in the two adjacent degrees; TopCat.isIso_reducedMayerVietorisδ_of_contractible specializes this to contractible U and V.
• TopCat.eq_zero_of_comp_reducedSingularHomologyFunctor_map_inclusion: for open subsets A and B of a space with H_redₖ₊₁(A ∪ B) = 0, a class of A ∩ B in degree k vanishing in A and in B is zero, by exactness of the Mayer–Vietoris sequence at Hₖ(A ∩ B).
• TopCat.reducedMayerVietorisIsoOfIsZero: for open subsets A and B of a space with vanishing reduced homology in degrees k and k + 1, the isomorphism H_redₖ₊₁(A ∪ B) ≅ H_redₖ(A ∩ B).

References

• A. Hatcher, Algebraic Topology, Section 2.2, the reduced Mayer–Vietoris sequence.
• TopPair.reducedSingularHomologyδ for the connecting morphism in relative singular homology.

noncomputable def TopCat.reducedMayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (k : ℕ) : (toSSet.obj X).homology R (k + 1) ⟶ (TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑(U ∩ V)

The Mayer–Vietoris connecting morphism Hₖ₊₁(X) ⟶ H_redₖ(U ∩ V) of an open cover of X by U and V, into the reduced singular homology of the intersection. It lifts the Mayer–Vietoris connecting morphism through the inclusion of reduced into ordinary homology (TopCat.reducedMayerVietorisδ_comp_ι).

Equations

• One or more equations did not get rendered due to their size.
• TopCat.reducedMayerVietorisδ R hU hV hUV k.succ = CategoryTheory.CategoryStruct.comp (TopCat.δ✝ R hU hV hUV (k + 1)) ((TauCeti.reducedSingularHomologySuccIso R k).inv.app ↧↑(U ∩ V))

@[simp]

theorem TopCat.reducedMayerVietorisδ_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (k : ℕ) : CategoryTheory.CategoryStruct.comp (reducedMayerVietorisδ R hU hV hUV k) ((TauCeti.reducedSingularHomologyι R k).app ↧↑(U ∩ V)) = mayerVietorisδ R hU hV hUV (k + 1) k ⋯

The reduced Mayer–Vietoris connecting morphism followed by the inclusion of reduced into ordinary homology is the Mayer–Vietoris connecting morphism.

@[simp]

theorem TopCat.reducedMayerVietorisδ_comp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (k : ℕ) {Z : C} (h : ((AlgebraicTopology.singularHomologyFunctor C k).obj R).obj ↧↑(U ∩ V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (reducedMayerVietorisδ R hU hV hUV k) (CategoryTheory.CategoryStruct.comp ((TauCeti.reducedSingularHomologyι R k).app ↧↑(U ∩ V)) h) = CategoryTheory.CategoryStruct.comp (mayerVietorisδ R hU hV hUV (k + 1) k ⋯) h

The reduced Mayer–Vietoris connecting morphism followed by the inclusion of reduced into ordinary homology is the Mayer–Vietoris connecting morphism.

theorem TopCat.isIso_reducedMayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) {k : ℕ} (hU₁ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj ↧↑U)) (hV₁ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj ↧↑V)) (hU₀ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑U)) (hV₀ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑V)) : CategoryTheory.IsIso (reducedMayerVietorisδ R hU hV hUV k)

The reduced Mayer–Vietoris connecting morphism is an isomorphism when both open sets are acyclic in the adjacent degrees: if the reduced homology of U and of V vanishes in degrees k and k + 1, then Hₖ₊₁(X) ⟶ H_redₖ(U ∩ V) is an isomorphism.

instance TopCat.isIso_reducedMayerVietorisδ_of_contractible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) [ContractibleSpace ↑U] [ContractibleSpace ↑V] (k : ℕ) : CategoryTheory.IsIso (reducedMayerVietorisδ R hU hV hUV k)

The reduced Mayer–Vietoris connecting morphism of an open cover by two contractible sets is an isomorphism in every degree.

theorem TopCat.reducedMayerVietorisδ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : 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') (k : ℕ) : CategoryTheory.CategoryStruct.comp (reducedMayerVietorisδ R hU hV hUV k) ((TauCeti.reducedSingularHomologyFunctor R k).map (ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (U ∩ V) (U' ∩ V') ⋯, continuous_toFun := ⋯ })) = CategoryTheory.CategoryStruct.comp (SSet.homologyMap (toSSet.map f) R (k + 1)) (reducedMayerVietorisδ R hU' hV' hUV' k)

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

theorem TopCat.reducedMayerVietorisδ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : 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') (k : ℕ) {Z : C} (h : (TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑(U' ∩ V') ⟶ Z) : CategoryTheory.CategoryStruct.comp (reducedMayerVietorisδ R hU hV hUV k) (CategoryTheory.CategoryStruct.comp ((TauCeti.reducedSingularHomologyFunctor R k).map (ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (U ∩ V) (U' ∩ V') ⋯, continuous_toFun := ⋯ })) h) = CategoryTheory.CategoryStruct.comp (SSet.homologyMap (toSSet.map f) R (k + 1)) (CategoryTheory.CategoryStruct.comp (reducedMayerVietorisδ R hU' hV' hUV' k) h)

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

theorem TopCat.eq_zero_of_comp_reducedSingularHomologyFunctor_map_inclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {Y : TopCat} {A B D E : Set ↑Y} (hA : IsOpen A) (hB : IsOpen B) (hDA : D ⊆ A) (hDB : D ⊆ B) (hD : A ∩ B ⊆ D) (hE : A ∪ B = E) {k : ℕ} (hk : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj ↧↑E)) {P : C} (x : P ⟶ (TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑D) (hxA : CategoryTheory.CategoryStruct.comp x ((TauCeti.reducedSingularHomologyFunctor R k).map (ofHom (ContinuousMap.inclusion hDA))) = 0) (hxB : CategoryTheory.CategoryStruct.comp x ((TauCeti.reducedSingularHomologyFunctor R k).map (ofHom (ContinuousMap.inclusion hDB))) = 0) : x = 0

Injectivity in the Mayer–Vietoris sequence. Let A and B be open subsets of a space, and suppose that the reduced homology of A ∪ B vanishes in degree k + 1. Then a (generalized) reduced homology class of A ∩ B in degree k that vanishes both in A and in B is zero.

The intersection and the union are allowed to be given by any sets D and E equal to them.

noncomputable def TopCat.reducedMayerVietorisIsoOfIsZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {Y : TopCat} {A B D E : Set ↑Y} (hA : IsOpen A) (hB : IsOpen B) (hD : A ∩ B = D) (hE : A ∪ B = E) {k : ℕ} (hA₁ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj ↧↑A)) (hB₁ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj ↧↑B)) (hA₀ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑A)) (hB₀ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑B)) : (TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj ↧↑E ≅ (TauCeti.reducedSingularHomologyFunctor R k).obj ↧↑D

The reduced Mayer–Vietoris isomorphism of two acyclic open sets. Let A and B be open subsets of a space, and suppose that the reduced homology of A and of B vanishes in degrees k and k + 1. Then the reduced Mayer–Vietoris connecting morphism of the cover of A ∪ B by A and B (TopCat.reducedMayerVietorisδ) is an isomorphism H_redₖ₊₁(A ∪ B) ≅ H_redₖ(A ∩ B).

The intersection and the union are allowed to be given by any sets D and E equal to them.

Equations

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