asub
plain-language theorem explainer
Barycentric subdivision on affine chains: a degree-preserving ℤ-linear operator S defined by the cone recursion S(σ)=b_σ·S(∂σ) on generators, with S=id in degree 0. Algebraic topologists cite it as the affine model of Hatcher's subdivision before lifting to singular chains. The body is a recursive definition on n, not a proof.
Claim. Fix a barycenter map $b$ sending each finite vertex tuple in $\alpha$ to a point of $\alpha$. The barycentric subdivision operator $S_b$ is the family of $\mathbb{Z}$-linear endomorphisms of the affine chain groups $AC(\alpha,n)$ given by $S_b=\mathrm{id}$ in degree $0$, and on an $(n+1)$-generator $\sigma$ by $S_b(\sigma)=b_\sigma\cdot S_b(\partial\sigma)$ (cone of the already-subdivided boundary).
background
Affine $n$-chains $AC(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the indicator chains attached to a single tuple. The boundary $\partial:AC(\alpha,n+1)\to AC(\alpha,n)$ is the alternating sum of face restrictions (omit one vertex). The cone with apex $b$ prepends $b$ to every tuple, raising degree by one.
Classical singular homology uses barycentric subdivision to prove excision and Mayer–Vietoris: repeatedly subdivide until simplices lie in a prescribed open cover. This module builds the affine skeleton of that argument (Hatcher, Prop. 2.21), before the singular lift. The parameter $b$ is an abstract barycenter assignment; geometric barycenters in a convex set are the intended instance.
Upstream pieces are exactly the boundary, cone, and generator maps used in the recursion, together with the identity endomorphism in degree zero.
proof idea
Definition by recursion on degree, not a theorem. In degree 0 the operator is the identity linear map on $AC(\alpha,0)$. In degree $n+1$ it is the unique $\mathbb{Z}$-linear extension (via Finsupp.linearCombination) of the rule that sends a generator $w$ to the cone, with apex $b(w)$, of the already-defined subdivision of $\partial$ of that generator. No lemmas are invoked beyond the constructors of boundary, cone, and generators.
why it matters
This is the affine subdivision operator that the rest of the module is built around. Downstream it feeds the chain-map identity $\partial\circ S=S\circ\partial$, the prism homotopy $\partial T+T\partial=\mathrm{id}-S$ (and its iterates $\mathrm{id}-S^k$), and naturality under pushforward of vertex maps. Those identities are the Hatcher Prop. 2.21 package used to prove that subdivision is chain-homotopic to the identity.
Further downstream, the singular Mayer–Vietoris development cites that the singular subdivision operator preserves the small-span submodule of chains supported in a two-set cover, which is the technical step toward excision. In the Recognition Science foundation layer this sits in the singular-homology toolkit that underwrites topological invariants of the recognition complex; it is scaffolding for homology, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.