Local homology of finite unions of convex sets in a chart

Let M be a Hausdorff space and φ : M → E an open partial homeomorphism to a real normed space of finite dimension n, such as a chart of a topological n-manifold. This file proves the finite-union case of Hatcher's Lemma 3.27: if L = φ.symm '' (K₁ ∪ ⋯ ∪ Kₘ) for compact convex sets Kᵢ ⊆ φ.target, then

• the local homology Hₖ(M, M ∖ L) vanishes for k > n (TauCeti.isZero_localHomology_symm_image_iUnion), and
• a morphism into Hₙ(M, M ∖ L) is determined by its composites with the restrictions to the local homology groups Hₙ(M, M ∖ {x}) at the points x ∈ L (TauCeti.localHomology_symm_image_iUnion_hom_ext).

With coefficients in a module, the second statement says that a class of Hₙ(M, M ∖ L) vanishes when its images in all Hₙ(M, M ∖ {x}), x ∈ L, vanish. These are the properties from which the fundamental class of a closed manifold is assembled.

The proof is Hatcher's induction on the number of convex pieces. For a single convex piece containing φ x, the restriction to x is an isomorphism (TauCeti.isIso_localHomologyRestriction_symm_image). The induction step applies the relative Mayer–Vietoris sequence of the complements of two closed sets A and B, ⋯ ⟶ Hₖ₊₁(M, M ∖ (A ∩ B)) ⟶ Hₖ(M, M ∖ (A ∪ B)) ⟶ Hₖ(M, M ∖ A) ⊞ Hₖ(M, M ∖ B) ⟶ ⋯, to A = L₁ ∪ ⋯ ∪ Lₘ₋₁ and B = Lₘ, where A ∩ B is again a union of m - 1 convex pieces of the same chart. The two consequences of that sequence used in the step hold for any closed sets: TauCeti.isZero_localHomology_union and TauCeti.localHomology_hom_ext_of_union.

References

• A. Hatcher, Algebraic Topology, Section 3.3, Lemma 3.27, steps (1) and (2) of its proof.

theorem TauCeti.isZero_localHomology_symm_image_iUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {M : Type w} [TopologicalSpace M] [T2Space M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (φ : OpenPartialHomeomorph M E) {n : ℕ} {ι : Type u_1} [Finite ι] {K : ι → Set E} (hn : Module.finrank ℝ E = n) (hK : ∀ (i : ι), Convex ℝ (K i)) (hKk : ∀ (i : ι), IsCompact (K i)) (hKφ : ∀ (i : ι), K i ⊆ φ.target) {k : ℕ} (hk : n < k) : CategoryTheory.Limits.IsZero (localHomology R (↑φ.symm '' ⋃ (i : ι), K i) k)

Local homology of a finite union of convex sets vanishes above the dimension (Hatcher, Lemma 3.27, finite-union case). Let φ : M → E be an open partial homeomorphism from a Hausdorff space to a real normed space of finite dimension n, and let L = φ.symm '' ⋃ i, K i for finitely many compact convex sets K i ⊆ φ.target. Then Hₖ(M, M ∖ L) vanishes for k > n.

theorem TauCeti.localHomology_symm_image_iUnion_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {M : Type w} [TopologicalSpace M] [T2Space M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (φ : OpenPartialHomeomorph M E) {n : ℕ} {ι : Type u_1} [Finite ι] {K : ι → Set E} (hn : Module.finrank ℝ E = n) (hK : ∀ (i : ι), Convex ℝ (K i)) (hKk : ∀ (i : ι), IsCompact (K i)) (hKφ : ∀ (i : ι), K i ⊆ φ.target) {T : C} {g₁ g₂ : T ⟶ localHomology R (↑φ.symm '' ⋃ (i : ι), K i) n} (h : ∀ (x : M) (hx : x ∈ ↑φ.symm '' ⋃ (i : ι), K i), CategoryTheory.CategoryStruct.comp g₁ (localHomologyRestriction R ⋯ n) = CategoryTheory.CategoryStruct.comp g₂ (localHomologyRestriction R ⋯ n)) : g₁ = g₂

Local homology of a finite union of convex sets is detected at points (Hatcher, Lemma 3.27, finite-union case). Let φ : M → E be an open partial homeomorphism from a Hausdorff space to a real normed space of finite dimension n, and let L = φ.symm '' ⋃ i, K i for finitely many compact convex sets K i ⊆ φ.target. Then a morphism into Hₙ(M, M ∖ L) is determined by its composites with the restrictions to Hₙ(M, M ∖ {x}) for x ∈ L.