constantOneSimplex
plain-language theorem explainer
The constant singular 1-simplex at a point p of the circle is the continuous map sending every point of the standard 1-simplex Δ¹ to p. It is the zero-displacement edge used throughout cone faces, geodesic self-identities, and oriented cyclic families on S¹. Anyone citing the chain-level winding invariant or the kills-boundaries identity needs this degenerate edge. The body is a one-line Mathlib constant continuous map.
Claim. For each point $p$ on the circle $S^1$, the constant singular $1$-simplex at $p$ is the continuous map $\Delta^1\to S^1$ with constant value $p$, where $\Delta^1$ is the standard topological $1$-simplex $\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$ and proves the chain-level fact that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $C(\Delta^1,S^1)$ from the standard topological $1$-simplex into the carrier of $\mathrm{TopCat.sphere},1$. Displacement of such an edge is path displacement after reparameterizing $\Delta^1$ to the unit interval. The constant edge is the fully degenerate case: no motion on the circle, hence zero winding.
Upstream, $S^1$ is the exact Mathlib sphere object; the constant map is Mathlib's ContinuousMap.const on that domain.
proof idea
One-line definition wrapper: the body is ContinuousMap.const applied to the standard $1$-simplex domain with value the given point of the circle. No lemmas, no tactics, no proof obligations beyond the type of continuous maps.
why it matters
This is the canonical zero edge in the singular-chain story for circle winding. Downstream, the $\delta_1$ face of the cone over a path equals the constant edge at the cone apex. When lifted endpoints of the base path agree, or when simplex winding vanishes, the terminal-return side of the cone collapses to this constant apex edge. A geodesic $1$-simplex with equal endpoints is definitionally this constant edge at the projected point. Oriented cyclic family terms also use it as a degenerate singular edge.
In the module's larger program, constant edges are the null contribution to displacement, so they sit under the kills-boundaries identity and under the left-inverse property of winding against the fundamental class. The generation (surjectivity) half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ remains open here, pending a simplicial prism or subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.