support_transport
plain-language theorem explainer
If a ℤ-linear map on affine chains sends every generator whose vertices satisfy P into a chain supported only on tuples satisfying Q, then every chain supported on P is sent into support on Q. Homological algebraists and anyone bounding barycentric subdivision supports cite it. The proof expands the chain as a finite sum of scaled generators and pushes the predicate through linearity and support of scalar multiples.
Claim. Let $T : C_n^{\mathrm{aff}}(\alpha) \to C_m^{\mathrm{aff}}(\alpha)$ be $\mathbb{Z}$-linear on affine chains. Suppose that whenever a vertex tuple $w$ satisfies predicate $P$, every tuple in the support of $T$ applied to the generator simplex on $w$ satisfies $Q$. Then for every chain $c$ whose support lies in $P$, every tuple in the support of $T(c)$ satisfies $Q$.
background
Affine $n$-chains $AC,\alpha,n$ are finitely supported $\mathbb{Z}$-valued functions on vertex tuples $\mathrm{Fin}(n+1)\to\alpha$: formal integer combinations of ordered $(n+1)$-tuples of points in $\alpha$. The generator attached to a tuple $w$ is the Dirac chain $\mathrm{asimplex},w = \mathrm{single}(w,1)$.
The module sits in the singular-subdivision development: barycentric (and iterated) subdivision operators act as $\mathbb{Z}$-linear endomorphisms of these chain groups. Support predicates track geometric constraints on the vertices of those generators (pairwise distances, membership in a convex hull).
The lemma is the standard support-transport fact for free $\mathbb{Z}$-modules with finite support: linearity plus control on generators yields control on all chains. Upstream ingredients are just the definition of $AC$, the generator $\mathrm{asimplex}$, and the usual Finsupp identities ($\mathrm{sum_single}$, $\mathrm{map_sum}$, $\mathrm{support_smul}$).
proof idea
Fix $u$ in the support of $T(c)$. Rewrite $c$ via $\mathrm{Finsupp.sum_single}$, push $T$ through the finite sum ($\mathrm{map_sum}$), and obtain some $w\in c.\mathrm{support}$ with $u$ in the support of $T(\mathrm{single},w,(c,w))$.
Identify $\mathrm{single},w,(c,w)$ with the scalar multiple $(c,w)\cdot\mathrm{asimplex},w$ (using $\mathrm{smul_single}$ and $1\cdot m=m$). Apply $\mathrm{map_smul}$, then $\mathrm{Finsupp.support_smul}$, and invoke the generator hypothesis $hT$ at $w$ together with the assumption that every support point of $c$ satisfies $P$.
why it matters
Stage-6 subdivision estimates need to pass geometric predicates (hull membership, diameter contraction by $n/(n+1)$) from a single affine simplex to the full image chain under the barycentric operator $\mathrm{asub}$ and its iterates $\mathrm{asubIter}$. This lemma is the abstract engine behind $\mathrm{asub_support_bound}$ and $\mathrm{asubIter_support_bound}$.
Those bounds keep subdivided vertices inside the original hull while shrinking pairwise distances, which is the analytic control required for mesh refinement and for comparing singular chains to the discrete Recognition lattice. In the broader foundation stack this is pure chain-level bookkeeping, not a forcing-chain step (T0–T8), but it underwrites the geometric side of the singular-subdivision bridge used later for continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.