ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1
plain-language theorem explainer
The ordinary two-cell cellular chain model of the circle and the reduced one-generator model have isomorphic first homology; the claim is packaged as a Nonempty witness rather than a bare isomorphism. Algebraic H₁(S¹) work cites this when assembling the finite-chain certificate. The proof is a one-line term that inhabits Nonempty with the already-constructed degree-1 iso.
Claim. There exists an isomorphism $H_1(C^{\mathrm{ord}}_\bullet) \cong H_1(C^{\mathrm{red}}_\bullet)$ of $\mathbb{Z}$-modules, where $C^{\mathrm{ord}}$ is the ordinary two-cell cellular chain model of the circle ($\mathbb{Z}$ in degrees $0$ and $1$, zero differential) and $C^{\mathrm{red}}$ is the reduced model ($\mathbb{Z}$ only in degree $1$).
background
This module is the Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It stays algebraic: finite chain models over $\mathrm{ModuleCat},\mathbb{Z}$, not yet a replacement for TopCat.sphere 1 or a feed into the strict T8 bridge.
The ordinary cellular circle chain model places one integer generator in degree $0$ and one in degree $1$, with all boundaries zero. The reduced model is the single-degree complex with $\mathbb{Z}$ only in degree $1$. Both are finite algebraic stand-ins for the circle until a later equivalence to singular homology is proved.
Upstream, an explicit isomorphism of degree-$1$ homology groups is already built by composing each model's iso to $\mathbb{Z}$ (ordinary then reduced, inverted). The present declaration only changes the packaging to a Nonempty witness of that iso.
proof idea
One-line term proof. The body is the angle-bracket constructor for Nonempty, applied to the already-defined isomorphism ordinaryCellularCircleChainModelH1IsoReducedCellularH1. That iso is itself the composite of the ordinary model's $H_1\cong\mathbb{Z}$ with the inverse of the reduced model's $H_1\cong\mathbb{Z}$. No new homology computation occurs here.
why it matters
Feeds the checked certificate cellularCircleAlgebraicH1Certificate, which bundles nonempty isos of both ordinary and reduced $H_1$ to $\mathbb{Z}$ as the finite cellular algebraic part of the circle-$H_1$ computation. The doc-comment marks this as the proposition-facing form of the bare iso: consumers that only need existence of an iso (certificate structures, Nonempty fields) cite this rather than the iso def.
In the broader Recognition stack this is scaffolding toward identifying algebraic circle homology with Mathlib singular homology, a prerequisite before any strict link to the eight-tick octave or T8 ($D=3$) topology bridge. It does not yet close that topological gap; it only stabilizes the algebraic comparison between the two finite models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.