singularHomologyFunctorSphereOneIntIsoHomologyOne
plain-language theorem explainer
Packages the definitional equality between Mathlib's singular homology of the circle in degree 1 (integer coefficients) and the degree-1 homology of the imported singular chain complex of S¹ as a canonical isomorphism. Downstream nonvanishing arguments cite it to transport zero/nonzero statements across that identification. The body is reflexivity of isomorphism.
Claim. There is a canonical isomorphism $$H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\;\cong\; H_1\bigl(C_\bullet^{\mathrm{sing}}(S^1;\mathbb{Z})\bigr)$$ between the value of Mathlib's singular homology functor at the topological 1-sphere and the degree-$1$ homology of the singular chain complex of that same space.
background
The module is a Mathlib-style workbench aimed at the classical computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace TopCat.sphere 1 and does not yet close the strict T8 bridge; it isolates the algebraic and chain-level atoms needed for that closure.
The upstream abbreviation sphereOneSingularIntChainComplex is exactly Mathlib's singular chain complex of the topological 1-sphere with coefficients in $\mathbb{Z}$-modules. Its degree-1 homology is the strict T8 target object. The singular homology functor applied in degree 1 to the same space is definitionally the homology of that complex; this declaration merely exposes that fact as an isomorphism rather than a bare equality.
Sibling lemmas in the file handle the purely algebraic core: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology isomorphic to $\mathbb{Z}$, and quasi-isomorphisms into that model transport the computation.
proof idea
One-line definitional wrapper: Iso.refl _. By construction of Mathlib's singularHomologyFunctor, evaluating it at degree 1 on $S^1$ is definitionally equal to taking homology in degree 1 of the singular chain complex of that space. No further lemmas or rewrites are required.
why it matters
Feeds the unconditional nonvanishing theorem circleH1ZNonzero_unconditional in CircleWindingChain. That parent states that Mathlib's circle $H_1$ object is nonzero, and discharges the claim by transporting a zero hypothesis across the inverse of this isomorphism into homologyOne_nonzero.
In the Recognition forcing chain this is infrastructure for the strict T-1-to-T8 frontier: T8 forces $D=3$ spatial dimensions, and the circle computation is the concrete Mathlib homology atom the bridge was waiting on. The nearby doc-comment is explicit that a degree-1 quasi-isomorphism from singular chains on $S^1$ to the ordinary cellular circle model is the remaining geometric bridge; this declaration only isolates the functor-versus-complex identification, not that geometric step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.