ordinaryCellularCircleChainModelCyclesOneIsoInt
plain-language theorem explainer
Degree-1 cycles in the ordinary two-cell cellular chain model of the circle are isomorphic to ℤ as ℤ-modules. Anyone computing algebraic H₁ of that finite model cites this before passing from cycles to homology. The proof composes the cycles-equals-chains iso (outgoing boundary vanishes) with the identification of the degree-1 chain group with ℤ.
Claim. There is a canonical isomorphism of $\mathbb{Z}$-modules $$Z_1(C_\bullet^{\mathrm{ord}}) \cong \mathbb{Z},$$ where $C_\bullet^{\mathrm{ord}}$ is the ordinary two-cell cellular chain complex of the circle (one generator in degree $0$, one in degree $1$, zero differentials) and $Z_1$ denotes its module of degree-$1$ cycles.
background
The Circle H₁ Computation workbench targets the missing algebraic fact $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Per the module doc, it does not replace Mathlib's TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to imported singular homology is proved. The first atom is purely algebraic: a complex supported by ℤ in degree 1 has degree-1 homology ℤ.
The ordinary cellular circle model is a HomologicalComplex over ModuleCat ℤ with shape down ℕ: chain groups equal ℤ in degrees 0 and 1, vanish elsewhere, and every differential is the zero map. The degree-1 chain group is identified with ℤ by the sibling iso ordinaryCellularCircleChainModelXOneIsoInt. All differentials are definitionally zero (ordinaryCellularCircleChainModel_d_eq_zero).
Cycles in degree n are the kernel of the outgoing differential. When that map is zero, cycles equal the whole chain group.
proof idea
One-line composite of two isomorphisms. Apply the complex's built-in iCyclesIso at degree 1 toward index 0: the side condition ordinaryCellularCircleChainModel_d_eq_zero 1 0 makes the outgoing boundary vanish, so the inclusion of cycles into chains is an iso. Compose (≪≫) with ordinaryCellularCircleChainModelXOneIsoInt, which rewrites the degree-1 chain group as ModuleCat.of ℤ ℤ. No further diagram chase is needed.
why it matters
This is the cycles half of the algebraic H₁ computation for the ordinary two-cell model. Downstream, ordinaryCellularCircleChainModelH1IsoInt builds first homology as cycles modulo boundaries: it takes the inverse of the homology-projection iso (incoming boundary from degree 2 also zero) and composes with this cycles iso, yielding homology 1 ≅ ℤ.
That parent definition is the module's stated first proved atom. Relative to the broader Recognition framework it remains pre-topological scaffolding: the module doc explicitly withholds any claim on Mathlib singular homology of the circle and on the strict T8 bridge. The separate winding-chain has class already gives the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via covering-space winding; surjectivity (generation by the fundamental loop) stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.