pointOf_map
plain-language theorem explainer
Naturality of the underlying-point extraction for singular 0-simplices: pushing a 0-simplex forward along a continuous map, then reading its point, equals applying the map to the original point. Cited wherever singular chain maps must track basepoints. Proof unfolds the point extractor and applies naturality of the simplex equivalence, then closes by definitional equality.
Claim. Let $X,Y$ be topological spaces and $f:X\to Y$ continuous. For any singular $0$-simplex $s$ of $X$, the underlying point of the pushforward of $s$ along $f$ equals $f$ applied to the underlying point of $s$.
background
In the singular-sphere foundation layer, Idx X n is the type of singular $n$-simplices of a space $X$ (the index set of the degree-$n$ singular chain group). A singular $0$-simplex is a continuous map from the standard $0$-simplex into $X$, so it is determined by a single point of $X$.
The extractor pointOf recovers that point: it evaluates the simplex-equivalence of $s$ at the unique vertex $v_0$ of $\Delta^0$. The companion lemma simplexEquiv_map records naturality of that equivalence under continuous maps: the simplex-equivalence of a pushforward equals the continuous map composed with the original simplex-equivalence.
The local module builds singular homology of spheres and related chain-level maps; this lemma is the degree-$0$ naturality step needed when chain maps act on generators coming from points.
proof idea
Unfold pointOf on both sides so the claim is an equality of evaluations of simplex-equivalences at $v_0$. Rewrite the left-hand side by simplexEquiv_map, which replaces the simplex-equivalence of the pushforward by $f$ composed with the original simplex-equivalence. The two sides then match definitionally, and rfl finishes.
why it matters
Feeds ptFrom_sChainMap, which states that the chain-level point-inclusion map intertwines with the singular chain map of $f$: sending a point $x$ into chains of $X$ and then applying the chain map equals sending $f(x)$ into chains of $Y$. Without degree-$0$ naturality of pointOf, that intertwining identity cannot be checked on generators.
In the broader Recognition foundation stack this sits in the singular-homology toolkit (prisms, subdivision, Mayer–Vietoris) used to control sphere and circle winding data that later constrain discrete geometric structure. It is pure algebraic topology bookkeeping, not a forcing-chain step (T0–T8), but it is load-bearing for any argument that moves basepoints through singular chain maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.