asub_zero
plain-language theorem explainer
Barycentric subdivision of affine chains is the identity linear map in degree 0, for any barycenter choice. Algebraic topologists cite it when discharging the base case of the chain-map and prism-homotopy identities for subdivision. The proof is definitional reflexivity from the recursive clause of the operator.
Claim. For any barycenter assignment $\mathrm{bary}$, the barycentric subdivision operator $S$ on affine chains satisfies $S_0 = \mathrm{id}$ as a $\mathbb{Z}$-linear endomorphism of the module of affine $0$-chains.
background
The module AC α n is the free $\mathbb{Z}$-module on affine $n$-simplices in an ambient affine space $\alpha$ (tuples $\mathrm{Fin}(n+1)\to\alpha$). The boundary abnd and cone acone operators act on these chains in the usual combinatorial way.
Barycentric subdivision asub bary is defined by cone recursion on generators: in positive degree, $S(\sigma)=b_\sigma\cdot S(\partial\sigma)$, where $b_\sigma$ is the barycenter of the vertex tuple. The base clause of that recursion is exactly $S_0=\mathrm{id}$. The parameter bary is an arbitrary choice of apex for each finite tuple; no convexity or metric structure is required at this algebraic stage.
This sits in the Foundation singular-subdivision development, which ports Hatcher's barycentric subdivision and prism operator to affine chains before lifting to singular chains on topological spaces.
proof idea
One-line definitional proof (rfl). The recursive definition of the subdivision operator has explicit clause | 0 => LinearMap.id, so equality with the identity endomorphism is by reduction of the match.
why it matters
Base case for every inductive identity involving subdivision. Downstream it is rewritten in the chain-map property $\partial\circ S=S\circ\partial$ (abnd_comp_asub), in both degree-0 and positive-degree prism identities $\partial T+T\partial=\mathrm{id}-S$ (abnd_comp_atee_zero, abnd_comp_atee), in equivariance of $S$ under affine maps (amap_comp_asub), in the support-diameter contraction estimate (asub_support_bound), and when showing the singular subdivision operator is the identity in degree 0 (sdOp_zero).
Those facts are the algebraic engine behind Hatcher's Prop. 2.21 (subdivision is chain-homotopic to the identity), which the monolith uses to control mesh of singular chains. In the broader Recognition stack this is pure foundation scaffolding for homology, not a physics forcing step (T0–T8), but it underwrites later geometric estimates on the phi-ladder and eight-tick discrete structures once singular chains enter the picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.