ptFrom_f_zero
plain-language theorem explainer
In degree 0, the chain map that realises a basepoint as a singular 0-cycle equals the generator of the constant 0-simplex at that point. Anyone computing point classes, augmentations, or naturality of singular chains on TopCat cites this. The proof is a short rewrite unfolding the single-complex construction and cancelling the identity iso.
Claim. For a topological space $X$ and a point $x\in X$, the degree-$0$ component of the chain map $\mathbb{Z}[0]\to C_\bullet(X)$ sending $1$ to the class of $x$ equals the generator of the constant singular $0$-simplex at $x$.
background
The module builds singular chain machinery on TopCat aimed at sphere homology and related Recognition foundation arguments. A singular $0$-simplex is a continuous map $\Delta^0\to X$; the constant simplex at $x$ is the unique such map with image ${x}$.
The generator map attaches to each singular simplex the corresponding basis arrow $\mathbb{Z}\to C_n(X)$ in the free $\mathbb{Z}$-module on simplices. The point class is the chain map from the complex with $\mathbb{Z}$ concentrated in degree $0$ into the singular complex of $X$, built by mkHomFromSingle from that generator (higher differentials vanish for degree reasons).
Upstream, the prism generator abbreviation supplies the free-module inclusion used here; the constant-simplex construction supplies the geometric $0$-simplex being included.
proof idea
Unfold the definition of the point-class chain map, then apply the standard component formula for a morphism out of a single complex in degree $0$. The remaining isomorphisms are the canonical identification of the single complex with itself and the identity arrow on that object; id_comp cancels the identity, leaving exactly the generator of the constant $0$-simplex.
why it matters
This is the computational hinge for every later identity that moves a point class through a chain map or pairs it with an augmentation. Downstream, the clopen-augmentation pairing reduces composition in degree $0$ via this equality and then evaluates membership of $x$ in the clopen set. Naturality under continuous maps likewise rewrites both sides in degree $0$ and compares generators of constant simplices.
In the broader SingularSphere development, point classes seed the comparison between singular homology and discrete Recognition data (connected components, augmentations). The lemma itself is pure algebraic topology bookkeeping, not a forcing-chain step, but it keeps the singular-homology interface honest for later sphere and Mayer–Vietoris arguments in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.