ordinaryCellularCircleChainModelXZeroIsoInt
plain-language theorem explainer
The ordinary two-cell cellular chain model of the circle carries chain group isomorphic to ℤ in degree 0. Anyone assembling the finite algebraic model of S¹ cites this iso as the degree-0 identification. The body is a one-line eqToIso after simp unfolds the piecewise definition of the model.
Claim. The degree-$0$ chain module of the ordinary cellular circle model is canonically isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module: $X_0 \cong \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 ordinary cellular circle model is the finite algebraic stand-in: one integer generator in degree 0, one in degree 1, vanishing higher groups, and zero differential. Explicitly, $X_n=\mathbb{Z}$ for $n=0,1$ and $0$ otherwise, with $d\equiv 0$. The first proved atom of the workbench is that a complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$; the present definition simply names the degree-0 chain group as $\mathbb{Z}$.
proof idea
One-line definitional wrapper. Unfold ordinaryCellularCircleChainModel by simp; the piecewise clause for $n=0$ is definitionally ModuleCat.of ℤ ℤ, so eqToIso turns the resulting equality of objects into the required isomorphism in ModuleCat ℤ.
why it matters
Names the degree-0 chain group of the ordinary cellular model as $\mathbb{Z}$, matching the companion fact that degree 1 is also $\mathbb{Z}$. Together these pin the algebraic skeleton used to compute $H_1$ of the finite circle model before any comparison with Mathlib singular homology.
Per the module doc, nothing here yet feeds the strict T8 ($D=3$) bridge or replaces TopCat.sphere 1. Downstream use sites are not yet wired (used_by empty). The injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (infinite order of the once-around loop) lives in the separate winding-chain development; surjectivity/generation remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.