singularTwoSimplex_boundary_apply
plain-language theorem explainer
On the unit generator of a singular 2-simplex summand in Mathlib's integer singular chains of S¹, the degree-2 boundary equals the alternating face combination ι(δ₀s) − ι(δ₁s) + ι(δ₂s) in free C₁. Anyone computing H₁(S¹;ℤ) via free generators cites this elementwise form. The proof evaluates the morphism identity singularTwoSimplex_boundary_ι at 1, then simplifies with ModuleCat and LinearMap lemmas.
Claim. Let $s$ be a singular $2$-simplex of $S^1$. Write $C_\bullet(S^1;\mathbb{Z})$ for Mathlib's singular chain complex, and let $\iota_s(1)$ be the image of the unit $1\in\mathbb{Z}$ under the free-summand inclusion of $s$. Then $d_2(\iota_s(1))=\iota_{\delta_0 s}(1)-\iota_{\delta_1 s}(1)+\iota_{\delta_2 s}(1)$, where $\delta_i s$ are the three face $1$-simplices of $s$ in the singular simplicial set of $S^1$.
background
The module works at the chain level of Mathlib's singular homology of the topological circle. A singular 2-simplex is an element of the singular simplicial set in degree 2; a singular 1-simplex is the same in degree 1. The object sphereOneSingularIntChainComplex is the imported singular chain complex with integer coefficients whose H1 is the strict T8 target.
Free chains are assembled as coproducts of copies of Z, one summand per singular simplex, via Sigma inclusions. The differential d2 : C2 to C1 is Mathlib's alternating-face boundary. An upstream morphism-level identity already states that this differential, on the summand inclusion of s, equals the free alternating combination of the three face inclusions; the present theorem is that identity evaluated on the unit generator 1.
Locally the module's goal is the winding and displacement invariant on singular 1-simplices and the kills-boundaries identity: alternating face displacements of every singular 2-simplex vanish, so winding descends to homology.
proof idea
Term-mode evaluation of a prior morphism identity. Start from singularTwoSimplex_boundary_ι s, which equates the composite of the free-summand inclusion of s with d2 to the free alternating-face combination of the three face inclusions. Apply congrArg of the map sending a module morphism f to its value on 1, i.e. evaluate both sides on the unit of the Z summand. Discharge by simpa with the standard ModuleCat and LinearMap lemmas for composition, addition, subtraction, and negation. No new topology or face combinatorics is introduced here.
why it matters
Feeds directly into singularTwoChainFreeToChain_boundary_free, which states that Mathlib's singular C2 to C1 boundary, transported between the explicit free presentations of C2 and C1, is exactly the free alternating-face boundary. That transport bridges Mathlib's abstract singular complex and the concrete free generators on which the winding functional is defined.
In the module narrative this supports the chain-level winding-kills-boundaries fact and, with the once-around generator mapping to 1, the split-injective half of H1(S1;Z) isomorphic to Z. That isomorphism is the strict algebraic topology target tied to the T8 forcing step (D = 3 spatial dimensions via the circle's first homology). The generation half still needs a simplicial prism or subdivision operator that Mathlib's singular homology does not yet supply; this lemma does not close that gap, but it makes the free-boundary comparison usable elementwise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.