reducedCellularToOrdinaryChainMap_f_one
plain-language theorem explainer
In degree 1, the chain map from the reduced cellular circle complex into the ordinary two-cell model equals the inverse of the chosen integer-generator identification, composed with the definitional single-object isomorphism. Anyone verifying the retract relation between reduced and ordinary circle chain models cites this atom. The proof is a one-line simp that unfolds the mkHomFromSingle construction.
Claim. In degree $1$, the chain map from the reduced cellular circle model to the ordinary cellular circle model equals the composition of the canonical single-complex component map (for shape $\mathrm{down}\,\mathbb{N}$ at degree $1$ on $\mathrm{Mod}(\mathbb{Z})$) with the inverse of the integer identification of the ordinary model's degree-$1$ chain group.
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 TopCat.sphere 1 singular homology object, nor feed the strict T8 bridge.
Two models sit side by side. The reduced cellular circle model is supported by a single $\mathbb{Z}$ in degree $1$. The ordinary cellular circle model is the two-cell complex with chain groups $\mathbb{Z}$ in degrees $0$ and $1$. The ordinary degree-$1$ group is identified with $\mathbb{Z}$ by a definitional isomorphism (eqToIso after unfolding).
The chain map in view includes the reduced model into the ordinary model by sending the degree-$1$ generator along that inverse identification, via HomologicalComplex.mkHomFromSingle. Degree $0$ of the ordinary model is not hit by this inclusion.
proof idea
One-line term proof: simp unfolds the definition of the reduced-to-ordinary chain map. That definition is exactly mkHomFromSingle applied to the inverse of the ordinary degree-$1$ integer identification, so the degree-$1$ component is definitionally the composite of the single-complex self-component with that inverse. No further lemmas are needed.
why it matters
This atom pins the degree-$1$ face of the inclusion so that two parent theorems can fire by simp. First, the reduced model is a retract of the ordinary model at chain level: include then collapse degree $0$ recovers the identity on the reduced complex. Second, the opposite composite is the identity in degree $1$ (the only degree that matters for circle $H_1$), even though it need not be id on the ordinary complex globally because of the extra degree-$0$ generator.
Together these establish that the algebraic core of the finite circle chain model has degree-$1$ homology $\mathbb{Z}$, the first proved atom toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module doc is explicit that this does not yet feed the strict T8 ($D=3$) bridge until a real equivalence to Mathlib singular homology is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.