atee
plain-language theorem explainer
Subdivision chain homotopy T on affine chains: on generators T(σ)=b_σ·(σ−T(∂σ)), with T=0 in degree 0, extended ℤ-linearly. Algebraic topologists cite it for the standard chain homotopy from barycentric subdivision to the identity (Hatcher Prop. 2.21). Defined by recursion on degree via the cone operator and the affine boundary.
Claim. Fix a barycenter map $b$ sending each vertex tuple in $\alpha$ to a point of $\alpha$. The subdivision homotopy is the family of $\mathbb{Z}$-linear maps $T_n:C_n^{\mathrm{aff}}(\alpha)\to C_{n+1}^{\mathrm{aff}}(\alpha)$ with $T_0=0$ and, on an affine generator $\sigma$ of degree $n+1$, $T(\sigma)=b_\sigma\cdot(\sigma-T(\partial\sigma))$, where $\cdot$ is the cone that prepends the apex and $\partial$ is the alternating face-sum boundary.
background
Affine $n$-chains $C_n^{\mathrm{aff}}(\alpha)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The generator attached to a tuple $w$ is the Dirac chain $\mathrm{asimplex}(w)$. The affine boundary $\partial$ sends a generator of degree $n+1$ to the alternating sum of its faces $w\circ i.(\mathrm{succAbove})$.
The cone operator with apex $b$ prepends $b$ to every vertex tuple, raising degree by one. The module sits in the affine-chain layer of singular subdivision: one works with vertex tuples before realizing them as continuous singular simplices, so that barycentric subdivision and its homotopy can be written by pure linear algebra on generators.
Upstream ingredients are exactly those four maps: the chain groups, generators, boundary, and cone. The barycenter parameter is an arbitrary assignment of an apex to each tuple; geometric barycenters are a special case used later when diameters must shrink.
proof idea
Definition by recursion on degree, not a proved identity. In degree 0 the map is the zero linear map. In degree $n+1$ one extends by $\mathbb{Z}$-linear combination from generators: on the generator of a tuple $w$, form the chain $\mathrm{asimplex}(w)-T_n(\partial(\mathrm{asimplex}(w)))$, then apply the cone with apex $b(w)$. The recursion is well-founded because the boundary drops degree, so the inductive call is already defined.
why it matters
This is the operator $T$ in Hatcher's proof of Prop. 2.21: it supplies the chain homotopy between the identity and barycentric subdivision on affine chains. Downstream, $\partial\circ T+T\circ\partial=\mathrm{id}-S$ is proved as abnd_comp_atee (and the degree-0 case abnd_comp_atee_zero); iterating yields $\partial\circ T_k+T_k\circ\partial=\mathrm{id}-S^k$ (abnd_comp_ateeIter). Equivariance under maps that intertwine barycenters is amap_comp_atee.
In the singular Mayer–Vietoris development the same homotopy, transported to singular chains, preserves the small-span submodule (tOp_mem_smallSpan), which is the step that lets subdivision push cycles into a cover. Within Recognition Science this is pure foundational scaffolding for singular homology; it does not itself invoke the forcing chain T0–T8, but it underwrites the homological toolkit used when geometric realization and cover arguments appear later.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.