Mayer–Vietoris for local homology

For closed subsets S and T of a space M, the relative Mayer–Vietoris sequence of the open sets M ∖ S and M ∖ T (TopCat.relativeMayerVietoris_exact₁) contains the segment Hₖ₊₁(M, M ∖ (S ∩ T)) ⟶ Hₖ(M, M ∖ (S ∪ T)) ⟶ Hₖ(M, M ∖ S) ⊞ Hₖ(M, M ∖ T) of local homology groups (TauCeti.localHomology).

Main results

• TauCeti.isZero_localHomology_union: for closed S and T, if Hₖ(M, M ∖ S), Hₖ(M, M ∖ T) and Hₖ₊₁(M, M ∖ (S ∩ T)) vanish, then so does Hₖ(M, M ∖ (S ∪ T)).
• TauCeti.localHomology_hom_ext_of_union: for closed S and T with Hₖ₊₁(M, M ∖ (S ∩ T)) = 0, maps into Hₖ(M, M ∖ (S ∪ T)) are determined by their restrictions to S and to T.
• TauCeti.exists_localHomologyRestriction_union_eq: with coefficients in a module, classes along closed sets S and T with the same restriction to S ∩ T are the restrictions of a single class along S ∪ T.

theorem TauCeti.isZero_localHomology_union {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {R : A} {M : Type w} [TopologicalSpace M] {S T : Set M} (hS : IsClosed S) (hT : IsClosed T) {k : ℕ} (hSk : CategoryTheory.Limits.IsZero (localHomology R S k)) (hTk : CategoryTheory.Limits.IsZero (localHomology R T k)) (h : CategoryTheory.Limits.IsZero (localHomology R (S ∩ T) (k + 1))) : CategoryTheory.Limits.IsZero (localHomology R (S ∪ T) k)

Vanishing of local homology along a union. For closed sets S and T, if Hₖ(M, M ∖ S), Hₖ(M, M ∖ T) and Hₖ₊₁(M, M ∖ (S ∩ T)) vanish, then so does Hₖ(M, M ∖ (S ∪ T)), by the relative Mayer–Vietoris sequence of the open sets M ∖ S and M ∖ T.

theorem TauCeti.localHomology_hom_ext_of_union {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {R : A} {M : Type w} [TopologicalSpace M] {S T : Set M} (hS : IsClosed S) (hT : IsClosed T) {k : ℕ} (h : CategoryTheory.Limits.IsZero (localHomology R (S ∩ T) (k + 1))) {Z : A} {f g : Z ⟶ localHomology R (S ∪ T) k} (hfS : CategoryTheory.CategoryStruct.comp f (localHomologyRestriction R ⋯ k) = CategoryTheory.CategoryStruct.comp g (localHomologyRestriction R ⋯ k)) (hfT : CategoryTheory.CategoryStruct.comp f (localHomologyRestriction R ⋯ k) = CategoryTheory.CategoryStruct.comp g (localHomologyRestriction R ⋯ k)) : f = g

Maps into local homology of a union are detected on the pieces. Let S and T be closed and let Hₖ₊₁(M, M ∖ (S ∩ T)) vanish. Two maps into Hₖ(M, M ∖ (S ∪ T)) that agree after restriction to S and to T are equal.

theorem TauCeti.exists_localHomologyRestriction_union_eq {M : Type w} [TopologicalSpace M] {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) {S T : Set M} (hS : IsClosed S) (hT : IsClosed T) {k : ℕ} (α : ↑(localHomology N S k)) (β : ↑(localHomology N T k)) (h : (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) α = (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) β) : ∃ (γ : ↑(localHomology N (S ∪ T) k)), (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) γ = α ∧ (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) γ = β

Local homology classes on two closed sets glue. Let S and T be closed. Classes of Hₖ(M, M ∖ S) and Hₖ(M, M ∖ T) with the same restriction to S ∩ T are the restrictions of a single class of Hₖ(M, M ∖ (S ∪ T)). This is exactness of the relative Mayer–Vietoris sequence at Hₖ(M, M ∖ S) ⊞ Hₖ(M, M ∖ T).