homologyOneNonemptyIsoIntOfIsoSingleDegreeOneIntComplex
plain-language theorem explainer
If a chain complex of abelian groups is isomorphic to the single-supported integer complex in degree 1, then its first homology admits an isomorphism to ℤ. Algebraic topologists building the finite circle model for H₁(S¹; ℤ) cite this proposition-facing Nonempty form. The proof is a one-line wrapper that packages the underlying concrete isomorphism into a Nonempty witness.
Claim. Let $K$ be a chain complex of $\mathbb{Z}$-modules with downward shape on $\mathbb{N}$. If $K$ is isomorphic to the complex that is $\mathbb{Z}$ in degree $1$ and zero elsewhere, then the degree-$1$ homology of $K$ is nonempty-isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module.
background
This module is the local Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to Mathlib's singular homology object is proved. The first proved atom is algebraic: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The single-supported integer complex is the complex with $\mathbb{Z}$ placed only in degree 1 (and zero elsewhere). The sibling transport lemma states that any complex isomorphic to that model has degree-1 homology exactly $\mathbb{Z}$ as a module isomorphism, not merely up to nonempty existence. Homology is taken via the standard homology functor of homological complexes of $\mathbb{Z}$-modules.
proof idea
One-line term-mode wrapper. Apply the sibling transport lemma that, given an isomorphism $e:K\cong$ (single degree-1 integer complex), returns a concrete isomorphism between the degree-1 homology of $K$ and $\mathbb{Z}$. Package that isomorphism as the unique inhabitant of a Nonempty type via angle-bracket introduction. No further rewriting or homology computation is performed here.
why it matters
Proposition-facing form of the isomorphism transport lemma for the algebraic core of the finite circle chain model. Downstream consumers that only need existence of an isomorphism (rather than a chosen one) can cite this Nonempty variant. It sits inside the Circle $H_1$ workbench whose goal is $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, a standard topological fact required before any bridge from the reduced cellular circle model to Mathlib singular homology can close.
The module explicitly withholds feeding the strict T8 ($D=3$) bridge until that topological identification is proved. Used-by is currently empty, so this is a leaf convenience form for later quasi-isomorphism and cellular-model transport steps in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.