OneSimplex
plain-language theorem explainer
A singular 1-simplex on the circle is a continuous map from the standard topological 1-simplex Δ¹ into S¹. Anyone working with singular chains, winding numbers, or the H₁(S¹) ≅ ℤ comparison cites this type. It is a pure type abbreviation with no proof content.
Claim. Write $\mathrm{OneSimplex}$ for the type of continuous maps $C(\Delta^1,S^1)$, where $\Delta^1=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$ is the standard topological 1-simplex and $S^1$ is the carrier of $\mathrm{TopCat.sphere}\,1$.
background
The module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of the circle, then proves that displacement kills boundaries. That identity is the chain-level fact that makes winding a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
SphereOne is the carrier type of Mathlib's exact TopCat.sphere 1 object (no project-local replacement). The standard 1-simplex $\Delta^1$ is the convex set of barycentric coordinates on two vertices; continuous maps out of it are the singular 1-simplices used by singular homology.
Downstream, every closed-edge cone theorem and every zero-winding bounding statement is stated for maps of this type (or for the Mathlib singular simplex obtained by transporting them).
proof idea
Pure abbreviation: the type is definitionally equal to the Mathlib continuous-map type $C(\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2),,\mathrm{SphereOne})$. No tactics, no lemmas, no proof term beyond the type synonym.
why it matters
This is the working type for every singular-edge statement in CircleWindingChain. Parent results include the family of closed-edge cone theorems: closedSingularOneCycle_bounds_of_cone_map, closedSingularOneCycle_bounds_of_closed_cone_map, closedSingularOneCycle_bounds_of_continuous_coneCirclePoint, closedSingularOneCycle_bounds_of_zero_winding_coneCirclePoint, and the generation-shaped form closedSingularOneCycle_boundary_generate_of_zero_winding_coneCirclePoint. Those theorems turn zero simplexWinding into an explicit singular 2-chain boundary, which is the concrete half of the winding homomorphism being a left inverse to the fundamental class.
In the broader Recognition foundation this sits under the circle-winding chain that feeds the homology comparison for $S^1$; the module doc notes that the converse generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No T0–T8 forcing step is discharged here; the declaration is infrastructure for the topological side of that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.