sdOp_natural
plain-language theorem explainer
The singular subdivision operator in degree n is natural in the space: for any continuous map f : X → Y it intertwines the induced chain maps. Algebraic topologists cite this when assembling subdivision into a natural endomorphism of the singular chain functor, or when building prism/homotopy operators. The proof checks the identity on coproduct generators via Sigma.hom_ext, using generator-mapping lemmas and the simplex-equivalence naturality.
Claim. Let $f : X \to Y$ be a continuous map of topological spaces and let $n \in \mathbb{N}$. Write $C_n(f)$ for the induced map on singular $n$-chains and $\mathrm{sd}_X$, $\mathrm{sd}_Y$ for the singular subdivision operators in degree $n$. Then $C_n(f) \circ \mathrm{sd}_X = \mathrm{sd}_Y \circ C_n(f)$ as morphisms of chain groups (equivalently, the naturality square for subdivision commutes).
background
The module develops singular subdivision on the coproduct presentation of singular chain groups used throughout the Foundation singular-homology stack. Generators are indexed by singular simplices; the subdivision operator sends a generator to the integer chain obtained by barycentric subdivision of the standard simplex, pushed forward along the singular simplex map.
Upstream, chainMap is the degree-$n$ component of the singular chain complex functor applied to a continuous map $f$, typed on that coproduct presentation. The companion lemma gen_map records that this chain map sends the generator of a simplex $\sigma$ to the generator of the postcomposed simplex $f\circ\sigma$. Subdivision itself is assembled generatorwise from an abstract subdivision chain on the standard simplex (asub of the barycentric map on the identity simplex) via a toChain pushforward.
Naturality is the statement that subdivision is a natural endomorphism of the singular chain functor in each degree, not merely an endomorphism of each individual chain group.
proof idea
Both sides are morphisms out of a coproduct of copies of $\mathbb{Z}$, so Sigma.hom_ext reduces the claim to equality on each generator index $s$.
After cancelling associations, gen_map and the generator formula for subdivision (gen_sdOp) rewrite both composites as maps out of a single generator. The right-hand composite is identified with toChain of the postcomposed simplex applied to the fixed abstract subdivision chain, via toChain_comp_chainMap evaluated on that chain. The left-hand composite is rewritten the same way using naturality of the simplex equivalence (simplexEquiv_map). The two expressions match, and rfl closes.
why it matters
Naturality is the missing square that lets singular subdivision descend from a family of endomorphisms of chain groups to a natural transformation of the singular chain functor. Without it, one cannot conjugate subdivision past continuous maps, nor build natural prism operators or natural chain homotopies between $\mathrm{id}$ and $\mathrm{sd}$.
In the Recognition Science foundation layer this sits beside the singular prism package: subdivision and prisms are the classical toolkit for proving homotopy invariance of singular homology and for controlling mesh size under refinement. The forcing chain (T0–T8) and the Recognition Composition Law do not depend on this lemma directly; it is infrastructure for the topological side of the monolith (singular chains, octaves as discrete periods, and any later comparison of continuous vs discrete recognition complexes).
No downstream consumers are recorded yet in the graph, so the lemma is currently a proved leaf supporting future naturality and homotopy arguments rather than an already-cited step in a closed theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.