homologyOneNonemptyIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex
plain-language theorem explainer
If a ℤ-module chain complex maps by a degree-1 quasi-isomorphism to the single-supported integer complex, then its first homology is isomorphic to ℤ. Proposition-facing existence form of the degree-local transport; anyone needing Nonempty rather than an explicit iso cites this. One-line term proof that packages the constructive isomorphism.
Claim. Let $K$ be a chain complex of $\mathbb{Z}$-modules (shape $\mathrm{down}\,\mathbb{N}$) and let $f:K\to C$ be a morphism to the complex $C$ supported by $\mathbb{Z}$ in degree $1$. If $K$ has homology in degree $1$ and $f$ is a quasi-isomorphism at degree $1$, then there exists an isomorphism $H_1(K)\cong\mathbb{Z}$ of $\mathbb{Z}$-modules.
background
This module is the Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace TopCat.sphere 1 or feed the strict T8 bridge; the first proved atom is algebraic: a complex supported by $\mathbb{Z}$ in degree $1$ has degree-$1$ homology $\mathbb{Z}$.
The single-supported integer complex $C$ is the algebraic core of the finite circle chain model before topological transport. The sibling homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex builds the actual isomorphism $H_1(K)\cong\mathbb{Z}$ by composing isoOfQuasiIsoAt f 1 with the known homology of $C$. The present declaration is the proposition-facing packaging of that transport as mere existence of an iso.
proof idea
One-line term wrapper. The proof is the constructor of Nonempty applied to the constructive isomorphism homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex f, which already assumes HasHomology 1 and QuasiIsoAt f 1 and returns $K.\mathrm{homology},1\cong\mathrm{ModuleCat.of},\mathbb{Z},\mathbb{Z}$. No extra algebraic work.
why it matters
Fills the proposition-facing slot in the Circle $H_1$ workbench: existence of $H_1\cong\mathbb{Z}$ under a degree-local quasi-iso to the single-supported model. Downstream usage is not yet wired (used_by empty). It sits upstream of any future global quasi-iso transport to the reduced cellular circle chain model and, eventually, of a real equivalence to Mathlib singular homology of $S^1$. Until that bridge exists, the result does not enter the T8 ($D=3$) forcing chain; it only certifies the algebraic atom the topological step must hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.