tOp
plain-language theorem explainer
Defines the singular subdivision chain homotopy operator sending degree-n singular chains on a space X to degree-(n+1) chains. Algebraic topologists cite it as the prism/homotopy half of barycentric subdivision on singular chains. It is the coproduct descent of the generator map that attaches the affine prism of the barycentric subdivision of the standard simplex.
Claim. For a topological space $X$ and $n \in \mathbb{N}$, let $C_n(X)$ be the free $\mathbb{Z}$-module on singular $n$-simplices of $X$. The singular subdivision homotopy is the $\mathbb{Z}$-linear map $t_X^{(n)} : C_n(X) \to C_{n+1}(X)$ obtained by extending, over the coproduct of generators, the assignment that sends each singular $n$-simplex to the chain given by the affine prism of the barycentric subdivision of the identity simplex.
background
In this module the singular chain groups are realized as coproducts of copies of $\mathbb{Z}$, one per singular simplex index: $C_n(X) = \coprod_{\sigma \in \mathrm{Idx}(X,n)} \mathbb{Z}$. Generators are the canonical inclusions of those summands.
The companion generator map $t_{\mathrm{gen}}$ evaluates, on each index $s$, the chain obtained by pushing the affine prism construction $\mathrm{atee}(\mathrm{baryFn}, n)$ of the standard identity simplex along the simplex equivalence attached to $s$. That is the classical prism operator on a single simplex, written in the module's affine-simplex language (barycenters, cones, and face operators from the SingularPrism import).
The local setting is the algebraic-topology half of the foundation layer: barycentric subdivision and its chain homotopy are built so that later Mayer–Vietoris and excision arguments can move chains into small open covers while staying homologous.
proof idea
One-line definition: $tOp$ is the unique morphism out of the coproduct $C_n(X)$ induced by the family $tGen, X, n$ on each summand. Concretely it is Sigma.desc (tGen X n), so on a generator it recovers $tGen$ by the coproduct universal property (Sigma.ι_desc), which is exactly the content of the sibling lemma gen_tOp.
why it matters
This operator is the homotopy half of singular barycentric subdivision. Downstream it feeds the transport lemmas gen_tOp and gen_pushSimplex_comp_tOp, the chain-homotopy successor identity tOp_chain_homotopy_succ, and the small-span preservation facts tOp_mem_smallSpan and tOpIter_mem_smallSpan used in SingularMayerVietoris.
Those small-span lemmas are what let iterated subdivision push a cycle into a cover while the prism homotopy keeps track of the homology. In the Recognition foundation stack this is infrastructure for singular homology computations that later interface with discrete forcing and octave structure; the declaration itself is pure classical AT, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.