ordinaryCellularCircleChainModelH1NonemptyIsoInt
plain-language theorem explainer
The ordinary two-cell cellular chain model of the circle has first homology isomorphic to the integers, packaged as a Nonempty witness. Algebraic H1 certificates and circle-homology workbench consumers cite this proposition-facing form. The proof is a one-line wrapper that inhabits Nonempty with the already-built explicit isomorphism.
Claim. There exists an isomorphism of $\mathbb{Z}$-modules $$H_1(C_\bullet^{\mathrm{ord}})\cong\mathbb{Z},$$ where $C_\bullet^{\mathrm{ord}}$ is the ordinary two-cell cellular chain model of the circle (one $\mathbb{Z}$ generator in degree $0$, one in degree $1$, all boundaries zero).
background
This module is the local Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It develops finite algebraic chain models first and does not replace Mathlib's singular homology of the topological 1-sphere until a real equivalence is proved.
The ordinary cellular circle chain model places a single integer generator in degree 0 and one in degree 1, with vanishing differentials and no higher groups. Upstream: "This remains an algebraic finite-chain model until a later theorem connects it to Mathlib's TopCat.sphere 1."
A sibling definition already builds an explicit module isomorphism from that model's degree-1 homology to $\mathbb{Z}$. The present result only repackages that iso as a Nonempty existence claim, matching the shape expected by downstream certificate structures.
proof idea
One-line term proof: inhabit Nonempty by the existing isomorphism that identifies the ordinary model's first homology with $\mathbb{Z}$. That upstream iso is the composite of the homology-$\pi$ identification (using vanishing of the degree-2-to-1 differential) with the cycles-in-degree-1 iso onto $\mathbb{Z}$. No new chain-level algebra is done here.
why it matters
Supplies the ordinary half of cellularCircleAlgebraicH1Certificate, the checked certificate for "the finite cellular algebraic part of the circle-H1 computation" (the reduced half is the sibling Nonempty witness).
In the Recognition foundation stack this is an atom toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module doc is explicit that the workbench "does not feed the strict T8 bridge until a real equivalence to Mathlib's imported singular homology object is proved." T8 forces $D=3$ spatial dimensions; circle homology here is local algebraic scaffolding, not yet that bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.