ptFromHomotopy
plain-language theorem explainer
A continuous path from x to y induces a degree-0 chain homotopy between the two point chain maps into the singular complex of X. Algebraic topologists cite it to move between basepoints in H_0. The construction puts the reversed path simplex in bidegree (0,1) and checks the homotopy identity via the path-boundary formula.
Claim. Let $X$ be a topological space and $x,y\in X$. Given a path $\gamma$ from $x$ to $y$, there is a chain homotopy between the point chain maps that send the generator of $\mathbb{Z}$ in degree $0$ to the constant $0$-simplex at $x$ and at $y$ respectively.
background
In the singular-sphere foundation layer one works with the singular chain complex $SC(X)$ of a space $X\in\mathbf{Top}$ (universe $0$), valued in $\mathbb{Z}$-modules. The point chain map associated to $x\in X$ is the map of complexes that, in degree $0$, sends $1\in\mathbb{Z}$ to the constant $0$-simplex at $x$ (and is zero in positive degrees). Its induced class in $H_0$ is the homology class of the point.
A continuous path $\gamma:x\leadsto y$ determines a singular $1$-simplex (the path simplex). Its boundary is the difference of the two constant $0$-simplices at the endpoints, which is exactly the algebraic content needed for a chain homotopy between the two point maps.
The local setting is Stage A/B of the singular-sphere development: relating path-connectedness of $X$ to equality of degree-$0$ homology classes of points, before exporting sphere homology facts used later in the Recognition forcing chain.
proof idea
Define the homotopy component $s_{i,j}$ to be zero except in bidegree $(i,j)=(0,1)$, where it is (up to identity rewrites on the single-object complex) the generator map of the reversed path simplex $\mathrm{pathSimplex}(\gamma^{\mathrm{symm}})$.
The zero-off-support obligation is immediate from the if guard. Commutation is by cases on degree: in degree $0$, expand both sides, apply the path-boundary identity gen_pathSimplex_bnd (boundary of the path simplex equals constant-$x$ minus constant-$y$), cancel with zero_add and an abelian-group rewrite; in positive degrees both sides vanish because the single complex supported in degree $0$ is zero there.
why it matters
This definition is the bridge from geometric paths to algebraic homotopies of point maps. Its sole recorded consumer is ptH_eq_of_joined: joined points have equal degree-$0$ homology classes, proved by unfolding the point-homology map and applying homologyMap_eq of this homotopy along a chosen path.
In the broader Recognition foundation, equality of $H_0$ classes for path-joined points is the singular-homology half of connectedness statements that feed sphere and Mayer–Vietoris arguments in the same module family. It does not itself touch T5–T8 or the J-cost calculus; it is pure singular-chain infrastructure those later geometric claims rely on when they need $H_0(S^n)$ or related comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.