SingularOneSimplex
plain-language theorem explainer
Names the type of singular 1-simplices on the topological circle: continuous maps from the standard 1-simplex Δ¹ into S¹, taken from Mathlib's singular simplicial set of TopCat.sphere 1. Anyone working with free singular chains, winding, or the H₁(S¹;ℤ) ≅ ℤ comparison cites this carrier type. It is a pure abbreviation with no proof content.
Claim. Write $\mathrm{Sing}_1(S^1)$ for the set of singular $1$-simplices of the circle: continuous maps $\Delta^1 \to S^1$, equivalently the degree-$1$ component of the singular simplicial set of the topological space $S^1$.
background
The module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of the topological circle $S^1$, then proves that displacement vanishes on boundaries of singular 2-simplices. That identity is what makes winding a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $n$-simplex in a space $X$ is a continuous map from the standard topological $n$-simplex $\Delta^n$ into $X$. Here $X$ is Mathlib's TopCat.sphere 1 (the unit circle), and the singular simplicial set is obtained by applying TopCat.toSSet. The degree-1 object of that simplicial set is exactly the type of continuous maps $\Delta^1\to S^1$.
Sibling abbreviations in the same file introduce the 0- and 2-simplex carriers, the reparameterization of $\Delta^1$ onto the unit interval, and the maps simplexDisplacement / simplexWinding that send each singular 1-simplex to a real displacement (equivalently $2\pi$ times winding).
proof idea
Pure definitional abbreviation. The right-hand side is the evaluation of the singular simplicial set of TopCat.sphere 1 at the opposite of the object $\Delta[1]$ in the simplex category: no tactics, no lemmas, no computational content beyond unfolding the Mathlib singular-set construction.
why it matters
This carrier type is the domain for every free singular 1-chain and every winding computation in CircleWindingChain. Downstream results that quantify over it include incidence sums on edge supports (boundaryIncidenceSum_single, boundaryIncidenceSum_eq_support_sum), $\ell^1$ size of oriented cyclic walks (chainL1_orientedCyclicChain, chainL1_sub_orientedCyclic), and the generation routes that discharge the Mathlib comparison circleH1ZIsoInt (via directed-cycle terms, free prisms, or explicit raw prisms).
In the module narrative it is the object to which simplexDisplacement is applied; together with the kills-boundaries identity and the fact that the fundamental loop has winding 1, one obtains a left inverse to the fundamental class. The remaining open half (every 1-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No Recognition forcing-chain step (T0–T8) is invoked here; the work is classical algebraic topology supporting the circle homology bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.