The complement of an embedded sphere and the Jordan–Brouwer separation theorem

Let Y be a Hausdorff space in which the complement of every point has vanishing reduced homology, such as a sphere. If h : Sᵈ⁻¹ → Y is an embedding of the unit sphere of a d-dimensional real normed space, then the reduced homology of Y ∖ h(Sᵈ⁻¹) is that of Y shifted down by d: H_redᵢ(Y ∖ h(Sᵈ⁻¹)) ≅ H_redᵢ₊d(Y). For Y = Sⁿ this is the second half of Hatcher's Proposition 2B.1: the complement of an embedded k-sphere in Sⁿ has the reduced homology of an (n - k - 1)-sphere.

The sphere of a d-dimensional real normed space is homeomorphic to that of a Euclidean space of the same dimension (TauCeti.sphereHomeomorphOfFinrankEq), so it suffices to treat inner product spaces. The proof is then by induction on d. The unit sphere Sᵈ⁻¹ is empty when d = 0. Otherwise it is the union of the two closed hemispheres around a unit vector p, which meet in the equator, the unit sphere of (ℝ ∙ p)ᗮ. The hemispheres are discs (TauCeti.hemisphereHomeomorph), so the complements of their images are acyclic (TauCeti.isZero_reducedSingularHomologyFunctor_compl_range_closedBall). These two complements are open, their intersection is Y ∖ h(Sᵈ⁻¹) and their union is the complement of the image of the equator, so the Mayer–Vietoris sequence (TopCat.reducedMayerVietorisIsoOfIsZero) shifts degrees by one while lowering the dimension of the sphere by one.

In the top case of a sphere Sᵈ⁻¹ embedded in Sᵈ, the reduced homology of the complement in degree zero is one copy of the coefficients. With field coefficients, this says that the complement has exactly two path components: the Jordan–Brouwer separation theorem.

Main results

• TauCeti.reducedSingularHomologyComplRangeSphereIso: in a Hausdorff space Y whose point complements are acyclic, H_redᵢ(Y ∖ h(Sᵈ⁻¹)) ≅ H_redᵢ₊d(Y) for every embedding h of the unit sphere of a d-dimensional real normed space.
• TauCeti.isZero_reducedSingularHomologyFunctor_sphere_compl_range_sphere and TauCeti.reducedSingularHomologySphereComplRangeSphereIso: for Y = Sⁿ, the reduced homology of the complement of an embedded Sᵈ⁻¹ vanishes in degrees i ≠ n - d and is one copy of the coefficients in degree n - d.
• TauCeti.natCard_zerothHomotopy_sphere_compl_range_eq_two: the Jordan–Brouwer separation theorem: the complement of an embedded Sⁿ⁻¹ in Sⁿ has exactly two path components.

References

• A. Hatcher, Algebraic Topology, Section 2.B, Proposition 2B.1(b) and Corollary 2B.2.

noncomputable def TauCeti.reducedSingularHomologyComplRangeSphereIso {A : Type w} [Ring A] (M : ModuleCat A) {Y : Type w} [TopologicalSpace Y] [T2Space Y] (hY : ∀ (y : Y) (n : ℕ), CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor M n).obj ↧↑{y}ᶜ)) {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {h : ↑(Metric.sphere 0 1) → Y} (hc : Continuous h) (hi : Function.Injective h) (i : ℕ) : (reducedSingularHomologyFunctor M i).obj ↧↑(Set.range h)ᶜ ≅ (reducedSingularHomologyFunctor M (i + Module.finrank ℝ E)).obj ↧Y

The homology of the complement of an embedded sphere. Let Y be a Hausdorff space in which the complement of every point has vanishing reduced homology, and let h be a continuous injection into Y of the unit sphere of a real normed space of dimension d. Then H_redᵢ(Y ∖ h(Sᵈ⁻¹)) ≅ H_redᵢ₊d(Y), with coefficients in any module.

This is Hatcher, Algebraic Topology, Proposition 2B.1(b), in a general form. Like TauCeti.reducedSingularHomologySphereIso, the isomorphism depends on a chosen point of each sphere in the induction on the dimension, and is not a canonical identification.

Equations

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

theorem TauCeti.isZero_reducedSingularHomologyFunctor_sphere_compl_range_sphere {A : Type w} [Ring A] (M : ModuleCat A) {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {h : ↑(Metric.sphere 0 1) → ↑(Metric.sphere 0 1)} {n : ℕ} (hF : Module.finrank ℝ F = n + 1) (hc : Continuous h) (hi : Function.Injective h) {i : ℕ} (hin : i + Module.finrank ℝ E ≠ n) : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor M i).obj ↧↑(Set.range h)ᶜ)

The complement of an embedded sphere in a sphere is acyclic outside one degree. Let h be a continuous injection of the unit sphere of a finite-dimensional real normed space E into the unit sphere of an (n + 1)-dimensional one. Then the reduced homology of the complement of its image vanishes in every degree i with i + dim E ≠ n (Hatcher, Algebraic Topology, Proposition 2B.1(b)).

noncomputable def TauCeti.reducedSingularHomologySphereComplRangeSphereIso {A : Type w} [Ring A] (M : ModuleCat A) {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {h : ↑(Metric.sphere 0 1) → ↑(Metric.sphere 0 1)} {i : ℕ} (hF : Module.finrank ℝ F = i + Module.finrank ℝ E + 1) (hc : Continuous h) (hi : Function.Injective h) : (reducedSingularHomologyFunctor M i).obj ↧↑(Set.range h)ᶜ ≅ M

The complement of an embedded sphere in a sphere has the homology of a sphere. Let h be a continuous injection of the unit sphere of a finite-dimensional real normed space E into the unit sphere of a real normed space of dimension i + dim E + 1. Then the reduced homology of the complement of its image in degree i is one copy of the coefficients (Hatcher, Algebraic Topology, Proposition 2B.1(b)). Like TauCeti.reducedSingularHomologySphereIso, the isomorphism depends on chosen points, and is one choice of generator rather than a canonical identification.

Equations

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

theorem TauCeti.natCard_zerothHomotopy_sphere_compl_range_eq_two {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {h : ↑(Metric.sphere 0 1) → ↑(Metric.sphere 0 1)} (hEF : Module.finrank ℝ F = Module.finrank ℝ E + 1) (hc : Continuous h) (hi : Function.Injective h) : Nat.card (ZerothHomotopy ↑(Set.range h)ᶜ) = 2

The Jordan–Brouwer separation theorem. The complement of the image of a continuous injection of the unit sphere of a finite-dimensional real normed space E into the unit sphere of a real normed space of dimension dim E + 1 has exactly two path components (Hatcher, Algebraic Topology, Corollary 2B.2).