singularOneSimplexChain_boundary_zero_of_faces_eq
plain-language theorem explainer
A singular 1-simplex on S¹ whose two endpoints coincide is a 1-cycle in the integer singular chain complex: the generator it defines has vanishing differential. Anyone building closed cycles from geometric loops on the circle cites this. The proof unfolds the alternating-face differential to endpoint-minus-endpoint and cancels by the equal-faces hypothesis.
Claim. Let $s$ be a singular $1$-simplex of $S^1$. If its two face maps agree ($\delta_0 s = \delta_1 s$), then the free $\mathbb{Z}$-generator of $s$ is sent to zero by the degree-$1$ differential of the singular chain complex $C_\bullet(S^1;\mathbb{Z})$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a homology invariant. A SingularOneSimplex is a point of the singular simplicial set of TopCat.sphere 1 in degree 1: a continuous map $\Delta^1\to S^1$.
The ambient complex is Mathlib's singular chain complex of $S^1$ with integer coefficients (sphereOneSingularIntChainComplex). Its differential in degree 1 is the alternating face map: for a generator $s$, $d_1(s)=\delta_0 s-\delta_1 s$ in free $C_0$. Equal faces therefore mean the two endpoint $0$-simplices cancel, so $s$ is a cycle.
This is the generator-level boundary-zero statement inside the actual singular complex, not a project-local model of $S^1$.
proof idea
Term/tactic hybrid that unfolds definitions rather than quoting a deep lemma. Expand sphereOneSingularIntChainComplex through the singular-chain and alternating-face functors, then rewrite the differential via AlternatingFaceMapComplex.obj_d_eq. On $\mathrm{Fin},2$ the alternating sum is $\delta_0-\delta_1$. After simplifying the coproduct inclusions (Sigma.ι_comp_map', identity compositions), the goal is exactly $\iota(\delta_0 s)-\iota(\delta_1 s)=0$. Substitute the hypothesis $\delta_0 s=\delta_1 s$ and cancel.
why it matters
Feeds closedSingularOneCycle, which packages a closed singular 1-simplex as an element of the degree-1 cycles of the singular complex via liftCycles. That is the concrete cycle object used when comparing geometric loops to homology classes.
In the module's program this is the generator half of "closed loops are cycles": together with simplexDisplacement_boundary (winding kills boundaries) and pathWinding_fundamentalLoop (once-around has winding 1), it supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module doc flags that isomorphism as the strict T8 target on the chain complex side. Surjectivity (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs prism/subdivision operators Mathlib does not yet supply; this lemma only closes the cycle-membership step for equal-endpoint generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.