sdOp_zero
plain-language theorem explainer
In degree 0 the singular subdivision operator on integer singular chains is the identity. Anyone checking the base case of the subdivision chain homotopy (or the prism operator identity ∂T = id − S) cites this. The argument is a generator-wise reduction: Sigma-extensionality, the degree-0 affine subdivision identity, and the standard simplex generator map.
Claim. For every topological space $X$, the singular subdivision operator $S_X$ in degree $0$ equals the identity endomorphism of the singular chain group $C_0(X;\mathbb{Z})$.
background
The ambient module builds the classical singular subdivision operator on integer chains of a space $X\in\mathbf{Top}$, together with the prism operator that will witness $S\simeq\mathrm{id}$. Chains live in the coproduct group $C_n(X;\mathbb{Z})=\coprod_{\sigma} \mathbb{Z}$ indexed by singular $n$-simplices; each simplex contributes a generator via the coproduct inclusion.
Affine chains $AC$ carry the combinatorial model: an affine simplex is the Dirac generator on a vertex tuple, and affine subdivision $asub$ (barycentric, via $baryFn$) acts on those generators before they are pushed forward to singular chains by $toChain$. The degree-0 fact $asub_zero$ says barycentric subdivision on $0$-simplices is the identity linear map.
Local setting is the algebraic-topology half of the Foundation layer (imports from Mathlib singular homology and the in-repo SingularPrism chain groups), not yet the J-cost or forcing chain.
proof idea
Term/tactic hybrid on the ModuleCat morphism. Apply coproduct (Sigma) hom-extensionality and work on a single generator $s$. Rewrite the composite against $gen_sdOp$ and the category identity law, reducing the claim to: the chain image of the affine subdivision of the standard identity $0$-simplex equals the singular generator of $s$. Invoke $asub_zero$ (affine subdivision is $\mathrm{id}$ in degree 0) and $LinearMap.id_apply$, then finish with $toChain_asimplex_idTuple$, which identifies that standard generator with $gen,s$.
why it matters
Base case for the subdivision chain-homotopy package. The sole recorded consumer is $tOp_chain_homotopy_zero$, whose doc-comment states the degree-0 prism identity $\partial\circ T=\mathrm{id}-S$ and discharges it by rewriting both $tOp$ and $sdOp$ to zero/identity so both sides vanish. Without $S_0=\mathrm{id}$, the homotopy equation fails to even typecheck as an equality of endomorphisms of $C_0$.
In the broader Recognition stack this sits under Foundation singular machinery (prism and subdivision), the topological substrate used when continuum or chain-level arguments are later tied to discrete recognition structure. It does not itself touch T5–T8, RCL, or the $\varphi$-ladder; it is pure singular-homology bookkeeping that keeps the homotopy identities honest in the lowest degree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.