ptFrom_sChainMap
plain-language theorem explainer
Naturality of the degree-zero point inclusion into singular chains: postcomposing the constant 0-simplex at x with the singular chain map of f equals the constant 0-simplex at f(x). Cited by anyone assembling H_0 point classes or checking that basepoint maps commute with continuous maps. Proof reduces via from_single_hom_ext to the generator identity gen_map plus a 0-simplex uniqueness check.
Claim. For topological spaces $X,Y$ and a continuous map $f:X\to Y$, and any point $x\in X$, the chain-level point map at $x$ composed with the singular chain map of $f$ equals the chain-level point map at $f(x)$: $\mathrm{pt}_{X,x}\circ C_*(f)=\mathrm{pt}_{Y,f(x)}$.
background
The module builds singular homology infrastructure for Recognition Science foundation arguments (contractibility, spheres, Mayer–Vietoris). Singular chain groups are presented as coproducts of $\mathbb{Z}$ indexed by singular simplices; gen is the coproduct inclusion of a simplex, and chainMap f (degreewise) is the map induced by postcomposition with $f$.
The point map ptFrom X x is the morphism out of the single complex concentrated in degree 0 that sends the unit to the generator of the constant 0-simplex at $x$. The full singular chain map sChainMap f is the HomologicalComplex morphism assembled from those degreewise maps.
Upstream, gen_map records that induced chain maps send generators to generators of postcomposed simplices. Sibling facts constSimplex, pointOf, pointOf_map, and idx0_ext identify 0-simplices with points of the space, so constant simplices transform exactly under $f$.
proof idea
Term-mode reduction via HomologicalComplex.from_single_hom_ext: morphisms out of a single complex are determined by the degree-0 component. After comp_f and unfolding both ptFrom components at degree 0, the goal is the generator identity
gen X 0 (constSimplex X x) ≫ chainMap f 0 = gen Y 0 (constSimplex Y (f.hom x)).
Apply gen_map to move $f$ onto the simplex index. The remaining equality of 0-simplices is discharged by idx0_ext (0-simplices agree iff their underlying points agree), using pointOf_map and pointOf_constSimplex twice.
why it matters
Feeds the immediate parent ptH_natural, which lifts the same square to homology: the $H_0$ class of a point is natural in continuous maps. That naturality is the algebraic input for comparing basepoint classes under maps of spheres, pairs, and prism homotopies elsewhere in Foundation.SingularSphere and the singular Mayer–Vietoris / subdivision stack.
In the Recognition forcing chain this sits in the topological scaffolding that underwrites dimension and octave arguments (T7 eight-tick structure, T8 $D=3$), not in the J-cost or mass ladder themselves. It closes a small naturality obligation so later sphere and contractibility lemmas can treat point classes as functorial without re-proving chain-level bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.