SingularZeroSimplex
plain-language theorem explainer
Names the type of singular 0-simplices of the topological circle S¹: continuous maps Δ⁰ → S¹, i.e. points of S¹ in the singular simplicial set. Downstream free-chain and incidence-sum lemmas treat this type as the vertex set of singular 1-chains. The body is a one-line Mathlib unpack of Sing(S¹)₀.
Claim. Write $\mathrm{Sing}(S^1)$ for the singular simplicial set of the topological circle. A singular $0$-simplex of $S^1$ is an element of $\mathrm{Sing}(S^1)_0$, equivalently a continuous map $\Delta^0\to S^1$.
background
The module lifts the path-level winding and displacement invariant of the circle to singular simplices of TopCat.sphere 1, and proves that displacement vanishes on boundaries of singular 2-simplices. That identity is the chain-level fact making winding a homology invariant, and (with the generator evaluation) gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $n$-simplex of a space $X$ is a continuous map from the standard topological $n$-simplex $\Delta^n$ into $X$. For $n=0$, $\Delta^0$ is a point, so singular 0-simplices of $S^1$ are just points of $S^1$, packaged as the degree-0 object of Mathlib's singular simplicial set TopCat.toSSet.obj (TopCat.sphere 1).
Sibling abbreviations in the same file name the 1- and 2-simplices and the displacement/winding maps on 1-simplices that feed the kills-boundaries theorem.
proof idea
Definitional abbreviation only: evaluate Mathlib's singular simplicial set functor on the topological circle at the opposite of the 0-simplex object of the simplex category. No proof obligations.
why it matters
This type is the vertex sort for the free singular 1-chain calculus in the same module. Incidence-sum definitions and lemmas (boundaryIncidenceSum, its additivity and support expansions, and the vanishing statements for free-boundary-zero flows) all quantify over vertices of this type when reading off boundary coefficients of edge-chains.
Those incidence identities are the finite-support algebra behind the support-decreasing graph argument that every free 1-cycle is homologous (in the free singular complex) to an integer multiple of the fundamental loop. Together with simplexDisplacement_boundary (winding kills boundaries) and the generator evaluation from CircleWinding, this is the split-injective half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module doc notes the converse generation half still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply.
No Recognition forcing-chain landmark (T0–T8) is proved here; the declaration is pure topological scaffolding for the circle homology comparison used in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.