atee_zero
plain-language theorem explainer
In degree zero the affine subdivision chain homotopy vanishes identically: T_0 = 0 for any choice of apex map. Algebraic topologists cite this when checking Hatcher's chain-homotopy identity ∂T + T∂ = id − S at the base degree. The proof is definitional reflexivity from the recursive clause that sets T to the zero map on 0-chains.
Claim. For any apex assignment $\mathrm{bary}$ sending finite point tuples in $\alpha$ to an apex in $\alpha$, the affine subdivision chain homotopy $T$ satisfies $T_0 = 0$ as a $\mathbb{Z}$-linear map on degree-$0$ affine chains.
background
The module builds affine singular subdivision in the style of Hatcher's proof of the subdivision theorem (Prop. 2.21). Affine chains $\mathrm{AC},\alpha,n$ are finitely supported integer combinations of ordered $(n+1)$-tuples of points in an ambient affine space $\alpha$. The boundary $\partial$ is the usual alternating face sum; the subdivision operator $S$ replaces each simplex by the cone decomposition of its faces about chosen apices.
The operator $T$ (here atee) is the prism/cone chain homotopy that witnesses $S \simeq \mathrm{id}$. Upstream, $T$ is defined by recursion on generators: $T(\sigma) = b_\sigma \cdot (\sigma - T(\partial\sigma))$ in positive degree, and explicitly $T = 0$ in degree $0$. The apex map $\mathrm{bary}$ supplies the cone point $b_\sigma$ for each generator.
This base clause is the algebraic reason the degree-$0$ homotopy identity collapses to $\partial\circ T = \mathrm{id}-S$ with both sides zero after $S_0=\mathrm{id}$.
proof idea
One-line definitional proof. The recursive definition of the subdivision homotopy sets the degree-$0$ component to the zero linear map, so atee bary 0 = 0 holds by rfl. No lemmas are applied.
why it matters
Feeds four local parents. The degree-$0$ chain-homotopy identity rewrites with this fact and $S_0=\mathrm{id}$ to get $\partial\circ T=0=\mathrm{id}-S$. The positive-degree identity $\partial T+T\partial=\mathrm{id}-S$ uses the same base case in its induction. Equivariance of $T$ under affine maps begins with a double application of the zero clause. Finally the singular (topological) homotopy $t_{\mathrm{Op}}$ is shown to vanish in degree $0$ by transporting this affine fact through the generating equivalence.
In the Recognition foundation stack this is pure scaffolding for singular homology of the recognition complex: subdivision must be chain-homotopic to the identity so that homology is invariant under barycentric refinement. It does not itself touch the forcing chain T0–T8, but it underwrites the topological side of the eight-tick and dimension arguments that sit on singular chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.