atee_asimplex
plain-language theorem explainer
On an affine simplex generator, the subdivision chain homotopy in degree n+1 equals the cone from the barycenter of that simplex minus the homotopy of its boundary. Algebraic topologists checking the Hatcher-style prism operator on free affine chains cite this generator identity. The proof is a one-line lift from the free-module presentation of affine chains.
Claim. Fix a barycenter assignment $\mathrm{bary}$ on finite vertex tuples in $\alpha$. For every $n$ and every $w:\mathrm{Fin}(n+2)\to\alpha$, the subdivision homotopy $T$ in degree $n+1$ applied to the affine simplex on $w$ equals the cone from $\mathrm{bary}(w)$ of that simplex minus $T$ applied to its boundary: $T_{n+1}(\sigma_w)=C_{\mathrm{bary}(w)}\bigl(\sigma_w-T_n(\partial\sigma_w)\bigr)$.
background
The module builds affine singular chains $AC_\alpha$ and the barycentric subdivision apparatus used to prove that subdivision is chain-homotopic to the identity (Hatcher, Prop. 2.21). Generators are affine simplices $\sigma_w$ on ordered vertex tuples $w$; the free-module map lift_asimplex extends identities stated on those generators.
The boundary $\partial$ is the usual alternating face sum. The cone operator $C_b$ adjoins an apex $b$ (here a barycenter) to a chain one degree lower. The operator $T$ (written atee) is the prism/subdivision homotopy built recursively from cones and boundaries; the companion operator $S$ is barycentric subdivision.
Locally one works over an arbitrary coefficient type $\alpha$ equipped with a choice of barycenter for every finite tuple, so the same formulas apply both to geometric simplices in a convex set and to purely combinatorial vertex data.
proof idea
One-line term proof: apply the free-module extension lemma lift_asimplex to the vertex tuple $w$. That lemma reduces any linear identity on affine chains to the corresponding identity on generators, and the recursive clause defining $T$ on generators is exactly the displayed cone formula, so no further rewriting is required.
why it matters
This generator formula is the inductive step fuel for the full chain-homotopy identity $\partial\circ T+T\circ\partial=\mathrm{id}-S$ on positive-degree affine chains (abnd_comp_atee), which is the Lean rendering of Hatcher's proof of Prop. 2.21. It is also the generator input to equivariance of $T$ under affine maps that intertwine barycenters (amap_comp_atee).
In the Recognition Science foundation stack, singular subdivision supplies the homological scaffolding that later interfaces with the eight-tick octave and the Clifford/Bott side of the forcing chain: once subdivision is homotopic to the identity, homology is invariant under the discrete recognition refinements used downstream. The lemma itself is pure algebraic topology; its value is that the homotopy identity and the map-equivariance theorems sit on a proved, sorry-free generator clause rather than an axiomatized black box.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.