reducedCellularToOrdinary_comp_ordinaryCellularToReduced
plain-language theorem explainer
The reduced cellular chain model of the circle is a retract of the ordinary two-cell model: including the degree-1 generator and then collapsing degree 0 recovers the reduced complex exactly. Anyone building the algebraic core of H₁(S¹; ℤ) ≅ ℤ cites this to justify working with the single-generator reduced complex. The proof is a one-step extension from the single-degree complex plus simplification of the degree-1 components.
Claim. The composite of the chain map from the reduced cellular circle complex into the ordinary cellular complex with the reverse collapse map equals the identity chain map on the reduced complex: $\mathrm{red}\to\mathrm{ord}\to\mathrm{red}=\mathrm{id}_{\mathrm{red}}$.
background
This module is a Mathlib-style 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 homology object, and it does not feed the strict T8 dimensional bridge until a real equivalence is proved. The first proved atom is algebraic: a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
Two finite cellular models of the circle appear. The reduced model is concentrated in degree 1 (a single $\mathbb{Z}$ generator, the loop). The ordinary model keeps an extra degree-0 cell. Chain maps go both ways: include the degree-1 generator into the ordinary complex, and collapse degree 0 to recover the reduced complex. The present statement records that the reduced model is a retract of the ordinary one at the chain level.
proof idea
Apply the Mathlib lemma that a morphism out of a single-degree homological complex is determined by its component in that degree (HomologicalComplex.from_single_hom_ext). Then simplify the degree-1 components of both chain maps; those components are definitionally inverse on the single $\mathbb{Z}$ generator, so the composite is the identity on the reduced complex.
why it matters
Inside the circle $H_1$ workbench this retract legitimizes computing with the reduced single-generator complex rather than the ordinary two-cell complex: homology in degree 1 is unaffected by the extra degree-0 cell. The module's first atom is that a complex supported by $\mathbb{Z}$ in degree 1 has $H_1\cong\mathbb{Z}$; the retract is the structural reason the reduced model is faithful for that computation.
Downstream the workbench aims at a real equivalence to Mathlib singular homology of $S^1$, which would eventually support the T8 forcing step ($D=3$) and related Recognition landmarks. No parent theorem is yet wired in the graph (zero used_by edges); the declaration is local infrastructure for that bridge, not a closed link into the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.