sdGen
plain-language theorem explainer
For each singular n-simplex s of a space X, this map ℤ → C_n(X) is the value of barycentric subdivision on that generator: push the affine subdivision of the standard simplex forward along s. Anyone assembling the full singular subdivision operator as a coproduct over generators cites it. The body is a one-line composite of affine subdivision of the identity tuple with the chain map induced by s.
Claim. Let $X$ be a topological space, $n \in \mathbb{N}$, and $s$ a singular $n$-simplex of $X$. The generator value of singular barycentric subdivision is the $\mathbb{Z}$-linear map $\mathbb{Z} \to C_n(X)$ sending $1$ to the image, under the chain map induced by $s$, of the affine barycentric subdivision of the standard $n$-simplex.
background
Singular chains here are the free $\mathbb{Z}$-module on singular simplices: the degree-$n$ group $C_n(X)$ is the coproduct $\coprod_{\sigma} \mathbb{Z}$ indexed by the set of continuous maps $\Delta^n \to X$. Generators of that coproduct are the unit maps $\mathbb{Z} \to C_n(X)$ attached to each simplex.
Affine chains live on vertex tuples in a convex set. The affine simplex generator is the Dirac mass on a tuple; the affine barycentric subdivision operator is defined by the usual cone recursion $S(\sigma) = b_\sigma \cdot S(\partial\sigma)$ on generators (identity in degree 0), using a chosen barycenter map. The barycenter map on the standard simplex $\Delta^n$ is the ordinary barycenter of the vertices of a face.
The identity vertex tuple is the ordered list of vertices of $\Delta^n$. Affine subdivision of that generator is the subdivided standard simplex; transporting it along a singular simplex $s$ yields the singular subdivided chain.
proof idea
Pure definition, not a proof. Form the affine generator on the identity vertex tuple of $\Delta^n$, apply affine barycentric subdivision with the standard barycenter function, then convert the resulting affine chain into a singular chain via the map induced by the given singular simplex $s$ (through the simplex equivalence and the affine-to-singular chain transport). The result is a morphism $\mathbb{Z} \to C_n(X)$.
why it matters
This is the generator-wise building block of the singular barycentric subdivision operator: the full operator on $C_n(X)$ is the coproduct (Sigma-desc) of these maps over all singular simplices. The companion lemma records that composing the ordinary generator inclusion with the full operator recovers exactly this value.
Downstream, the chain-map identity $\partial \circ S = S \circ \partial$ and naturality of subdivision are proved by reducing to generators and rewriting with this definition. In the Recognition foundation stack, singular subdivision is the classical tool that makes singular homology homotopy-invariant and comparable to other chain models; the module sits under the prism and subdivision apparatus used for those comparisons.
No forcing-chain landmark (T0–T8) is stated here; the declaration is pure algebraic topology scaffolding inside the Foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.