gen_tOp
plain-language theorem explainer
On each generator of the singular chain group, the subdivision homotopy equals its prescribed generator-level value. Anyone proving naturality, the chain-homotopy identity ∂T+T∂=id−S, degree-zero vanishing, or small-span preservation for barycentric subdivision cites this. The proof is a one-line appeal to the coproduct universal property (Sigma.ι_desc).
Claim. Let $X$ be a topological space and $s$ a singular $n$-simplex of $X$. Write $C_\bullet(X)$ for singular chains with $\mathbb{Z}$ coefficients, $\iota_s: \mathbb{Z}\to C_n(X)$ for the generator inclusion at $s$, and $T_n: C_n(X)\to C_{n+1}(X)$ for the singular subdivision homotopy. Then $\iota_s\circ T_n$ equals the explicitly prescribed generator value of that homotopy at $s$.
background
Singular chains $C_n(X)$ are the free $\mathbb{Z}$-module on the set of continuous maps $\Delta^n\to X$ (the index type of singular $n$-simplices). Each simplex $s$ contributes a generator inclusion $\iota_s:\mathbb{Z}\hookrightarrow C_n(X)$, realized as a coproduct summand map.
The singular barycentric subdivision operator $S_n:C_n(X)\to C_n(X)$ is defined by descending a generator formula through that coproduct. Parallel to it, the subdivision homotopy $T_n:C_n(X)\to C_{n+1}(X)$ is the operator whose value on the generator at $s$ is the chain obtained by applying the algebraic prism/cone construction (barycenter cone on the identity tuple, transported along the simplex equivalence of $s$).
This module builds those operators and the chain-homotopy relation that connects $S$ to the identity, the classical engine behind excision and Mayer–Vietoris for singular homology.
proof idea
One-line term proof. The homotopy $T_n$ is defined as the coproduct descent of its generator formula. The identity $\iota_s\circ T_n=$ (generator formula at $s$) is exactly the defining equation of that descent, discharged by Sigma.ι_desc.
why it matters
This is the generator-level interface every subsequent identity about $T$ reduces to. Downstream it is rewritten into: naturality of $T$ under continuous maps; vanishing of $T$ in degree $0$; the positive-degree chain-homotopy identity $\partial T+T\partial=\mathrm{id}-S$; the pushed-simplex computation of $T$; and preservation of the small span used in the singular Mayer–Vietoris argument.
In the Recognition foundation stack this is pure classical singular-homology scaffolding (subdivision and prism operators), not a forcing-chain step. It sits under the homology toolkit that later interfaces with geometric and dynamical constructions, rather than under T5–T8 or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.