constSimplex
plain-language theorem explainer
The constant singular 0-simplex at a chosen point of a space X. Algebraic topologists cite it when writing point generators and path boundaries in singular chains. The definition transports the constant continuous map on the standard 0-simplex through the retyped simplex equivalence.
Claim. For a topological space $X$ and a point $x \in X$, write $\sigma_x$ for the singular $0$-simplex corresponding (under the standard identification of singular $0$-simplices with continuous maps from the standard $0$-simplex) to the constant map with value $x$.
background
In this module, singular $n$-simplices of a space $X$ are the index set of the degree-$n$ singular chain group: $\mathrm{Idx}, X, n$ is the set of $n$-simplices in the singular simplicial set of $X$. The degree-$n$ chain group is the free abelian group on that index set.
The retyped equivalence simplexEquiv identifies $\mathrm{Idx}, X, m$ with continuous maps $C(\Delta^m, X)$, where the domain is literally the standard simplex $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},(m+1))$. That retyping exists so face and degeneracy identities rewrite cleanly.
A $0$-simplex is therefore a continuous map from a point (the standard $0$-simplex) into $X$. The constant such map at a base point $x$ is the geometric content of this definition. Downstream, path simplices have boundary equal to the difference of the two constant $0$-simplices at the path endpoints.
proof idea
One-line definition. Apply the inverse of the retyped simplex equivalence in degree $0$ to the constant continuous map $\mathrm{ContinuousMap.const},_, x$. No further lemmas are invoked in the body.
why it matters
Constant $0$-simplices are the point generators used throughout the singular-sphere development. The path-boundary identity states $\partial[\gamma]=[y]-[x]$ with both endpoints realized as constant $0$-simplices; that identity is the engine behind "joined points have homologous point chains" and the reduction of every $0$-chain in a path-connected space to a multiple of a base-point generator.
Those lemmas feed the theorem that augmentation induces $H_0(X)\cong\mathbb{Z}$ for path-connected $X$. In the Recognition foundation stack this is the algebraic-topology substrate for treating recognition spaces and their low-degree homology, not a physics forcing step (T5–T8) itself. Sibling round-trip lemmas (pointOf / constant simplex) pin that every $0$-simplex is constant at its evaluation point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.