sphereOneSingularIntChainComplex
plain-language theorem explainer
The singular chain complex of the topological circle S¹ with integer coefficients, taken directly from Mathlib. Anyone closing the strict T8 computation H₁(S¹; ℤ) ≅ ℤ cites this as the exact chain-level object whose degree-1 homology is the target. It is a one-line abbreviation applying Mathlib's singular chain complex functor to TopCat.sphere 1.
Claim. Write $C_*(S^1;\mathbb{Z})$ for the singular chain complex of the topological 1-sphere with coefficients in $\mathbb{Z}$, obtained by applying Mathlib's singular chain complex functor (valued in the category of $\mathbb{Z}$-modules) to $\mathrm{TopCat.sphere}\,1$.
background
This module is the local Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace $\mathrm{TopCat.sphere},1$ and does not feed the strict T8 bridge until a real equivalence to Mathlib's imported singular homology object is proved. The first proved atom in the file is algebraic: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
Singular chains are the free $\mathbb{Z}$-modules on continuous maps $\Delta^n\to X$, assembled into a chain complex via the usual face-boundary formula. Here $X$ is Mathlib's model of the 1-sphere. Upstream, the once-around singular 1-simplex (the geometric generator candidate) is already defined as a point of the singular simplicial set of that sphere; the present complex is the ambient chain object in which that simplex becomes a degree-1 chain.
Integer coefficients and the $\mathrm{ModuleCat},\mathbb{Z}$ enrichment match the conventions of the cohomology bridge that later packages the isomorphism $H_1\cong\mathbb{Z}$ for T8.
proof idea
Pure definitional abbreviation: apply Mathlib's singularChainComplexFunctor at coefficient category $\mathrm{ModuleCat},\mathbb{Z}$ (with the free module on $\mathbb{Z}$ as the coefficient object), then evaluate the resulting functor on $\mathrm{TopCat.sphere},1$. No tactics, no lemmas, no rewriting.
why it matters
This is the exact chain-level object whose degree-1 homology is the final strict T8 target (three spatial dimensions forced via the circle's first homology). Downstream, the geometric bridge is the proposition that this complex is chain-homotopy equivalent to the ordinary two-cell cellular circle model; several conditional theorems then turn a homotopy equivalence or a degree-1 quasi-isomorphism into the packaged isomorphism circleH1ZIsoInt used by the Mathlib cohomology bridge.
The fundamental degree-1 singular chain (coproduct summand inclusion of the once-around simplex) is typed against this complex, as is the statement that its boundary vanishes. Until the geometric bridge is discharged, the workbench stays local and does not yet close T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.