singularTwoSimplex_boundary_
plain-language theorem explainer
Raw chain-level boundary of a singular 2-simplex generator in C_*(S¹;ℤ): d₂ on the generator equals the alternating sum of its three singular 1-faces. Cited by anyone building the winding-kills-boundaries identity or an explicit prism for zero-winding cycles. Proof unfolds the alternating-face singular chain complex and normalizes the resulting three-term sum.
Claim. For every singular $2$-simplex $s$ on $S^1$, the degree-$2$ differential of the integer singular chain complex applied to the free generator of the $s$-summand equals $\iota(\delta_0 s)-\iota(\delta_1 s)+\iota(\delta_2 s)$, where $\iota$ embeds each singular $1$-simplex as a free $\mathbb{Z}$-generator of $C_1(S^1;\mathbb{Z})$ and $\delta_i$ are the face maps of the singular simplicial set of $S^1$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$, aiming at the chain-level fact that displacement vanishes on boundaries. A singular $2$-simplex is a continuous map $\Delta^2\to S^1$ (an object of the singular simplicial set in degree $2$); a singular $1$-simplex is likewise a map $\Delta^1\to S^1$.
The integer singular chain complex is built as the alternating-face complex of free $\mathbb{Z}$-modules on those simplices: generators are the simplices themselves, and $d_n$ is the signed sum of face maps. The present statement records that differential explicitly on a single free generator in degree $2$, before any winding invariant is applied.
Module goal: together with homotopy invariance and additivity of path displacement, the face formula yields $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$, the "winding kills boundaries" identity used for the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Term/tactic hybrid that never leaves the chain-complex definitions. Unfold the singular integer chain complex of $S^1$ down to the alternating-face complex and the constant-sigma presentation of free modules. Rewrite the differential via AlternatingFaceMapComplex.obj_d_eq, expand the degree-$2$ face sum over Fin 3, and evaluate the signs $(-1)^i$ (giving $+,-,+$). Push the coproduct inclusions through addition and negation, then finish by abelian normal form. No geometric input: pure simplicial-chain algebra.
why it matters
Doc-comment places this equality as the raw boundary step that the explicit prism construction for zero-winding cycles will invoke before applying any invariant. In the module narrative it is the algebraic face of the $2$-simplex telescoping that proves simplexDisplacement_boundary: displacement of the alternating face sum is zero, hence winding descends to homology.
That descent, paired with the fact that the fundamental loop has winding $1$, gives a left inverse to the fundamental class and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The surjective/generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No Recognition forcing-chain landmark (T0–T8, RCL, $\varphi$) is touched; this is pure foundational topology supporting later circle invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.