amap_comp_atee
plain-language theorem explainer
If a vertex-set map preserves chosen apex (barycenter) operations, the induced chain maps commute with the subdivision homotopy operators built from those apices. Algebraic topologists in the singular-subdivision package cite this naturality square when pushing generators through the prism homotopy. The proof is induction on dimension, reducing on free generators via the cone and boundary intertwining lemmas.
Claim. Let $f:\alpha\to\beta$ be a map of vertex sets and let $\mathrm{bary}_\alpha$, $\mathrm{bary}_\beta$ be apex functions on finite tuples. Suppose $f$ intertwines apices: $\mathrm{bary}_\beta(f\circ w)=f(\mathrm{bary}_\alpha w)$ for every tuple $w$. Then for every $n$, the induced chain maps satisfy $(\mathrm{amap}\,f)_{n+1}\circ T_n^{\alpha}=T_n^{\beta}\circ(\mathrm{amap}\,f)_n$, where $T^{\cdot}$ is the subdivision homotopy operator built from the corresponding apex function.
background
The module develops singular subdivision and prism homotopies on free chain modules generated by vertex tuples (abstract simplices). The generator asimplex w is the basis chain for a tuple $w:\mathrm{Fin}(n+1)\to\alpha$. The operator abnd is the alternating face-boundary on those generators; acone is the algebraic cone that adjoins a fixed apex; atee is the subdivision homotopy assembled from repeated coning against a chosen apex function bary.
A map $f:\alpha\to\beta$ of vertex sets induces degreewise chain maps amap f by postcomposition on tuples. The hypothesis hf says $f$ intertwines the two apex choices, so barycenters (or other apex prescriptions) push forward correctly. The ambient setting is the Foundation singular-subdivision stack (imports from Mathlib singular homology and the local SingularPrism package), preparing geometric realization on the standard simplex.
Upstream companion facts used here are the already-proved intertwining lemmas for cone and boundary: amap commutes with acone and with abnd under the same data.
proof idea
Induction on the degree $n$. For $n=0$, both atee operators are zero, so both composites vanish.
At $n+1$, extend equality of linear maps by the free-module extensionality AC.hom_ext on a generator asimplex w. Unwind both sides with the simplicial formulas for atee and amap. The cone intertwining lemma amap_comp_acone moves amap across the cone on the residual chain asimplex w - atee(\mathrm{abnd}(\mathrm{asimplex}\,w)); the apex hypothesis hf identifies the image apex. The inductive hypothesis applied to the boundary chain, together with amap_comp_abnd and map_sub, closes the remaining face terms. All steps are LinearMap.congr_fun rewrites plus one congruence.
why it matters
This is the naturality square for the subdivision homotopy: maps that preserve apex data automatically preserve the prism operator atee. The sole recorded consumer is gen_pushSimplex_comp_tOp, whose doc-comment states that tOp on a pushed generator computes the homotopy of the pushed tuple; that lemma rewrites through atee after pushing a continuous simplex, and needs exactly this commutation to move amap (or its geometric counterpart) past the homotopy.
In the Recognition Foundation stack the result sits in the singular-subdivision layer that supplies honest chain-level homotopies before geometric realization on $\Delta^n$ (Stage 5b in the same file). It does not itself touch the forcing chain T0–T8, the J-cost, or the eight-tick octave; it is infrastructure ensuring subdivision and pushforward commute, so later continuum-bridge and ledger arguments can move chains without tracking apex choices by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.