pointOf_constSimplex
plain-language theorem explainer
Extracting the underlying point of the constant singular 0-simplex at x recovers x. Anyone working with the point/0-simplex correspondence in singular chains on TopCat cites this as the left inverse identity. The proof unfolds both maps and cancels the simplex equivalence against its inverse.
Claim. For any topological space $X$ and point $x \in X$, if $\sigma_x$ denotes the constant singular $0$-simplex at $x$, then the underlying point of $\sigma_x$ equals $x$.
background
In this module, singular $0$-simplices on a space $X$ (objects of TopCat) are identified with continuous maps from the standard $0$-simplex into $X$. The standard $0$-simplex is a single vertex $v_0$, so such a map is determined by where that vertex lands.
pointOf reads off that landing point: apply the simplex equivalence and evaluate at $v_0$. constSimplex builds the inverse direction: the constant continuous map at a chosen point $x$, transported back through the equivalence. Together they implement the classical bijection between points of $X$ and singular $0$-simplices.
The local setting is the singular-chain apparatus used to compute homology of spheres and related spaces in the Recognition foundation layer (Mayer–Vietoris, path simplices, augmentation).
proof idea
Unfold both definitions. After unfolding, the left-hand side is the simplex equivalence applied to its own inverse on the constant map at $x$, then evaluated at $v_0$. Equiv.apply_symm_apply cancels the equivalence pair, leaving evaluation of the constant map at $v_0$, which is definitionally $x$. Close by rfl.
why it matters
This is the left-inverse half of the point/0-simplex correspondence. Its sibling constSimplex_pointOf uses it (via idx0_ext) to get the right inverse, so every $0$-simplex is the constant simplex at its underlying point.
Downstream, path-boundary calculations (gen_pathSimplex_bnd) write $\partial[\gamma]=[y]-[x]$ in terms of constant simplices and need this identity when simplifying. Augmentation pairings (ptFrom_augTo) and naturality of point classes under continuous maps (ptFrom_sChainMap) both reduce through pointOf_constSimplex when comparing generators built from constant simplices.
In the broader RS foundation stack this sits under singular homology scaffolding for spheres and contractible spaces, not on the T0–T8 forcing chain itself; it is infrastructure for chain-level arguments that later feed topological invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.