abnd_comp_atee_zero
plain-language theorem explainer
In degree zero the prism operator vanishes and barycentric subdivision acts as the identity, so the chain-homotopy identity ∂∘T = id−S holds by four rewrites. Algebraic topologists formalizing Hatcher's subdivision argument cite this as the base case before the inductive step in positive degrees. The proof is pure rewriting from the degree-zero specializations of T and S.
Claim. For any barycenter operator $\mathrm{bary}$, the degree-$0$ boundary composed with the prism operator equals the identity minus barycentric subdivision: $\partial_0 \circ T_0 = \mathrm{id} - S_0$. Both sides are the zero map, since $T_0 = 0$ and $S_0 = \mathrm{id}$.
background
Module Foundation.SingularSubdivision builds the algebraic-topology toolkit for barycentric subdivision of singular chains (Hatcher, Prop. 2.21), importing Mathlib singular homology and the local prism construction. The ambient chain groups are the augmented singular chains AC α n on a convex set in a normed module.
Three operators appear: the boundary abnd (∂), the prism/homotopy operator atee bary (T), and the subdivision operator asub bary (S). The barycenter map bary chooses the cone point used to define both T and S on simplices. In degree 0 the geometry collapses: there is no prism to fill, and subdivision of a 0-simplex is the identity.
The full chain-homotopy identity in positive degrees is ∂∘T + T∘∂ = id − S. The present statement is the degree-0 truncation ∂∘T = id − S, which is forced once T₀ = 0 and S₀ = id are known.
proof idea
Term-mode proof by four rewrites. First atee_zero replaces T at degree 0 by the zero map. Then asub_zero replaces S at degree 0 by LinearMap.id. Composition on the left with the zero map is zero (LinearMap.comp_zero), and id − id is zero (sub_self). Both sides of the claimed equality therefore reduce to the zero map, and the identity holds.
why it matters
This is the base case of the chain-homotopy identity that shows barycentric subdivision is chain-homotopic to the identity on singular chains (Hatcher Prop. 2.21). The sibling positive-degree identity ∂∘T + T∘∂ = id − S on AC α (n+1) is the inductive step; together they prove that subdivision induces the identity on homology.
In the Recognition Science foundation layer the result sits inside the singular-subdivision package that supplies topological language for recognition complexes and forcing arguments. No downstream consumers are wired yet (used_by is empty), so the lemma presently closes the degree-0 obligation inside this module rather than feeding a named parent theorem. It does not itself touch the T0–T8 forcing chain, RCL, or the φ-ladder; those enter only if later RS arguments invoke singular homology of recognition spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.