gen_sdOp
plain-language theorem explainer
On each generator simplex, composing the generator inclusion with the singular subdivision operator recovers the subdivided generator. Algebraic topologists cite it when checking that subdivision is a chain map, is natural, or participates in the prism homotopy. The proof is a one-line term application of the coproduct universal property (Sigma.ι_desc).
Claim. For every topological space $X$, degree $n$, and index $s$ of an $n$-simplex in $X$, the composite of the generator map associated to $s$ with the singular subdivision operator equals the subdivided generator of $s$: $\mathrm{gen}(s)\circ S = S(\mathrm{gen}(s))$.
background
The module builds barycentric subdivision on singular chains of a space $X$ in TopCat. Singular $n$-chains are the free module on continuous maps from the standard $n$-simplex into $X$. Generators are the canonical inclusions of those basis simplices into the chain group; indices Idx X n label them.
The singular subdivision operator $S$ (written sdOp) is defined on the free module by specifying its value on each generator and extending linearly via the coproduct/desc universal property. The target value on a generator is the subdivided generator sdGen, built from the barycentric subdivision data imported from SingularPrism (affine simplices, barycentric maps, cone and boundary operators on abstract simplices).
Local setting: foundation-layer singular homology infrastructure used later for Mayer–Vietoris and chain-homotopy arguments, not yet the Recognition forcing chain itself.
proof idea
One-line term proof: Sigma.ι_desc _ _. Because sdOp is defined as the unique morphism out of the coproduct of generators that acts by sdGen on each summand, precomposing with the summand inclusion gen X n s is definitionally the component sdGen X n s. No further algebraic identity is needed.
why it matters
This is the generator-level evaluation lemma for subdivision. Downstream it is the first rewrite in the chain-map proof sdOp_comp_bnd ($\partial\circ S=S\circ\partial$), in naturality sdOp_natural, in the degree-zero identity sdOp_zero, and in the positive-degree prism homotopy tOp_chain_homotopy_succ ($\partial T+T\partial=\mathrm{id}-S$). It also feeds gen_pushSimplex_comp_sdOp (transport of subdivision under pushforward of simplices) and sdOp_mem_smallSpan in SingularMayerVietoris, which needs $S$ to preserve the small-span submodule for the MV argument.
In the broader Recognition stack this sits in Foundation singular-homology scaffolding: subdivision and the prism operator supply the standard homological toolkit (excision/MV, homotopy invariance) on which later geometric recognition constructions can rest. It is not itself a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.