singularHomologyFunctorSphereOneInt_eq_homologyOne
plain-language theorem explainer
The degree-1 singular homology of the circle S¹ with integer coefficients, as produced by Mathlib's singularHomologyFunctor, is definitionally identical to the degree-1 homology of the imported singular chain complex of TopCat.sphere 1. Anyone citing the strict T8 singular-homology target uses this identification. The proof is a one-line rfl, so the two presentations coincide by unfolding.
Claim. The object $H_1(S^1;\mathbb{Z})$ obtained by applying Mathlib's singular homology functor (coefficients in $\mathrm{Mod}\,\mathbb{Z}$, degree $1$) to the topological circle equals, by definition, the degree-$1$ homology module of the singular chain complex of $S^1$ with integer coefficients.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It keeps Mathlib's TopCat.sphere 1 as the geometric object and builds toward a strict bridge into the T8 forcing step (three spatial dimensions), without yet claiming a full replacement of Mathlib homology.
The upstream abbreviation sphereOneSingularIntChainComplex is exactly Mathlib's singular chain complex of the circle with $\mathbb{Z}$ coefficients: apply the singular chain-complex functor at $\mathrm{Mod},\mathbb{Z}$ to $S^1$. Its degree-1 homology is documented as "the final strict T8 target."
Singular homology in degree $n$ is the homology of that chain complex in degree $n$. Mathlib also packages the same construction as a functor singularHomologyFunctor valued in modules; the present statement equates the two presentations at $(S^1,1,\mathbb{Z})$.
proof idea
One-line definitional equality via rfl. Unfolding singularHomologyFunctor at coefficients $\mathrm{Mod},\mathbb{Z}$ and degree $1$, applied to $S^1$, is definitionally the same as taking .homology 1 of the abbreviated singular chain complex of the circle. No lemmas are invoked; the two sides are the same term after reduction.
why it matters
Strict T8 work needs a single, named object for $H_1(S^1;\mathbb{Z})$. This theorem pins Mathlib's functorial homology object to the chain-complex homology used everywhere else in the circle workbench, so later arguments can switch presentations without transport.
The immediate parent is homologyOne_nonzero in CircleWindingChain: that theorem proves $H_1(S^1;\mathbb{Z})$ is not the zero module by showing the fundamental loop class is nonzero (via the winding retraction to $\mathbb{R}$ and the mono half of the fundamental class). It reasons on sphereOneSingularIntChainComplex.homology 1; the present equality licenses reading the same nonvanishing as a statement about the functorial singular homology of the sphere.
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions. Circle homology is the algebraic seed for that dimensional argument; locking the target object definitionally removes a presentation gap before any generation or isomorphism theorems are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.