closedSingularOneCycle_bounds_of_cone_simplex
plain-language theorem explainer
A closed singular 1-simplex on S¹ that is the base face of a cone 2-simplex (side faces equal) generates a 1-cycle that bounds in the integer singular chain complex. Algebraic topologists computing H₁(S¹;ℤ) cite this as the geometric-to-chain handoff after a rel-endpoint nullhomotopy. The proof is a one-line term applying the free-boundary consumer to the free 2-chain built from the cone faces.
Claim. Let $s$ be a singular $1$-simplex on $S^1$ with equal $0$- and $1$-faces (a closed edge). Let $\sigma$ be a singular $2$-simplex whose base face $\delta_2\sigma$ equals $s$ and whose two side faces agree ($\delta_0\sigma=\delta_1\sigma$). Then there exists an integer singular $2$-chain $b$ whose image under the cycle map equals the closed singular $1$-cycle generated by $s$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. Together with the once-around generator mapping to winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A SingularOneSimplex (resp. SingularTwoSimplex) is an object of the singular simplicial set of TopCat.sphere 1 in degree $1$ (resp. $2$). The closed singular $1$-cycle packages a closed edge $s$ (equal endpoint faces) as a genuine cycle-object morphism into degree $1$ of Mathlib's integer singular chain complex of $S^1$.
Upstream, the free-boundary consumer states that if a closed edge is the explicit free boundary of a free $2$-chain, then the corresponding cycle-object generator is a toCycles boundary. The geometric task left is to build that free $2$-chain from a cone simplex.
proof idea
One-line term wrapper. It feeds the free $2$-chain ModuleCat.freeMk sigma and the face-identity lemma singularTwoBoundaryFree_freeMk_of_cone_faces (which checks that the free boundary of the cone generator is exactly the closed edge $s$, using the base-face and equal-sides hypotheses) into closedSingularOneCycle_bounds_of_free_boundary. That consumer discharges the existence of a degree-$2$ chain whose toCycles image is the closed singular $1$-cycle of $s$.
why it matters
This is the smallest geometric handoff after a rel-endpoint nullhomotopy of a winding-zero loop: once a cone $2$-simplex over the closed edge is constructed, the edge's cycle bounds in the actual singular chain complex. Downstream, closedSingularOneCycle_bounds_of_cone_map lifts the statement from simplicial-set objects to continuous maps $F:C(\Delta^2,S^1)$ with matching side faces, transporting through TopCat.toSSetObjEquiv.
In the module's program this feeds the generation/surjectivity half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the split-injective half already comes from winding killing boundaries plus the fundamental loop). The chain sits in the Foundation layer supporting the strict T8 target (three spatial dimensions via the circle's homology). No axioms or local $S^1$ replacements are used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.