singularOneSimplexChain_boundary_free
plain-language theorem explainer
For each singular 1-simplex s on S¹, the Mathlib degree-1 boundary of its free generator, transported into free C₀, equals freeMk(terminal face) minus freeMk(initial face). Anyone proving free-coordinate cycle decomposition or the free boundary formula on S¹ cites this. The proof unfolds the alternating-face differential and collapses the two-term Fin sum.
Claim. Let $s$ be a singular $1$-simplex on $S^1$. The composite of the coproduct inclusion of the generator at $s$, the singular boundary $d_1\colon C_1(S^1;\mathbb{Z})\to C_0(S^1;\mathbb{Z})$, and the transport of $C_0$ into the free $\mathbb{Z}$-module on singular $0$-simplices equals the free generator of the terminal $0$-face $\delta_0 s$ minus the free generator of the initial $0$-face $\delta_1 s$.
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 winding homomorphism on $H_1(S^1;\mathbb{Z})$. A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. The object sphereOneSingularIntChainComplex is Mathlib's singular chain complex of $S^1$ with integer coefficients; its degree-$1$ homology is the strict T8 target.
Raw $C_0$ is a coproduct of copies of $\mathbb{Z}$, one per singular $0$-simplex. The map singularZeroChainToFree sends each coproduct summand to the corresponding free generator of the explicit free module on singular $0$-simplices. Face maps $\delta_0,\delta_1$ extract the terminal and initial vertices of a $1$-simplex. The present lemma records the boundary of a single free $C_1$ generator in those free $C_0$ coordinates.
proof idea
Term-mode proof. Unfold the singular chain complex, the singular-chain functor, and the alternating-face complex; rewrite the differential via AlternatingFaceMapComplex.obj_d_eq. On degree $1\to 0$ the face sum is over Fin 2, so it collapses to $+\delta_0 - \delta_1$ after the usual sign rules (pow_zero, neg_zsmul). Simplify the simplicial face maps and the sigma-constant coproduct structure (Sigma.ι_comp_map'_assoc, id_comp). Rewrite through singularZeroChainToFree and apply Sigma.ι_desc twice. Finish by ModuleCat.hom_ext and LinearMap.ext_ring, reducing to the identity toSpanSingleton(a) - toSpanSingleton(b) = toSpanSingleton(a-b) on the free generators.
why it matters
This is the generator-wise cancellation surface for free-coordinate boundaries on $S^1$. The sole downstream consumer is singularOneChainFreeToChain_boundary_free, which extends the identity from one generator to the full free $C_1\to C_0$ boundary: "the Mathlib singular boundary, transported from explicit free $C_1$ to explicit free $C_0$, is the free boundary terminal minus initial."
Together with simplexDisplacement_boundary (winding kills $2$-boundaries) and the fundamental-loop normalisation, the free boundary formula is the finite-support bookkeeping needed for the remaining cycle-decomposition half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That isomorphism is the strict T8 landmark (three spatial dimensions via the circle's first homology). The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib does not yet supply; this lemma closes only the free-boundary identification step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.