not_detects_zero
plain-language theorem explainer
No continuous embedding of a circle into the 0-sphere has nontrivial first singular homology of its complement. Cited by the low-dimension half of the D=3 linking uniqueness argument and by the public spine vanishing lemma at D=0. Proof: S⁰ is totally disconnected, every subspace inherits that, and H₁ of totally disconnected spaces vanishes.
Claim. There is no continuous embedding $f\colon S^{1}\hookrightarrow S^{0}$ such that the first singular homology (integer coefficients) of the complement $S^{0}\setminus\mathrm{im}(f)$ is nonzero.
background
This module is a Mathlib-only leaf that banks the vanishing of nontrivial linking detection in dimensions 0 and 1. The detector predicate (restated from PublicSpine) asserts: there exists a continuous map $f\colon S^{1}\to S^{D}$ that is a topological embedding and whose complement has nonvanishing first singular homology object linkingComplementH1.
In dimension 0 the ambient space is the unit sphere in $\mathbb{R}^{1}$, a two-point discrete space. Every subspace of a totally disconnected space is totally disconnected. Mathlib supplies that the singular homology functor in positive degree sends totally disconnected spaces to the zero object in ModuleCat ℤ.
The local goal is purely topological: rule out the detector at $D=0$ so the uniqueness half of the dimension-forcing bridge can treat 0 and 1 as unconditional banked cases.
proof idea
Assume an embedding $f\colon S^{1}\to S^{0}$ with nonvanishing complement $H_{1}$. Exhibit that TopCat.sphere 0 is totally disconnected by identifying it with the ULift of the metric unit sphere in Euclidean $\mathbb{R}^{1}$ (two points) and invoking the instance. The open complement subspace inherits total disconnectedness. Apply AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace at degree 1 (using one_ne_zero) to obtain that the complement homology is zero, contradicting the detector hypothesis.
why it matters
This is the unconditional $D=0$ bank for the linking half of spatial-dimension forcing (framework landmark T8: $D=3$). Downstream, forces_D3_of_arcAcyclic quotes it explicitly: dimensions 0 and 1 are the banked unconditional results from this module; granting arc-complement acyclicity for all $D\ge 2$, $D\ne 3$, nontrivial linking forces $D=3$. PublicSpine re-exports it as not_detectsNontrivialLinking_zero (campaign P-d3link, R3a): every subspace of the two-point $S^{0}$ is totally disconnected, so complement $H_{1}$ vanishes for any map. Together with the $D=1$ sibling it closes the low-dimension side of the uniqueness bridge without arc-frontier hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.