tOp_zero
plain-language theorem explainer
In degree 0 the singular subdivision chain homotopy operator T vanishes identically on singular 0-chains of any space X. Algebraic topologists cite this when checking the prism identity ∂T + T∂ = id − S at the bottom degree. The proof is a generator-wise extension: after unfolding the free-module map, the affine prism construction atee is zero in degree 0.
Claim. For every topological space $X$, the singular subdivision homotopy operator $T$ in degree $0$ is the zero map $C_0(X) \to C_1(X)$.
background
This module builds the barycentric subdivision operator $S$ and its chain homotopy $T$ on the singular chain complex of a space $X \in \mathbf{Top}$, using affine simplices, cones, and the prism (atee) construction imported from SingularPrism.
Singular $n$-chains are free modules on continuous maps $\Delta^n \to X$. The operator $T$ is the usual prism homotopy that witnesses $S \simeq \mathrm{id}$ on chains; in positive degrees it satisfies $\partial T + T\partial = \mathrm{id} - S$. Degree $0$ is special: there is no incoming boundary from negative degree, and the geometric prism over a $0$-simplex collapses.
Upstream pieces used here include the generator presentation of $T$ (gen_tOp), the affine simplex on the identity tuple, and the fact that the atee/prism map vanishes when the degree index is zero (atee_zero).
proof idea
Apply Sigma.hom_ext so it suffices to check the claim on each generator $s$ of $C_0(X)$. Rewrite by Limits.comp_zero and the generator formula gen_tOp, reducing to showing that the chain associated to atee (baryFn 0) 0 (asimplex (idTuple 0)) is zero. Finish with atee_zero, then LinearMap.zero_apply and map_zero.
why it matters
Feeds directly into tOp_chain_homotopy_zero, which states that in degree 0 one has $\partial \circ T = \mathrm{id} - S$ because both sides are zero (tOp_zero and sdOp_zero). That identity is the base case of the full chain-homotopy relation for singular subdivision, needed before naturality and homology-level consequences of $S \simeq \mathrm{id}$.
In the Recognition Science foundation stack this sits in the singular-homology toolkit used to control discrete recognition complexes and octave/tick filtrations; it is ordinary algebraic topology, not a forcing-chain (T0–T8) step, but it closes the degree-0 gap so the subdivision homotopy can be quoted uniformly in all degrees.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.