ordinaryCellularToReducedChainMap_f_one
plain-language theorem explainer
In degree 1, the ordinary-to-reduced cellular circle chain map acts as the identity on the chosen integer generator, up to the definitional single-complex isomorphism. Anyone assembling the algebraic core of H₁(S¹; ℤ) ≅ ℤ cites this component identity. The proof is a one-line simp that unfolds the chain-map constructor.
Claim. In degree $1$, the component of the chain map from the ordinary two-cell cellular circle model to the reduced degree-$1$ model equals the composite of the definitional isomorphism $X_1^{\mathrm{ord}} \cong \mathbb{Z}$ with the inverse of the single-object identification for the degree-$1$ complex supported on $\mathbb{Z}$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It builds finite cellular chain models of the circle and does not yet replace Mathlib's singular homology of TopCat.sphere 1, nor feed the strict T8 bridge.
The ordinary cellular circle model is a two-cell complex with chain group $\mathbb{Z}$ in degree 1 (via the definitional iso ordinaryCellularCircleChainModelXOneIsoInt) and a degree-0 generator. The reduced model is the single-degree complex supported by $\mathbb{Z}$ in degree 1. The ordinary-to-reduced chain map collapses the degree-0 generator and retains the degree-1 circle generator, built by HomologicalComplex.mkHomToSingle from that degree-1 iso.
The first proved atom of the module is that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$. Component identities such as this one make the collapse map usable in quasi-isomorphism and retract arguments.
proof idea
One-line tactic proof: simp unfolds the definition of the ordinary-to-reduced chain map. That definition is HomologicalComplex.mkHomToSingle applied to the degree-1 iso into $\mathbb{Z}$, so the degree-1 component is definitionally the stated composite with the single-object inverse. No further lemmas are required.
why it matters
This component identity is the degree-1 atom used by three parent results in the same module. It feeds the proof that the ordinary-to-reduced map is a quasi-isomorphism in degree 1 (via Mathlib's zero-differential short-complex criterion, with the middle component an iso on the integer generator). It also feeds both composition identities: the reduced model is a chain-level retract of the ordinary model, and the other composite is the identity in degree 1 (the degree relevant to circle homology), even though it need not be the identity on the full ordinary complex.
Within Recognition Science this sits in the Foundation layer supporting the circle $H_1$ computation workbench. The module doc is explicit that the workbench does not yet feed the strict T8 ($D=3$) bridge until a real equivalence to Mathlib singular homology is proved. Closing that bridge remains open; this lemma only locks the algebraic component of the collapse map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.