singularHomologyFunctorSphereOneIntNonemptyIsoOfQuasiIsoAtOrdinaryCellular
plain-language theorem explainer
Conditional existence of an isomorphism $H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong\mathbb{Z}$ once a degree-1 quasi-isomorphism from Mathlib singular chains on the circle to the ordinary two-cell cellular model is given. Downstream bridge theorems cite this Nonempty packaging for MathlibCohomologyBridge. Proof is a one-line term wrapping the corresponding isomorphism into Nonempty.
Claim. Let $f$ be a chain map from the integer singular chain complex of $S^1$ to the ordinary cellular circle model ($\mathbb{Z}$ in degrees $0$ and $1$, zero differentials). Assume degree-$1$ homology exists and $f$ is a quasi-isomorphism at degree $1$. Then there exists an isomorphism $H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong\mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to Mathlib singular homology is proved. The algebraic core already known is that a chain complex supported by $\mathbb{Z}$ in degree $1$ has degree-$1$ homology $\mathbb{Z}$.
The ordinary cellular circle model is the finite complex with one integer generator in degree $0$, one in degree $1$, no higher groups, and zero boundary. The singular side is Mathlib's singular chain complex of $S^1$ with $\mathbb{Z}$ coefficients: the exact chain-level object whose degree-$1$ homology is the final strict T8 target.
Upstream, a degree-$1$ quasi-isomorphism from those singular chains to the ordinary cellular model already yields an explicit isomorphism of the singular-homology functor target with $\mathbb{Z}$, by composing the quasi-iso-induced homology iso with the cellular model's $H_1\cong\mathbb{Z}$.
proof idea
One-line term proof. It applies the upstream isomorphism (singular chains of $S^1$ to $\mathbb{Z}$, conditional on the same $f$, HasHomology 1, and QuasiIsoAt f 1) and packages that iso as a Nonempty witness via the angle-bracket constructor. No extra algebraic work: the composition isoOfQuasiIsoAt f 1 ≪≫ ordinaryCellularCircleChainModelH1IsoInt is already done upstream.
why it matters
Proposition-facing form of the conditional singular-homology iso. Its sole downstream consumer is circleH1ZIsoIntOfQuasiIsoAtOrdinaryCellular, which restates the same bridge in the exact proposition shape used by MathlibCohomologyBridge. The bridge file stays untouched until the chain-level quasi-isomorphism is proved unconditionally.
In the Recognition forcing chain this sits under the T8 spatial-dimension step: the circle's $H_1$ is the elementary topological atom that must match Mathlib before higher sphere and dimension arguments can be strict. The module deliberately isolates the remaining obligation as a single chain-level QuasiIsoAt f 1; everything after that (including this Nonempty packaging) is already proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.