ordinaryCellularToReducedChainMap_quasiIsoAt_one
plain-language theorem explainer
The chain map that collapses the ordinary two-cell cellular model of the circle onto the reduced single-generator model induces a quasi-isomorphism in degree 1. Anyone assembling the algebraic certificate that both cellular models have H₁ ≅ ℤ cites this. The proof reduces to Mathlib's zero-differential short-complex criterion plus the fact that the degree-1 component is (definitionally) an isomorphism on the integer generator.
Claim. The chain map from the ordinary cellular circle complex to the reduced cellular circle complex (one $\mathbb{Z}$ generator in degree $1$, zero elsewhere) is a quasi-isomorphism at degree $1$: it induces an isomorphism on homology $H_1$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace Mathlib's TopCat.sphere 1 singular chains; the algebraic core is a finite cellular model that must later be transported geometrically.
Two chain complexes of $\mathbb{Z}$-modules appear. The ordinary cellular circle model has generators in degrees $0$ and $1$ with all differentials zero. The reduced model is the single-degree complex with chain group $\mathbb{Z}$ only in degree $1$. The collapse map retains the degree-$1$ generator and kills the degree-$0$ cell; in degree $1$ it is the identity on the chosen integer generator (modulo the single-complex isomorphism).
Upstream, all ordinary differentials vanish by definition, and the degree-$1$ component of the collapse is identified with the composite of the ordinary degree-$1$ isomorphism to $\mathbb{Z}$ with the inverse of the single-object identification.
proof idea
Rewrite quasi-isomorphism-at-$1$ as the short-complex map at degree $1$ being a quasi-isomorphism. Both source and target short complexes have zero differentials (ordinary differentials are definitionally zero; the reduced model is single-supported), so Mathlib's criterion reduces the claim to the lift-to-cycles map on the middle arrow being an isomorphism.
The target short complex has iso inclusion of cycles (outgoing differential zero). The composite of the lift-to-cycles with that inclusion equals the degree-$1$ component of the collapse map, which is an isomorphism by the degree-$1$ component lemma. Cancel the right factor to conclude the lift itself is an iso.
why it matters
This is one of the three algebraic legs of the finite cellular certificate for circle $H_1$. The downstream certificate packages: reduced $H_1\cong\mathbb{Z}$, ordinary $H_1\cong\mathbb{Z}$, the ordinary-to-reduced collapse being a quasi-isomorphism in degree $1$, and the reduced model as a chain retract of the ordinary one.
The module doc is explicit that the remaining Phase-5 gap is only geometric transport from Mathlib singular chains on the $1$-sphere to this cellular model. Until that equivalence lands, the result does not feed the strict T8 ($D=3$) bridge; it closes the purely algebraic half of the circle-homology atom that the forcing chain eventually needs for topological consistency of the eight-tick octave and spatial dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.