ptFrom
plain-language theorem explainer
Chain-map representative of a basepoint: from ℤ concentrated in degree 0 into the singular chains of a space X, sending 1 to the constant 0-simplex at x. Algebraic topologists and RS foundation proofs cite it for degree-0 point classes, naturality under continuous maps, and path-induced chain homotopies. Built as the unique map out of the single complex on that generator.
Claim. For a topological space $X$ and a point $x \in X$, there is a chain map $\mathrm{pt}_x : \mathbb{Z}[0] \to C_*(X;\mathbb{Z})$ from the integers concentrated in degree $0$ to the singular chain complex of $X$, sending the generator $1$ to the constant singular $0$-simplex at $x$.
background
The ambient module builds singular-homology tools for spaces in TopCat, with ℤ coefficients. The singular chain complex $C_*(X;\mathbb{Z})$ is the usual complex whose degree-$n$ term is free on continuous maps $\Delta^n \to X$. The abbreviation for ℤ as a complex concentrated in degree 0 is the domain of the map defined here.
A constant singular 0-simplex at $x$ is the continuous map $\Delta^0 \to X$ with image ${x}$. The generator attached to a singular simplex is the corresponding basis inclusion into the free ℤ-module of chains. Together these supply the degree-0 component of the point chain map.
Local setting is the SingularSphere foundation layer: point classes, augmentations against clopen sets, and path homotopies, used to control $H_0$ and connectedness statements downstream.
proof idea
Definitional construction, not a multi-step proof. Apply HomologicalComplex.mkHomFromSingle to the generator of the constant 0-simplex at $x$. The side condition (vanishing of the differential out of every positive degree on the single complex) is discharged by absurd plus omega: there is no $k$ with $k+1=0$ in $\mathbb{N}$. The resulting morphism of complexes is the point chain map.
why it matters
This is the raw chain-level avatar of a point. Downstream it feeds the degree-0 homology class of a point (compose with the $H_0$ isomorphism), the pairing of that class against a clopen augmentation (membership test in $H_0$), naturality under continuous maps, and the fact that a path between points yields a chain homotopy between the two point maps.
In the Recognition foundation stack this sits under SingularSphere, SingularPrism, and Mayer–Vietoris infrastructure: controlling $H_0$ of spaces and spheres that appear in geometric forcing and connectedness arguments. It does not itself invoke T5–T8 or the RCL; it is pure singular-homology scaffolding those geometric claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.