idx0_ext
plain-language theorem explainer
Two singular 0-simplices of a space are equal exactly when they land on the same point. Algebraic topologists cite this when collapsing the 0-simplex type to the underlying point set. The proof is injectivity of the simplex equivalence plus the fact that the standard 0-simplex is a singleton.
Claim. Let $X$ be a topological space. If $s,t$ are singular $0$-simplices of $X$ and the underlying point of $s$ equals the underlying point of $t$, then $s=t$.
background
In the singular-set model used here, a singular $n$-simplex of a space $X$ is an element of the degree-$n$ object of the singular simplicial set of $X$: equivalently, via simplexEquiv, a continuous map from the standard geometric $n$-simplex into $X$. The degree-$n$ singular chain group is the free abelian group on that index set.
For $n=0$ the standard simplex is a singleton. Its unique vertex is written $v_0$. The map pointOf evaluates a singular $0$-simplex at $v_0$, recovering the point of $X$ at which the simplex sits. The companion constructor constSimplex builds the constant $0$-simplex at a given point.
The local module develops singular homology of spheres and path spaces, with generators, boundaries, and chain maps expressed in this language. Equality of $0$-simplices is the first bookkeeping step before writing $H_0$ and path boundaries.
proof idea
Transport the equality question across the equivalence that identifies singular $0$-simplices with continuous maps $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},1)\to X$. Injectivity of that equivalence reduces the claim to equality of the two continuous maps. Pointwise extensionality then asks only that the maps agree at every $z$ in the standard $0$-simplex. Subsingleton elimination replaces every such $z$ by the unique vertex $v_0$, and the hypothesis says the two maps already agree at $v_0$.
why it matters
This is the uniqueness half of the bijection between points of $X$ and singular $0$-simplices. Downstream, constSimplex_pointOf uses it to prove that building the constant simplex at pointOf s recovers $s$, so the two maps are inverse. That identification feeds the path-boundary formula gen_pathSimplex_bnd ($\partial[\gamma]=[\mathrm{target}]-[\mathrm{source}]$) and the naturality statement ptFrom_sChainMap for the chain map induced by a continuous map on point-supported $0$-chains.
In the Recognition foundation stack this sits under singular homology scaffolding (Mayer–Vietoris, prism operators, sphere computations) rather than under the T0–T8 forcing chain itself. It is pure bookkeeping, but without it every later identity that treats $0$-chains as formal sums of points would need an extra coherence argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.