singleDegreeOneIntComplexHomologyOneIsoInt
plain-language theorem explainer
The degree-1 homology of the chain complex that places ℤ only in degree 1 is canonically isomorphic to ℤ as a ℤ-module. Anyone building a finite cellular model of the circle cites this as the algebraic atom. The proof is a one-line application of Mathlib's single-object homology self-isomorphism.
Claim. Let $C_\bullet$ be the homological complex of $\mathbb{Z}$-modules that is concentrated in degree $1$ with $C_1 = \mathbb{Z}$. Then $H_1(C_\bullet) \cong \mathbb{Z}$ as objects of $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is a local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace Mathlib's singular homology of the circle, and it does not feed the strict T8 bridge until a real equivalence to the imported singular object is proved.
The algebraic core is the single-supported complex: place the free module $\mathbb{Z}$ in degree 1 and zero elsewhere, with the standard downward complex shape on $\mathbb{N}$. Mathlib already knows that the homology of a single-object complex at its support degree recovers that object. The bridge certificate circleH1ZIsoInt is the proposition-facing target: nonempty isomorphism of the circle's first singular homology with $\mathrm{ModuleCat},\mathbb{Z},\mathbb{Z}$.
proof idea
One-line wrapper. Apply Mathlib's HomologicalComplex.singleObjHomologySelfIso at degree 1 for the complex shape down ℕ and the object ModuleCat.of ℤ ℤ. That lemma states that the homology of a single-supported complex at its support degree is canonically isomorphic to the supporting module, which is exactly the claim.
why it matters
This is the first proved atom of the circle $H_1$ workbench: the algebraic identity that any finite reduced cellular model of the circle must match. Downstream, it is transported along ordinary isomorphisms and along degree-local quasi-isomorphisms, and it is specialized to give $H_1$ of the reduced cellular circle chain model as $\mathbb{Z}$. The nonempty wrapper matches the circleH1ZIsoInt pattern used by the strict T8 bridge (forcing $D=3$ spatial dimensions via the eight-tick octave and related topology). Until a genuine equivalence to Mathlib singular homology is proved, this remains local scaffolding rather than a closed T8 input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.