Local homology of a set as a colimit over its neighbourhoods

For a subset S of a space M, the relative singular homology Hₖ(M, M ∖ S) (TauCeti.localHomology) is approximated by the groups Hₖ(M, M ∖ K) of larger sets K ⊇ S, through the restriction maps Hₖ(M, M ∖ K) ⟶ Hₖ(M, M ∖ S). A singular simplex of M ∖ S has compact image. So when every compact set disjoint from S misses some member of a downward directed family of sets K ⊇ S, the subspaces M ∖ K exhaust M ∖ S in the sense of compact supports, and relative homology of the pair (M, M ∖ S) is the colimit of the relative homology of the pairs (M, M ∖ K) (TopPair.isColimitMapCoconeSingularHomology). With coefficients in a module this says two things:

• every class of Hₖ(M, M ∖ S) is the restriction of a class of some Hₖ(M, M ∖ K) (TauCeti.exists_localHomologyRestriction_eq);
• a class of Hₖ(M, M ∖ K) whose restriction to S vanishes already restricts to zero on some smaller member of the family (TauCeti.exists_localHomologyRestriction_eq_zero).

In a Hausdorff space compact sets are closed, so the neighbourhoods of any set A form such a family (TauCeti.exists_mem_nhdsSet_localHomologyRestriction_eq and TauCeti.exists_mem_nhdsSet_localHomologyRestriction_eq_zero). For a compact subset A of a manifold this is the compactness step in the computation of Hₖ(M, M ∖ A): it reduces statements about A to statements about neighbourhoods of A that are finite unions of compact convex sets in charts, the input to the fundamental class.

References

• A. Hatcher, Algebraic Topology, Section 3.3, the proof of Lemma 3.27.

theorem TauCeti.exists_localHomologyRestriction_eq {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) (k : ℕ) {M : Type w} [TopologicalSpace M] {S : Set M} {ι : Type w} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {K : ι → Set M} (hK : Antitone K) (hSK : ∀ (i : ι), S ⊆ K i) (hcpt : ∀ (T : Set M), IsCompact T → Disjoint T S → ∃ (i : ι), Disjoint T (K i)) (x : ↑(localHomology N S k)) : ∃ (i : ι) (y : ↑(localHomology N (K i) k)), (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) y = x

Local homology classes come from larger sets. If every compact set disjoint from S misses some member of a downward directed family of sets K i ⊇ S, then every class of Hₖ(M, M ∖ S) is the restriction of a class of some Hₖ(M, M ∖ K i).

theorem TauCeti.exists_localHomologyRestriction_eq_zero {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) (k : ℕ) {M : Type w} [TopologicalSpace M] {S : Set M} {ι : Type w} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {K : ι → Set M} (hK : Antitone K) (hSK : ∀ (i : ι), S ⊆ K i) (hcpt : ∀ (T : Set M), IsCompact T → Disjoint T S → ∃ (i : ι), Disjoint T (K i)) {i : ι} (y : ↑(localHomology N (K i) k)) (hy : (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) y = 0) : ∃ (j : ι) (hij : i ≤ j), (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) y = 0

Vanishing of local homology classes is detected on a smaller set. If every compact set disjoint from S misses some member of a downward directed family of sets K i ⊇ S, then a class of Hₖ(M, M ∖ K i) whose restriction to S vanishes already restricts to zero on some K j ⊆ K i.

theorem TauCeti.exists_mem_nhdsSet_localHomologyRestriction_eq {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) (k : ℕ) {M : Type w} [TopologicalSpace M] [T2Space M] {A : Set M} (x : ↑(localHomology N A k)) : ∃ (U : Set M) (hU : U ∈ nhdsSet A) (y : ↑(localHomology N U k)), (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) y = x

Local homology classes come from a neighbourhood. In a Hausdorff space, every class of Hₖ(M, M ∖ A) is the restriction of a class of Hₖ(M, M ∖ U) for some neighbourhood U of A.

theorem TauCeti.exists_mem_nhdsSet_localHomologyRestriction_eq_zero {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) (k : ℕ) {M : Type w} [TopologicalSpace M] [T2Space M] {A U : Set M} (hU : U ∈ nhdsSet A) (y : ↑(localHomology N U k)) (hy : (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N ⋯ k)) y = 0) : ∃ (V : Set M) (_ : V ∈ nhdsSet A) (hVU : V ⊆ U), (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction N hVU k)) y = 0

Vanishing of local homology classes is detected on a neighbourhood. In a Hausdorff space, a class of Hₖ(M, M ∖ U) for a neighbourhood U of A whose restriction to A vanishes already restricts to zero on some neighbourhood V ⊆ U of A.