singularTwoBoundaryFree_freeMk
plain-language theorem explainer
On the free singular chain complex of S¹, the explicit 2-boundary sends a free generator s to the alternating sum of its three face 1-simplices. Anyone evaluating free boundaries of cones, geodesics, or backtrack prisms cites this evaluation lemma. The proof is a one-line unfold of freeDesc on a generator.
Claim. For every singular $2$-simplex $s$ on $S^1$, the free-module boundary map applied to the free generator of $s$ equals $\mathrm{free}(\delta_0 s)-\mathrm{free}(\delta_1 s)+\mathrm{free}(\delta_2 s)$, the alternating sum of the three singular $1$-faces of $s$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1=\mathrm{TopCat.sphere},1$, and proves that displacement kills $2$-boundaries. That identity is the chain-level half of the injective comparison $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
A singular $2$-simplex is an element of the degree-$2$ object of the singular simplicial set of $S^1$. The free $2$- and $1$-chain modules are the free $\mathbb{Z}$-modules on those simplices. The map singularTwoBoundaryFree is defined by free-universal property: on a generator $s$ it is the alternating face sum $\delta_0 s-\delta_1 s+\delta_2 s$ in free $1$-chains (the classical singular boundary formula, written explicitly rather than via Mathlib's singular homology API).
Face operators $\delta_i$ are the simplicial-set face maps of $\mathrm{TopCat.toSSet.obj}(S^1)$. The companion geometric face construction on the project's own TwoSimplex type is the composition with the standard face maps of $\Delta^2$.
proof idea
One-line term/tactic wrapper. Rewrite by the definition of the free boundary (which is ModuleCat.freeDesc of the alternating-face formula) and apply ModuleCat.freeDesc_apply, which evaluates a free-descended map on a free generator. No geometric content is used.
why it matters
This is the evaluation lemma that every concrete free-boundary computation in the module reduces to. Downstream parents include the cone boundary shell (singularTwoBoundaryFree_freeMk_of_cone_faces: filling a loop by coning to a point), the geodesic composition law (..._linearSingularTwoSimplex: geodesics compose additively in $H_1$), path-backtrack and path-cone prism bricks, the constant-simplex degenerate case, and the free-to-chain boundary compatibility used in the kills-boundaries pipeline.
In the Recognition foundation stack this supports the hand-proved injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via the winding invariant (the covering-space argument that distinct integer multiples of the once-around loop are never homologous). Surjectivity/generation remains open and needs a prism/subdivision operator Mathlib does not yet supply. No direct T0–T8 forcing step, but the circle homology split is the topological backbone for the eight-tick and winding story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.