MathlibSingularHomologyAPIAvailable
plain-language theorem explainer
Records, as a Prop, that Mathlib exposes the singular homology functor for any suitable coefficient category and degree. Downstream bridge certificates cite it to pin every S¹ homology handoff to the real Mathlib API rather than a project-local stand-in. The body is a pure interface predicate: nonempty equality to AlgebraicTopology.singularHomologyFunctor.
Claim. The singular homology API is available when, for every category $C$ with coproducts, a preadditive structure, and homology, and for every degree $n\in\mathbb{N}$, there exists a functor $F:C\to\mathrm{Fun}(\mathbf{Top},C)$ equal to Mathlib's singular homology functor in degree $n$.
background
The module is the Mathlib Cohomology Bridge Contract. Mathlib already ships the singular homology functor API, but the T8 spatial-dimension forcing path still needs a Mathlib-backed computation of the reduced cohomology of $S^1$ and an Alexander-duality bridge from circle-complement homology to that group. The module deliberately refuses to fake that backend by reusing a project-local nontriviality lemma.
This definition is the import-checked surface those future computations must use. It quantifies over a coefficient category $C$ (with coproducts, preadditivity, and homology) and a degree $n$, and asserts that Mathlib's singularHomologyFunctor C n is present as a concrete functor $C\to\mathrm{Fun}(\mathbf{Top},C)$. It is not itself the $S^1$ computation.
Sibling objects in the same file name the concrete target circleH1Z as the degree-1 singular homology of the Mathlib sphere with $\mathbb{Z}$ coefficients, and package nonvanishing and $\mathbb{Z}$-isomorphism certificates around that object.
proof idea
Definitional, not a proof. The Prop is the universal statement that for every admissible coefficient category $C$ and every $n$, the subtype of functors equal to Mathlib's singular homology functor in degree $n$ is nonempty. Discharge is immediate in the companion theorem: introduce $C$ and $n$, then supply the Mathlib functor itself with rfl on the equality witness.
why it matters
This is the first gate in the cohomology bridge that will eventually replace the concrete $S^1$ encoding used in dimension forcing (T8: $D=3$). Every major certificate in the module requires it as a field: the final import interface for the missing $H_1(S^1;\mathbb{Z})$ computation, the checked target certificate pinning that object to $\cong\mathbb{Z}$, the linking backend that must route nonvanishing through the Mathlib circle homology object, and the top-level bridge contract that records API availability while leaving the linking backend as a named Nonempty target.
Without this predicate, later upgrades could silently swap in a project-local stand-in. With it, the only admissible surface is Mathlib's singular homology functor. The open work remains the actual Mathlib computation of $H_1(S^1;\mathbb{Z})$ and the Alexander-duality linking step; this definition only locks the API those steps must use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.