ordinaryCellularToReduced_comp_reducedCellularToOrdinary_f_one
plain-language theorem explainer
Composing the collapse ordinary→reduced with the inclusion reduced→ordinary yields the identity on the degree-1 chain group of the ordinary two-cell circle model. Anyone checking that the reduced single-degree model is a retract of the ordinary model in the degree that carries H₁ will cite this. The proof is a one-line simp of the two degree-1 component lemmas.
Claim. Let $C_\bullet$ be the ordinary two-cell cellular chain model of the circle ($\mathbb{Z}$ in degrees $0$ and $1$, zero differentials) and $R_\bullet$ the reduced model supported only in degree $1$. If $\varphi:C\to R$ collapses the degree-$0$ generator and $\psi:R\to C$ includes the degree-$1$ generator, then $(\varphi\circ\psi)_1=\mathrm{id}_{C_1}$.
background
The module is a Mathlib-style workbench aimed at the algebraic core of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace TopCat.sphere 1 or feed the strict T8 bridge; the first proved atom is that a chain complex supported by $\mathbb{Z}$ in degree $1$ has degree-$1$ homology $\mathbb{Z}$.
The ordinary cellular circle model places one integer generator in degree $0$ and one in degree $1$, with all boundaries zero. The reduced model keeps only the degree-$1$ generator (a single-complex). The collapse chain map $\varphi$ kills the degree-$0$ cell and retains the circle generator; the inclusion $\psi$ embeds the reduced model back into the ordinary one via the chosen integer-generator identification.
Upstream component lemmas record that in degree $1$, $\varphi_1$ is that identification (modulo the single-complex iso) and $\psi_1$ is its inverse. The composite $\psi\circ\varphi$ need not be $\mathrm{id}$ on the whole ordinary complex, because of the extra degree-$0$ generator; only degree $1$ matters for the circle homology computation.
proof idea
Term-level identity of chain-map components in degree $1$. Unfold the composite's degree-$1$ arrow and apply the two component lemmas ordinaryCellularToReducedChainMap_f_one and reducedCellularToOrdinaryChainMap_f_one. Those lemmas already express $\varphi_1$ and $\psi_1$ as a pair of mutually inverse isomorphisms (the ordinary $X_1\cong\mathbb{Z}$ iso composed with the single-complex unit/counit). A single simp cancels them to the identity on ordinaryCellularCircleChainModel.X 1.
why it matters
This is the degree-$1$ half of the retract relation between the ordinary two-cell model and the reduced single-degree model. Together with the companion quasi-isomorphism statement (collapse is a quasi-iso in degree $1$ via Mathlib's zero-differential short-complex criterion), it lets the workbench transfer the already-proved fact "$\mathbb{Z}$ in degree $1$ has $H_1\cong\mathbb{Z}$" from the reduced model back to the ordinary cellular model.
In the Recognition Science foundation stack this sits inside the Circle $H_1$ Computation workbench: the algebraic finite-chain model that must eventually be tied to Mathlib singular homology of $S^1$ before any strict T8 (three spatial dimensions / eight-tick octave) bridge can cite a fully formal $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No downstream consumers are wired yet; the lemma is infrastructure for that missing equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.