closedSingularOneCycle_bounds_of_cone_map
plain-language theorem explainer
A closed continuous edge f : Δ¹ → S¹ bounds in singular homology once a continuous cone F : Δ² → S¹ is supplied whose base face is f and whose two lateral faces agree. Anyone building the zero-winding nullhomotopy into an actual 2-chain cites this handoff. The proof is a one-line transport through the singular-simplex-of-map functors into the already-proved cone-simplex bounding lemma.
Claim. Let $f : \Delta^1 \to S^1$ be continuous with equal endpoints on the two face maps of $\Delta^1$, and let $F : \Delta^2 \to S^1$ be continuous with base face $\partial_2 F = f$ and equal side faces $\partial_0 F = \partial_1 F$. Then there exists a singular $2$-chain $b$ in the integer singular chain complex of $S^1$ whose boundary is the closed singular $1$-cycle generated by $f$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. Together with the fact that the once-around loop has winding $1$, this yields a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
Here OneSimplex (resp. TwoSimplex) means a continuous map $\Delta^1\to S^1$ (resp. $\Delta^2\to S^1$). Faces of a $2$-simplex are obtained by precomposition with the standard face maps of $\Delta^2$. The object closedSingularOneCycle packages a closed singular edge (equal $\delta_0$ and $\delta_1$) as an actual degree-$1$ cycle in Mathlib's integer singular chain complex of $S^1$.
The immediate upstream lemma closedSingularOneCycle_bounds_of_cone_simplex already shows that a singular cone $2$-simplex over a closed edge witnesses that the corresponding cycle bounds. The present statement is the continuous-map packaging of that geometric handoff.
proof idea
One-line wrapper. Apply closedSingularOneCycle_bounds_of_cone_simplex to the singular $1$-simplex and singular $2$-simplex obtained by transporting $f$ and $F$ through singularOneSimplexOfMap and singularTwoSimplexOfMap. The two face hypotheses are discharged by rewriting with singularTwoSimplexOfMap_delta against the given base-face and equal-sides assumptions on $F$.
why it matters
This is the continuous-map form of the cone-filling handoff needed after a zero-winding nullhomotopy: once a conical extension $F:C(\Delta^2,S^1)$ with matching sides is built, the closed edge is homologous to zero in the actual chain complex. Downstream, closedSingularOneCycle_bounds_of_closed_cone_map further specializes to the endpoint-closed formulation that the nullhomotopy construction targets directly.
In the broader Recognition foundation this sits inside the strict computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the topological half of the T8 forcing chain (three spatial dimensions via the circle's fundamental class). The module doc notes that the split-injective half is already in hand via winding; the generation half still needs a simplicial prism/subdivision operator that Mathlib does not yet supply. This lemma closes the cone-geometry step on the bounding side without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.