homologyOneIsoIntOfIsoSingleDegreeOneIntComplex
plain-language theorem explainer
Any chain complex of ℤ-modules isomorphic to the single degree-1 integer complex has first homology isomorphic to ℤ. Authors of the circle H₁ workbench cite this to transport the algebraic core once a finite circle model is identified with that single complex. The construction is a one-line composition of the homology functor on the given iso with the known self-homology iso of the single complex.
Claim. If $K$ is a chain complex of $\mathbb{Z}$-modules and $e : K \cong C$ where $C$ is the complex with $\mathbb{Z}$ concentrated in degree $1$ (and zero elsewhere), then $H_1(K) \cong \mathbb{Z}$ as objects of $\mathrm{Mod}_{\mathbb{Z}}$.
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 singular homology is proved. The first proved atom is algebraic: a complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The single degree-1 integer complex $C$ is (HomologicalComplex.single ... 1).obj (ModuleCat.of ℤ ℤ): $\mathbb{Z}$ in degree 1, zero elsewhere, under the downward $\mathbb{N}$-shaped complex shape. Its homology iso $H_1(C)\cong\mathbb{Z}$ is the Mathlib lemma singleObjHomologySelfIso packaged as singleDegreeOneIntComplexHomologyOneIsoInt.
The present declaration is the transport form of that atom: once any complex $K$ is identified with $C$ by an isomorphism of complexes, $H_1(K)$ is identified with $\mathbb{Z}$.
proof idea
One-line wrapper. Apply the degree-1 homology functor (as a functor on complexes of $\mathbb{Z}$-modules) to the given complex isomorphism $e:K\cong C$ via mapIso, obtaining $H_1(K)\cong H_1(C)$. Compose that iso (with ≪≫) with the upstream self-homology iso $H_1(C)\cong\mathbb{Z}$ from singleDegreeOneIntComplexHomologyOneIsoInt. No further case analysis or diagram chase.
why it matters
This is the transport lemma needed once a finite circle chain model is identified with the single degree-1 reduced model (doc-comment). Downstream it feeds homologyOneNonemptyIsoIntOfIsoSingleDegreeOneIntComplex, the proposition-facing Nonempty form of the same iso, which is the shape used in existence-style arguments in the workbench.
In the broader Recognition chain the target is $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as an algebraic atom toward the eight-tick / circle structure (T7) and the dimensional forcing path. The module doc is explicit that this workbench does not yet close the T8 bridge: no equivalence to Mathlib's imported singular homology of TopCat.sphere 1 is claimed here. The declaration only moves the algebraic core across complex isomorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.