vertexPoint
plain-language theorem explainer
Extracts the actual point of S¹ carried by a singular 0-simplex: transport through the singular simplicial-set equivalence and evaluate at the unique vertex of Δ⁰. Cited wherever chain-level edges must meet path-level endpoints (oriented edge paths, cyclic winding sums, null-homotopies of zero-winding loops). Pure definitional unwrap of TopCat.toSSetObjEquiv at stdSimplex.vertex 0.
Claim. Given a singular $0$-simplex $v$ of $S^1$ (a $0$-simplex in the singular simplicial set of $\mathrm{TopCat.sphere}\,1$), $\mathrm{vertexPoint}(v)\in S^1$ is the image of the unique vertex of $\Delta^0$ under the continuous map $\Delta^0\to S^1$ corresponding to $v$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of the exact Mathlib sphere $S^1$, and proves that displacement kills boundaries of $2$-simplices. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
A singular $0$-simplex is an element of $(\mathrm{TopCat.toSSet.obj}(\mathrm{TopCat.sphere},1)).\mathrm{obj}(\Delta^0)^{\mathrm{op}}$: equivalently, a continuous map $\Delta^0\to S^1$. SphereOne is the carrier type of that sphere object. The standard $0$-simplex $\Delta^0$ has a single vertex $\mathrm{stdSimplex.vertex},0$, so evaluating the map there recovers the geometric point of $S^1$.
Downstream path constructions (singular and oriented edge paths) need those geometric endpoints to state connectivity of cyclic walks and to apply pathDisplacement / pathWinding.
proof idea
Definitional one-liner. Apply the equivalence $\mathrm{TopCat.toSSetObjEquiv}$ that turns a singular $0$-simplex into a continuous map $\Delta^0\to S^1$, then evaluate at the unique standard vertex of $\Delta^0$ (index $0:\mathrm{Fin},1$). No lemmas, no tactics.
why it matters
Endpoint bridge between singular chains and path geometry on $S^1$. Downstream: orientedEdgePath_zero / orientedEdgePath_one identify the $t=0,1$ values of an oriented edge path with vertexPoint of the oriented initial/terminal vertices; orientedWindingSum_cyclic_integral uses that identification to turn cyclic face-matching into path endpoint matching and conclude integer total winding; singularEdgePath_homotopicRel_const_of_loop_winding_zero needs the basepoint as a geometric $S^1$ point; OrientedCyclicFamilyTerm and the terminal-side correction generator close the generation half of the winding comparison.
In the module narrative this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (winding as left inverse to the fundamental class), complementary to pathWinding_fundamentalLoop. It does not itself touch the forcing chain T0–T8, but sits in the topological infrastructure that makes the eight-tick / circle recognition story rigorous in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.