constantSingularOneSimplex_raw_boundary
plain-language theorem explainer
The differential of the constant singular 2-simplex at a point p on S¹, taken in Mathlib's integer singular chain complex, equals the raw degree-1 generator of the constant singular 1-simplex at p. Anyone proving that constant 1-cycles are boundaries, or that the winding chain map vanishes on constants, cites this. The proof transports the free-complex boundary identity across the free-to-raw comparison map.
Claim. For every point $p$ on $S^1$, the degree-$(2\to 1)$ differential of the integer singular chain complex of $S^1$, applied to the image of the free generator of the constant singular $2$-simplex at $p$, equals the raw coproduct inclusion of the constant singular $1$-simplex at $p$ evaluated at $1\in\mathbb{Z}$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of TopCat.sphere 1, and proves that winding kills boundaries. The key objects here are constant singular simplices: continuous maps from the standard simplex that send everything to a fixed point $p\in S^1$.
The free-chain identity constantSingularOneSimplex_free_boundary already states that the explicit free boundary of the constant $2$-simplex is the free generator of the constant $1$-simplex ("the degenerate base case of the null-homotopy prism construction"). The present theorem is the same fact after transport into Mathlib's actual singular chain complex sphereOneSingularIntChainComplex, whose degree-1 homology is the strict $H_1(S^1;\mathbb{Z})$ target.
Raw chains live in the coproduct of $\mathbb{Z}$ over singular simplices; free chains are the free module on those simplices. The comparison maps singularTwoChainFreeToChain and singularOneChainFreeToChain mediate between the two presentations.
proof idea
Term-mode transport of the free-complex identity. Apply rawBoundary_eq_of_singularTwoBoundaryFree_eq to the free generators of the constant $2$-simplex and constant $1$-simplex, feeding in constantSingularOneSimplex_free_boundary p as the free-boundary hypothesis. That lemma equates the raw differential of a free $2$-chain with the free-to-raw image of its free boundary. Rewrite the right-hand side with singularOneChainFreeToChain_freeMk so the free generator becomes the raw coproduct inclusion at coefficient $1$, and conclude.
why it matters
Constants must bound if winding is to be a homology invariant: a constant $1$-simplex is a cycle whose winding should be zero. Downstream, constantSingularOneCycle_bounds lifts this raw identity to the cycle-object level ("the constant closed singular $1$-cycle bounds the constant singular $2$-simplex"), and windingChainMap_constantSingularOneSimplex uses it directly to prove winding vanishes on constants ("each is the boundary of a constant singular $2$-simplex").
In the module's larger program this is the degenerate base of the kills-boundaries story that, together with pathWinding_fundamentalLoop sending the once-around generator to $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That isomorphism is the topological half of the T8 forcing of three spatial dimensions in the Recognition chain. The generation/surjectivity half still needs a simplicial prism operator Mathlib does not yet supply; this lemma closes only the constant/null-homotopy corner.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.