The Mayer–Vietoris sequence in singular homology

Let U and V be open subsets of a topological space X with U ∪ V = X, and let R be an object of an abelian category with coproducts. This file constructs the Mayer–Vietoris long exact sequence of singular homology with coefficients in R, ⋯ ⟶ Hₙ(U ∩ V) ⟶ Hₙ(U) ⊞ Hₙ(V) ⟶ Hₙ(X) ⟶ Hₙ₋₁(U ∩ V) ⟶ ⋯, whose first map is (i_U, -i_V) and whose second map is j_U + j_V, the i and j being the maps induced by the inclusions. The connecting morphism is natural in maps of covered spaces.

The construction is the one of Hatcher. For any two subsets U and V of X, the singular simplicial sets of U ∩ V, U and V form a pushout square with the subcomplex of singular simplices of X lying in U or in V (TopCat.isPushout_toSSet_inter_smallSingularSubcomplex), so the Mayer–Vietoris sequence of simplicial sets applies to it. When U and V are open and cover X, the small-chain theorem (TauCeti.smallSingularHomologyIso), which is also the core of the proof of excision, identifies the homology of that subcomplex with the singular homology of X.

Main definitions and results

• TopCat.isPushout_toSSet_inter_smallSingularSubcomplex: the pushout square of singular simplicial sets of an intersection.
• TopCat.mayerVietorisδ: the Mayer–Vietoris connecting morphism Hₙ(X) ⟶ Hₘ(U ∩ V), m + 1 = n, characterized by TopCat.homologyMap_ι_comp_mayerVietorisδ. The other two maps of the sequence are SSet.mayerVietorisToBiprod and SSet.mayerVietorisFromBiprod applied to the maps of singular simplicial sets induced by the inclusions.
• TopCat.mayerVietoris_exact₁, TopCat.mayerVietoris_exact₂, TopCat.mayerVietoris_exact₃: exactness at Hₘ(U ∩ V), at Hₙ(U) ⊞ Hₙ(V) and at Hₙ(X).
• TopCat.epi_mayerVietorisFromBiprod_zero: surjectivity at the degree-zero endpoint.
• TopCat.mayerVietorisδ_naturality: naturality of the connecting morphism.

References

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

theorem TopCat.isPushout_toSSet_inter_smallSingularSubcomplex {X : TopCat} (U V : Set ↑X) : CategoryTheory.IsPushout (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) (toSmallSingularSubcomplex ![U, V] ⋯) (toSmallSingularSubcomplex ![U, V] ⋯)

The singular simplicial sets of an intersection form a pushout square. For subsets U and V of X, the singular simplicial sets of U ∩ V, U and V form a pushout square with the subcomplex of singular simplices of X whose image lies in U or in V.

The Mayer–Vietoris sequence of an open cover by two sets

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

The Mayer–Vietoris connecting morphism Hₙ(X) ⟶ Hₘ(U ∩ V), where m + 1 = n, for an open cover of X by U and V. It is the connecting morphism of the Mayer–Vietoris sequence of the singular simplicial sets of U ∩ V, U and V, precomposed with the inverse of the small-chain isomorphism.

Equations

• TopCat.mayerVietorisδ R hU hV hUV n m h = CategoryTheory.CategoryStruct.comp (TauCeti.smallSingularHomologyIso R ![U, V] ⋯ ⋯ n).inv (SSet.mayerVietorisδ R ⋯ n m h)

@[simp]

theorem TopCat.homologyMap_ι_comp_mayerVietorisδ {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (X.smallSingularSubcomplex ![U, V]).ι R n) (mayerVietorisδ R hU hV hUV n m h) = SSet.mayerVietorisδ R ⋯ n m h

The Mayer–Vietoris connecting morphism of the open cover restricts, on the homology of the singular simplices lying in U or in V, to that of the pushout square of singular simplicial sets. Since that homology maps isomorphically onto Hₙ(X), this characterizes it.

@[simp]

