sdOp
plain-language theorem explainer
Singular barycentric subdivision as a degree-preserving endomorphism of the integer singular chain group of a space X. Algebraic topologists cite it when building the chain homotopy to the identity and when proving that small-support chains remain small under refinement (Mayer–Vietoris). Defined by coproduct descent: on each generator simplex it returns the pushed barycentric subdivision chain.
Claim. For a topological space $X$ and $n\in\mathbb{N}$, the singular barycentric subdivision operator is the $\mathbb{Z}$-module morphism $\mathrm{sd}_n:C_n(X)\to C_n(X)$ induced by sending each singular $n$-simplex to the integer chain given by barycentric subdivision of the standard $n$-simplex, transported along that simplex.
background
Work sits in the singular-chain layer of the foundation stack. The degree-$n$ singular chain group $C_n(X)$ is the coproduct $\coprod_{\sigma} \mathbb{Z}$ indexed by singular $n$-simplices of $X$ (continuous maps from the standard simplex into $X$). Generators are the canonical inclusions of $\mathbb{Z}$ at each index.
Barycentric subdivision refines a simplex by iteratively coning to barycenters of faces. The generator map records, for each singular simplex, the integer chain obtained by applying that combinatorial subdivision on the standard simplex and pushing forward. The module imports Mathlib singular homology basics together with the local prism and affine-simplex toolkit used to build those subdivided chains.
The operator is the unique $\mathbb{Z}$-linear map on the whole coproduct that extends the generator values; that is the standard way to define chain-level subdivision before proving it commutes with the boundary and is chain-homotopic to the identity.
proof idea
One-line definition by the coproduct universal property: Sigma.desc applied to the family of generator maps. Each generator map sends the copy of $\mathbb{Z}$ at a singular simplex $s$ to the chain toChain of the barycentric subdivision of the identity tuple on the standard simplex, transported by the simplex equivalence for $s$. No further computation lives in the definition itself; equational lemmas such as the generator-composition identity are proved separately by the coproduct inclusion-desc cancellation.
why it matters
This is the chain-level subdivision map that every later equivariance and support argument quotes. Downstream, the generator identity identifies composition on a pure generator with the generator value; the push-simplex transport lemma computes subdivision after reparametrization; and the Mayer–Vietoris layer uses it to prove that subdivision preserves the small span of an open cover (and that the telescoped prism homotopy stays inside the small span one degree up). Those facts are the classical engine that makes singular homology satisfy excision and Mayer–Vietoris, which the foundation stack needs before any Recognition-level topological forcing can sit on singular chains. It is infrastructure, not a T0–T8 step, but without a well-typed sd the small-chain arguments do not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.