homologyOneNonemptyIsoIntOfQuasiIsoSingleDegreeOneIntComplex
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 nonempty-isomorphic to ℤ. Algebraic topologists computing H₁(S¹; ℤ) via finite models cite this proposition-facing form. The proof is a one-line wrapper that inhabits Nonempty from the constructive isomorphism transport.
Claim. Let $K$ be a homological complex of $\mathbb{Z}$-modules indexed by $\mathbb{N}$ downward. If $f: K \to C_\bullet$ is a quasi-isomorphism onto the complex $C_\bullet$ that is $\mathbb{Z}$ in degree $1$ and zero elsewhere, and $K$ has homology in every degree, then there exists an isomorphism $H_1(K) \cong \mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$.
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 yet replace Mathlib's TopCat.sphere 1 singular object, and it does not feed the strict T8 dimensional bridge until a real equivalence is proved.
The algebraic core is the single-supported integer complex: the homological complex that places $\mathbb{Z}$ in degree 1 and zero elsewhere. Its degree-1 homology is definitionally $\mathbb{Z}$. Upstream, a global quasi-isomorphism transport lemma already builds an explicit isomorphism $H_1(K)\cong\mathbb{Z}$ whenever $K$ is quasi-isomorphic to that single-supported model in every degree.
This declaration is the proposition-facing packaging of that transport: it only asserts existence of the isomorphism (a Nonempty witness) rather than returning the iso term itself.
proof idea
One-line term proof. It applies the upstream constructive transport homologyOneIsoIntOfQuasiIsoSingleDegreeOneIntComplex to the given quasi-isomorphism $f$, then wraps the resulting isomorphism in an angle-bracket inhabitant of Nonempty. No extra algebraic work is done here; all homology and quasi-iso bookkeeping lives in the sibling that returns the actual iso.
why it matters
Inside Recognition Science this sits in the Foundation circle $H_1$ workbench, whose first proved atom is that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$. The present form is the existence-only face of global quasi-isomorphism transport onto that model, matching the doc-comment's "proposition-facing" role.
No downstream consumers are wired yet (used_by is empty). The module doc is explicit that the workbench does not feed the strict T8 bridge ($D=3$) until a genuine equivalence to Mathlib singular homology of the circle is established. The result therefore closes a local algebraic packaging step without yet touching the eight-tick octave or spatial-dimension forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.