TwoSimplex
plain-language theorem explainer
A singular 2-simplex on the circle is just a continuous map from the standard topological 2-simplex Δ² into S¹. Anyone working with singular chains, face maps, or cone fillings on the circle cites this type. It is a one-line type abbreviation, not a proved statement.
Claim. Write $\mathrm{TwoSimplex}$ for the type of continuous maps $C(\Delta^2, S^1)$, where $\Delta^2 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$ is the standard topological 2-simplex and $S^1$ is the carrier of $\mathrm{TopCat.sphere}\,1$.
background
The module lifts the path-level winding and displacement invariant from CircleWinding to singular simplices of the circle, then proves that displacement vanishes on boundaries. The key objects are singular 1-simplices (continuous maps $\Delta^1\to S^1$) and singular 2-simplices (continuous maps $\Delta^2\to S^1$).
Here $S^1$ is the abbreviation SphereOne for the carrier of Mathlib's exact TopCat.sphere 1. The standard 2-simplex $\Delta^2$ is Mathlib's stdSimplex ℝ (Fin 3): nonnegative barycentric coordinates on three vertices summing to 1. Continuous maps out of it are the geometric singular 2-simplices used throughout algebraic topology.
The sibling type for edges is the analogous continuous-map type on $\Delta^1$. Face maps, cone constructions, and the kills-boundaries identity all take values in, or consume, this 2-simplex type.
proof idea
Pure type abbreviation: TwoSimplex is defined to be C(stdSimplex ℝ (Fin 3), SphereOne), Mathlib's type of continuous maps from the standard 2-simplex into the circle. No proof obligations.
why it matters
This type is the ambient object for the chain-level winding story on $S^1$. Downstream, face extracts the three edge 1-simplices of a 2-simplex; simplexDisplacement_boundary states that the alternating face sum of displacements is zero (the telescoping homotopy inside the convex 2-simplex). Cone-filling theorems such as closedSingularOneCycle_bounds_of_cone_map and closedSingularOneCycle_bounds_of_closed_cone_map take a TwoSimplex whose base is a closed edge and whose side faces agree, then conclude the edge bounds in singular homology.
Together with the fact that path winding sends the once-around generator to 1, the kills-boundaries identity supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half still needs a simplicial prism or subdivision operator, which Mathlib singular homology does not yet provide. In the Recognition forcing chain this is foundation infrastructure for the circle's first homology, not a direct T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.