homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex
plain-language theorem explainer
If a chain complex of abelian groups maps by a degree-1 quasi-isomorphism to the complex supported by ℤ in degree 1, then its first homology is isomorphic to ℤ. Anyone transporting H₁ from a finite circle chain model cites this. The construction is the composite of Mathlib's quasi-iso-at-degree homology isomorphism with the known single-complex self-homology iso.
Claim. Let $K$ be a chain complex of $\mathbb{Z}$-modules (shape $\mathbb{N}$ downward) and let $S$ be the complex with $\mathbb{Z}$ supported only in degree $1$. If $f:K\to S$ is a quasi-isomorphism at degree $1$ and $K$ has homology in degree $1$, then $H_1(K)\cong\mathbb{Z}$ as $\mathbb{Z}$-modules.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace Mathlib's TopCat.sphere 1 singular homology, and it does not feed the strict T8 bridge until a real equivalence is proved.
The algebraic core is the single-supported integer complex $S$: the homological complex of $\mathbb{Z}$-modules with $\mathbb{Z}$ placed only in degree $1$. Its degree-1 homology is already identified with $\mathbb{Z}$ by the standard single-object self-homology isomorphism.
A quasi-isomorphism at a single degree induces an isomorphism on homology in that degree. The present definition packages that transport specifically against $S$ in degree $1$, so any complex quasi-isomorphic to $S$ at degree $1$ inherits $H_1\cong\mathbb{Z}$.
proof idea
One-line composite of two isomorphisms. First apply Mathlib's isoOfQuasiIsoAt f 1, which turns the degree-1 quasi-isomorphism hypothesis into $H_1(K)\cong H_1(S)$. Then right-compose with singleDegreeOneIntComplexHomologyOneIsoInt, the already-proved identification $H_1(S)\cong\mathbb{Z}$ coming from HomologicalComplex.singleObjHomologySelfIso. No further case analysis.
why it matters
This is the degree-local transport atom in the circle $H_1$ workbench. Downstream, the global form homologyOneIsoIntOfQuasiIsoSingleDegreeOneIntComplex simply specializes it under a full quasi-isomorphism (all degrees), and the proposition-facing nonempty wrapper packages existence of the iso for statement-level citations.
In the Recognition framework the target identity is $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, an algebraic prerequisite before any topological transport toward the eight-tick octave and the T8 forcing of $D=3$. The module doc is explicit that this workbench does not yet close that bridge: a real equivalence to Mathlib singular homology of the circle remains open. This definition closes only the algebraic quasi-iso transport step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.