sphereOneSingularIntChainComplexHasHomologyOne
plain-language theorem explainer
The singular integer chain complex of the circle $S^1$ admits a Mathlib homology object in degree 1. Anyone assembling the strict $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ target for the T8 bridge cites this existence fact. The proof is a one-line typeclass inference from Mathlib's homology infrastructure.
Claim. The singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$ has homology in degree $1$ (i.e., Mathlib can form the degree-$1$ homology object of that complex).
background
This module is a Mathlib-style workbench aimed at the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace 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 object in play is the imported singular chain complex of the topological circle: apply Mathlib's singular-chain-complex functor (coefficients in $\mathrm{ModuleCat},\mathbb{Z}$) to TopCat.sphere 1. That complex is the exact chain-level object whose degree-$1$ homology is the final strict T8 target.
In Mathlib, HasHomology n is the typeclass asserting that the homology object in degree $n$ can be formed for a given chain complex. The algebraic core already proved in this module is that a complex supported by $\mathbb{Z}$ only in degree $1$ has degree-$1$ homology $\mathbb{Z}$; the present declaration is the corresponding existence statement for the imported singular complex.
proof idea
One-line term proof: inferInstance. Mathlib's homology infrastructure already instances HasHomology 1 for the singular chain complex of any space in TopCat with coefficients in ModuleCat ℤ, so typeclass search discharges the goal with no further lemmas.
why it matters
The module doc and the following comment identify degree-$1$ homology of this imported singular complex as the final strict T8 singular-homology target. T8 in the forcing chain forces $D=3$ spatial dimensions; the circle computation is the 1-dimensional homology atom that the strict bridge must eventually match.
No downstream consumers are wired yet (used_by is empty). The declaration only guarantees that the homology object exists; sibling lemmas in the workbench handle isomorphisms from single-degree complexes and quasi-isomorphisms. Until a real equivalence (or quasi-iso) from a reduced cellular circle model to this singular complex is proved, the result stays off the T8 bridge path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.