stdSimplex_simplyConnectedSpace
plain-language theorem explainer
For every positive integer n, the topological standard simplex in R^n is simply connected. The circle-winding development cites this as the monodromy hypothesis that lets path lifts of homotopic loops agree, so the winding number vanishes on boundaries. The proof is a one-line instance inference from convex contractibility already in Mathlib.
Claim. For every positive integer $n$, the standard simplex $\{ x \in \mathbb{R}^n : x_i \ge 0,\; \sum_i x_i = 1 \}$ is a simply connected space.
background
This module supplies the two lifting ingredients for the winding (degree) invariant on singular 1-chains of the circle TopCat.sphere 1. Singular simplices lift through the trigonometric covering of the circle; monodromy invariance of path lifts then forces the winding number to kill boundaries.
The domain of an n-simplex is the topological standard simplex stdSimplex R (Fin n), a nonempty convex subset of Euclidean space. Convex sets are contractible, and contractible spaces are simply connected. Mathlib already packages both facts as typeclass instances; the sibling registration of contractibility is the immediate prior step.
The consumer is path-lifting monodromy: if the base of a covering is simply connected, any two paths with the same endpoints are homotopic rel endpoints, so their lifts end at the same point in the total space. That is exactly the hypothesis needed to show displacements of faces of a 2-simplex telescope to zero.
proof idea
One-line term proof: inferInstance. Mathlib already knows that a nonempty convex set in a topological vector space is contractible, and that a contractible space is simply connected. With NeZero n ensuring the simplex is nonempty, the SimplyConnectedSpace instance on stdSimplex R (Fin n) resolves automatically. No local lemmas are unfolded.
why it matters
Registers the simply-connectedness hypothesis that the winding chain actually consumes. Downstream, simplexDisplacement_boundary instantiates this at n = 3 and concludes that for every singular 2-simplex the alternating sum of face displacements vanishes: the broken boundary walk is homotopic rel endpoints, inside the simply connected standard 2-simplex, to the direct edge.
That telescoping identity is the chain-level statement that the winding invariant kills boundaries, so it descends to homology. In the Recognition foundation this sits under the circle-covering setup tied to the T7 eight-tick / circle realization: the covering is the trig map on the circle, and simple connectedness of the simplex domain is what makes monodromy trivial on boundaries. Stated explicitly only for discoverability; instance search would find it anyway.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.