theorem TopCat.homologyMap_ι_comp_mayerVietorisδ_assoc {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (toSSet.obj ↧↑(U ∩ V)).homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (X.smallSingularSubcomplex ![U, V]).ι R n) (CategoryTheory.CategoryStruct.comp (mayerVietorisδ R hU hV hUV n m h) h✝) = CategoryTheory.CategoryStruct.comp (SSet.mayerVietorisδ R ⋯ n m h) h✝

The Mayer–Vietoris connecting morphism of the open cover restricts, on the homology of the singular simplices lying in U or in V, to that of the pushout square of singular simplicial sets. Since that homology maps isomorphically onto Hₙ(X), this characterizes it.

@[simp]

theorem TopCat.mayerVietorisδ_toBiprod {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (mayerVietorisδ R hU hV hUV n m h) (SSet.mayerVietorisToBiprod R (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) m) = 0

@[simp]

theorem TopCat.mayerVietorisδ_toBiprod_assoc {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (toSSet.obj ↧↑U).homology R m ⊞ (toSSet.obj ↧↑V).homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (mayerVietorisδ R hU hV hUV n m h) (CategoryTheory.CategoryStruct.comp (SSet.mayerVietorisToBiprod R (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopCat.mayerVietorisFromBiprod_δ {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (SSet.mayerVietorisFromBiprod R (toSSet.map (ofHom (ContinuousMap.subtypeVal U))) (toSSet.map (ofHom (ContinuousMap.subtypeVal V))) n) (mayerVietorisδ R hU hV hUV n m h) = 0

@[simp]

theorem TopCat.mayerVietorisFromBiprod_δ_assoc {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (toSSet.obj ↧↑(U ∩ V)).homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.mayerVietorisFromBiprod R (toSSet.map (ofHom (ContinuousMap.subtypeVal U))) (toSSet.map (ofHom (ContinuousMap.subtypeVal V))) n) (CategoryTheory.CategoryStruct.comp (mayerVietorisδ R hU hV hUV n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopCat.mayerVietoris_exact₁ {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (toSSet.obj X).homology R n, X₂ := (toSSet.obj ↧↑(U ∩ V)).homology R m, X₃ := (toSSet.obj ↧↑U).homology R m ⊞ (toSSet.obj ↧↑V).homology R m, f := mayerVietorisδ R hU hV hUV n m h, g := SSet.mayerVietorisToBiprod R (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) m, zero := ⋯ }.Exact

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

theorem TopCat.mayerVietoris_exact₂ {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n : ℕ) : { X₁ := (toSSet.obj ↧↑(U ∩ V)).homology R n, X₂ := (toSSet.obj ↧↑U).homology R n ⊞ (toSSet.obj ↧↑V).homology R n, X₃ := (toSSet.obj ↧↑X).homology R n, f := SSet.mayerVietorisToBiprod R (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) (toSSet.map (ofHom (ContinuousMap.inclusion ⋯))) n, g := SSet.mayerVietorisFromBiprod R (toSSet.map (ofHom (ContinuousMap.subtypeVal U))) (toSSet.map (ofHom (ContinuousMap.subtypeVal V))) n, zero := ⋯ }.Exact

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

theorem TopCat.mayerVietoris_exact₃ {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (toSSet.obj ↧↑U).homology R n ⊞ (toSSet.obj ↧↑V).homology R n, X₂ := (toSSet.obj ↧↑X).homology R n, X₃ := (toSSet.obj ↧↑(U ∩ V)).homology R m, f := SSet.mayerVietorisFromBiprod R (toSSet.map (ofHom (ContinuousMap.subtypeVal U))) (toSSet.map (ofHom (ContinuousMap.subtypeVal V))) n, g := mayerVietorisδ R hU hV hUV n m h, zero := ⋯ }.Exact

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

theorem TopCat.epi_mayerVietorisFromBiprod_zero {X : TopCat} {U V : Set ↑X} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) : CategoryTheory.Epi (SSet.mayerVietorisFromBiprod R (toSSet.map (ofHom (ContinuousMap.subtypeVal U))) (toSSet.map (ofHom (ContinuousMap.subtypeVal V))) 0)

The map H₀(U) ⊞ H₀(V) ⟶ H₀(X) at the end of the Mayer–Vietoris sequence is an epimorphism.

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