pointOf_
plain-language theorem explainer
The point of the k-th face of a singular 1-simplex equals the simplex map evaluated at the corresponding prism face of the base vertex. Algebraic topologists tracking 0-chains under face maps cite this when relating geometric points to singular data. The proof unfolds the point extractor and rewrites by face-compatibility of the simplex equivalence.
Claim. Let $X$ be a topological space, $\sigma$ a singular $1$-simplex on $X$, and $k\in\{0,1\}$. The geometric point of the $k$-th face of $\sigma$ equals the continuous map associated to $\sigma$ evaluated at the $k$-th face of the prism base vertex $v_0$.
background
The module develops singular-homology infrastructure for spheres: singular simplicial sets of a space $X$, face operators $\delta_k$, and the standard equivalence sending a singular $n$-simplex to a continuous map from the geometric $n$-simplex into $X$.
Here pointOf extracts the underlying point of a singular $0$-simplex. The prism package supplies a model vertex $v_0$ and face maps on that model; evaluating the simplex map at a prism face recovers the geometric endpoints of a path-like $1$-simplex.
Local setting is the singular chain complex of $X$ (via TopCat.toSSet), preparatory to Mayer–Vietoris and sphere homology computations imported from the sibling foundation modules.
proof idea
Term-style tactic proof in three steps: unfold the definition of the point extractor on $0$-simplices; rewrite by the already-proved identity that the simplex equivalence intertwines singular face maps $\delta_k$ with geometric prism faces; close by reflexivity of equality on the resulting point.
why it matters
Sits in Foundation.SingularSphere, the layer that equips Recognition Science with singular homology of spheres. Face-point compatibility is the elementary bridge from geometric endpoints of $1$-simplices to $0$-chains, needed before augmentation maps and homology groups can be identified with integer coefficients.
No direct downstream edges are recorded for this lemma, but sibling material (augmentation against a set, generators of the augmented chain group, constant simplices) depends on the same point-extraction vocabulary. In the broader forcing chain this supports topological input to dimensional claims (T8, $D=3$) and the eight-tick discrete period (T7), where sphere homology and low-dimensional singular data appear as structural constraints rather than physical postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.