ptH
plain-language theorem explainer
The degree-0 singular homology class of a chosen point x in a space X, realized as a ℤ-module map ℤ → H₀(X;ℤ). Anyone tracking basepoint classes under continuous maps, path-joinings, or clopen augmentations cites this. The definition is the composite of the inverse of the canonical H₀(ℤ[0]) ≅ ℤ isomorphism with the homology map of the constant-simplex chain map from ℤ concentrated in degree 0.
Claim. For a topological space $X$ and a point $x \in X$, write $[x]_0$ for the morphism $\mathbb{Z} \to H_0(X;\mathbb{Z})$ obtained by composing the inverse of the canonical identification $H_0(\mathbb{Z}[0]) \cong \mathbb{Z}$ with the degree-$0$ homology map of the chain map that sends $1$ to the constant singular $0$-simplex at $x$.
background
The ambient module builds singular homology of spaces in TopCat with integer coefficients. Degree-$n$ homology $H_n(X;\mathbb{Z})$ is abbreviated as the homology of the singular chain complex of $X$. A companion abbreviation identifies the homology in degree $0$ of the chain complex $\mathbb{Z}$ concentrated in degree $0$ with the module $\mathbb{Z}$ itself.
Upstream, the class of a point is first packaged as a chain map from that concentrated complex: the generator $1$ is sent to the constant singular $0$-simplex at $x$, with the higher-degree components forced to vanish. Passing to homology and transporting across the canonical isomorphism yields a clean morphism out of $\mathbb{Z}$ rather than out of a homology object of a single complex.
Local setting is the singular-sphere foundation layer (prisms, pairs, subdivisions, Mayer–Vietoris), which needs a stable name for basepoint classes before comparing them under joins and covers.
proof idea
Pure definitional composite, not a tactic proof. Invert the canonical isomorphism $H_0(\mathbb{Z}[0]) \cong \mathbb{Z}$, then postcompose with the degree-$0$ homology map of the chain map that realizes the constant simplex at $x$. No further lemmas are invoked at the definition site; naturality and pairing identities are proved downstream by unfolding this composite.
why it matters
Gives the Foundation layer a named degree-$0$ point class that later lemmas can move and pair. Downstream, the pairing against a clopen augmentation recovers the characteristic value $1$ or $0$ according as the point lies in the set; path-joined points are shown to determine the same class; and the construction is natural for continuous maps. In the sphere-geometry module the same class builds the point-difference morphism on the two-arc intersection, which is then shown to die under the Mayer–Vietoris pair map into the direct sum of the punctured covers, supplying a concrete nonzero class in the intersection that becomes zero in each piece. That difference class is the algebraic witness used when the singular-sphere cover arguments need a nontrivial $H_0$ element supported on the overlap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.