pointOf
plain-language theorem explainer
Extracts the underlying point of a singular 0-simplex in a topological space by evaluating its continuous map at the unique vertex of the standard 0-simplex. Anyone working with singular chains, partial augmentation, or H_0 will cite it. The definition is a one-line application of the retyped simplex equivalence at that vertex.
Claim. For a topological space $X$ and a singular $0$-simplex $\sigma$ of $X$, $\mathrm{pointOf}(\sigma)$ is the point of $X$ obtained by evaluating the continuous map corresponding to $\sigma$ at the unique vertex of the standard $0$-simplex.
background
In singular homology, a singular $n$-simplex of a space $X$ is a continuous map from the standard $n$-simplex into $X$. The type Idx X n is exactly that index set: the $n$-simplices of the singular simplicial set of $X$. Degree-$0$ simplices are continuous maps from a one-point standard simplex, so each carries a single underlying point of $X$.
The unique vertex of the standard $0$-simplex is written $v_0$ (the barycentric coordinate vector with mass $1$ on the single index). The retyped equivalence simplexEquiv identifies a singular $m$-simplex with a continuous map $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(m+1))\to X$, avoiding a definitional normal-form obstruction that blocks rewriting.
This module builds singular-sphere and path-connectedness facts for $H_0$ (augmentation, clopen partial augmentation, and reduction of $0$-cycles to a base point).
proof idea
One-line definition: apply simplexEquiv X 0 to the given singular $0$-simplex to obtain a continuous map from the standard $0$-simplex into $X$, then evaluate that map at $v_0$. No further lemmas are needed at the definition site.
why it matters
This is the bridge from formal singular $0$-simplices to ordinary points of $X$. Downstream, partial augmentation augFun counts a generator with coefficient $1$ precisely when pointOf s lies in a set $A$; the same extraction appears in gen_augFun, augFun_genUnit, and the proof that clopen partial augmentation kills boundaries (bnd_augFun).
It also closes the round-trip with constant simplices (constSimplex_pointOf, idx0_ext) and feeds the path-connected reduction: every $0$-chain is homologous to its total augmentation times a base-point simplex (exists_bnd_of_pathConnected). In the Recognition foundation stack this is pure singular-homology scaffolding for $H_0\cong\mathbb{Z}$ on path-connected spaces, not a physics forcing step (T5–T8), but it is required infrastructure for any later topological invariants built on singular chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.