ordinaryCellularCircleChainModelXOneIsoInt
plain-language theorem explainer
The ordinary two-cell cellular chain model of the circle carries ℤ as its degree-1 chain group. This definition turns that definitional equality into a named isomorphism of ℤ-modules, so cycle and chain-map constructions can cite it without unfolding the piecewise complex. Anyone working the algebraic H₁(S¹;ℤ)≅ℤ core will use it. The body is a one-line eqToIso after simplifying the model.
Claim. There is a canonical isomorphism of $\mathbb{Z}$-modules $X_1 \cong \mathbb{Z}$ identifying the degree-$1$ chain group of the ordinary cellular circle chain model (one generator in degree $0$, one in degree $1$, zero differentials) with $\mathbb{Z}$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It builds finite algebraic chain models of the circle and does not yet replace Mathlib's TopCat.sphere 1 or feed the strict T8 bridge.
The ordinary cellular circle model is the two-cell complex with chain groups $\mathbb{Z}$ in degrees $0$ and $1$, zero elsewhere, and all boundaries zero. It remains an algebraic finite-chain model until a later theorem connects it to singular homology of the circle.
Degree-$1$ chain groups of such models are the raw material for cycle and homology isomorphisms; packaging $X_1\cong\mathbb{Z}$ as a named iso keeps later maps definitionally clean.
proof idea
One-line wrapper. Unfold the ordinary cellular circle model: its degree-$1$ object is definitionally ModuleCat.of ℤ ℤ. Apply eqToIso to that propositional equality, discharged by simp on the model definition. No homology or boundary lemmas are needed.
why it matters
Named generator identification for the ordinary cellular model. Downstream, the degree-$1$ cycles iso composes the inclusion-of-cycles iso with this map to conclude cycles in degree $1$ are $\mathbb{Z}$ (outgoing boundary zero). The ordinary-to-reduced and reduced-to-ordinary chain maps are built by mkHomToSingle / mkHomFromSingle using this iso's forward and inverse arrows; their degree-$1$ components are then identified with the single-complex unit/counit.
This sits in the algebraic core of the circle $H_1$ workbench (first proved atom: a complex supported by $\mathbb{Z}$ in degree $1$ has degree-$1$ homology $\mathbb{Z}$). It does not close the geometric bridge to Mathlib singular homology, nor the open generation half of the winding-class injectivity story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.