homologyOneIsoIntOfQuasiIsoSingleDegreeOneIntComplex
plain-language theorem explainer
If a chain complex of abelian groups is quasi-isomorphic to the integer complex supported only in degree 1, then its first homology is isomorphic to ℤ. Anyone transporting H₁ from a finite circle chain model cites this. The body is a one-line wrapper around the degree-local quasi-iso transport.
Claim. Let $K$ be a chain complex of $\mathbb{Z}$-modules (shape $\mathbb{N}$ downward) and let $C$ be the complex with $\mathbb{Z}$ only in degree $1$ and $0$ elsewhere. If $f:K\to C$ is a quasi-isomorphism and $K$ has homology in every degree, then $H_1(K)\cong\mathbb{Z}$ as $\mathbb{Z}$-modules.
background
This module is the algebraic 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 imported singular homology is proved. The first proved atom is that a complex supported by $\mathbb{Z}$ in degree $1$ has degree-$1$ homology $\mathbb{Z}$.
The single-supported integer complex is that algebraic core: $\mathbb{Z}$ placed in degree $1$, zero elsewhere. The degree-local transport says that a morphism which is a quasi-isomorphism only at degree $1$ already yields $H_1(K)\cong\mathbb{Z}$. The present declaration packages the common global case: $f$ is a quasi-isomorphism in every degree and $K$ has homology everywhere, so the local hypothesis is automatic.
proof idea
One-line wrapper. It applies the degree-local transport (quasi-isomorphism at degree $1$ implies $H_1\cong\mathbb{Z}$) to the same morphism $f$. Global QuasiIso f plus homology in all degrees supplies the local QuasiIsoAt f 1 instance; the composite isomorphism is then the local one composed with the known $H_1$ of the single-supported complex.
why it matters
Gives the proposition-facing global transport used immediately by the nonempty-isomorphism theorem in the same module (existence of $H_1(K)\cong\mathbb{Z}$ under a global quasi-iso to the single-supported model). That nonempty form is the citation surface for later circle-chain arguments.
In the Recognition stack this sits in the algebraic core of the finite circle model, before topological transport to $S^1$. The module doc is explicit: nothing here yet closes the bridge to Mathlib singular homology or to T8 ($D=3$) / the eight-tick octave. It only locks the chain-level $H_1\cong\mathbb{Z}$ step once a global quasi-iso to the reduced model is in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.