singleDegreeOneIntComplexHomologyOneNonemptyIsoInt
plain-language theorem explainer
The degree-1 homology of the single-supported integer chain complex is inhabited as isomorphic to ℤ. Anyone packaging the algebraic core of H₁(S¹;ℤ) ≅ ℤ for the strict T8 bridge cites this Nonempty form. The proof is a one-line constructor wrapping the explicit Mathlib single-object homology isomorphism.
Claim. There is a nonempty type of $\mathbb{Z}$-module isomorphisms $$H_1\bigl(C_\bullet\bigr)\;\simeq\;\mathbb{Z},$$ where $C_\bullet$ is the chain complex of $\mathbb{Z}$-modules that is $\mathbb{Z}$ in degree $1$ and zero elsewhere (with the downward natural grading).
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\simeq\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 to that imported object is proved.
The algebraic atom underneath is the single-supported complex: place the integer module $\mathbb{Z}$ in degree 1 of a homological complex over ModuleCat ℤ with shape ComplexShape.down ℕ, and zero elsewhere. Mathlib supplies HomologicalComplex.singleObjHomologySelfIso, which identifies the homology in that unique nonzero degree with the module itself.
The sibling definition singleDegreeOneIntComplexHomologyOneIsoInt is exactly that isomorphism. Downstream transport lemmas need the weaker Nonempty (... ≅ ...) packaging so they can match the circleH1ZIsoInt pattern used by the T8 bridge.
proof idea
One-line term proof. The constructor of Nonempty is applied to the already-built isomorphism singleDegreeOneIntComplexHomologyOneIsoInt, which itself is the Mathlib lemma HomologicalComplex.singleObjHomologySelfIso specialized to shape down ℕ, degree 1, and object ModuleCat.of ℤ ℤ. No further rewriting or case analysis.
why it matters
Fills the proposition-facing atom of the circle $H_1$ computation: a complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$. The module doc states this is the first proved algebraic core of the finite circle chain model.
It matches the circleH1ZIsoInt Nonempty pattern required by the strict T8 bridge (forcing chain step T8: $D=3$ spatial dimensions, which leans on circle topology and the eight-tick octave). Sibling transport lemmas (homologyOneNonemptyIsoIntOfIso..., ...OfQuasiIso...) lift this fact along isomorphisms and quasi-isomorphisms once a reduced cellular circle chain model is identified with the single degree-1 complex.
No downstream consumers are wired yet (used_by empty). The open gap remains the real equivalence from the finite circle model to Mathlib singular homology of $S^1$, plus the still-open generation half of the winding-chain story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.