tGen
plain-language theorem explainer
For each singular n-simplex s of a space X, this is the generator component of the singular subdivision chain homotopy: a map ℤ → C_{n+1}(X). It transports the affine barycentric cone recursion on the identity simplex of Δⁿ along s. Anyone assembling or naturalizing the full operator tOp cites it. The body is a direct composition of affine-to-singular transport with the affine homotopy on the standard simplex.
Claim. Let $X$ be a topological space, $n \in \mathbb{N}$, and $s$ a singular $n$-simplex of $X$. The generator value of the singular subdivision homotopy is the $\mathbb{Z}$-linear map $\mathbb{Z} \to C_{n+1}(X)$ obtained by transporting, along $s$, the affine subdivision chain homotopy (barycentric cone recursion) of the identity vertex tuple on the standard simplex $\Delta^n$.
background
Singular chains here are the free $\mathbb{Z}$-modules $C_n(X) = \coprod_{\sigma} \mathbb{Z}$ indexed by singular $n$-simplices of $X$ (the index type Idx). The full subdivision homotopy on singular chains is assembled generatorwise from this definition.
On the affine side, chains live on vertex tuples in an affine space. The affine subdivision homotopy is the cone recursion $T(\sigma) = b_\sigma \cdot (\sigma - T(\partial\sigma))$ on generators (vanishing in degree 0), with apex map the barycenter of the tuple. The identity vertex tuple on $\Delta^n$ is the standard embedding of the vertices; its affine simplex is the generator to which that recursion is applied.
Transport from affine chains on $\Delta^n$ into singular chains of $X$ is by the simplex equivalence attached to $s$: push the affine $(n+1)$-chain forward to a singular chain in degree $n+1$.
proof idea
Pure definitional composition, no tactics. Take the affine subdivision homotopy (barycentric apex function, degree $n$) applied to the affine generator of the identity vertex tuple on $\Delta^n$. Feed that affine $(n+1)$-chain into the transport map that sends affine chains on $\Delta^n$ to singular chains of $X$ along the simplex equivalence of $s$. The result is a morphism $\mathbb{Z} \to C_{n+1}(X)$.
why it matters
This is the generator-level seed of the singular subdivision chain homotopy. The full operator is the coproduct descent of these generator maps, and the generator comparison lemma records that composing a generator inclusion with that operator recovers exactly this value.
Naturality of the singular subdivision homotopy reduces, after coproduct extensionality, to identities involving these generator values under pushforward of simplices. In the Recognition foundation stack this sits inside the singular-prism / singular-subdivision layer that supplies chain-level subdivision and homotopy data for later geometric arguments; it is infrastructure rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.