amap_comp_asub
plain-language theorem explainer
If a point-map intertwines two apex (barycenter) assignments, the induced chain maps commute with the singular subdivision operators built from those apexes. Algebraic topologists cite this when transporting subdivision through continuous maps of spaces. The proof is induction on simplex dimension, reducing via cone and boundary equivariance and the intertwining hypothesis.
Claim. Let $f:\alpha\to\beta$ and let $\mathrm{bary}_\alpha$, $\mathrm{bary}_\beta$ be apex assignments on finite tuples in $\alpha$ and $\beta$. Suppose $f$ intertwines them: $\mathrm{bary}_\beta(f\circ w)=f(\mathrm{bary}_\alpha w)$ for every tuple $w$. Then for every dimension $n$, the induced chain map $\mathrm{amap}(f,n)$ commutes with subdivision: $\mathrm{amap}(f,n)\circ\mathrm{asub}(\mathrm{bary}_\alpha,n)=\mathrm{asub}(\mathrm{bary}_\beta,n)\circ\mathrm{amap}(f,n)$.
background
The module develops singular subdivision in the style of algebraic topology: free modules on abstract simplices, boundary, cone, and a barycentric subdivision operator built from an apex function on vertex tuples. The apex assignment $\mathrm{bary}$ picks a point in the ambient set from an ordered $(m+1)$-tuple; subdivision of an $n$-simplex is defined recursively by coning the subdivided boundary from that apex.
The induced map $\mathrm{amap}(f,n)$ pushes free generators by postcomposing vertex tuples with $f$. The operators $\mathrm{abnd}$ (abstract boundary) and $\mathrm{acone}$ (abstract cone) are the combinatorial ingredients of $\mathrm{asub}$. The local claim is naturality: whenever $f$ preserves apexes, subdivision on the domain and codomain are conjugate by $\mathrm{amap}$.
Upstream equivariance lemmas for cone and boundary under $\mathrm{amap}$ supply the inductive step; the zero-dimensional case is that subdivision acts as the identity on $0$-chains.
proof idea
Induction on dimension $n$. For $n=0$, both subdivision operators are the identity on the free module, so the two compositions collapse by the unit laws for linear-map composition.
For $n+1$, extend by the free-module universal property on generators (abstract simplices $w$). Unfold subdivision on a generator as the cone of the subdivided boundary. Apply the already-proved equivariance of cone under $\mathrm{amap}$, insert the intertwining hypothesis on the apex of $w$, then feed the inductive hypothesis into the subdivided boundary and finish with equivariance of the boundary operator under $\mathrm{amap}$. A final congruence restores the generator form on the codomain side.
why it matters
Naturality of subdivision is the algebraic step that lets subdivision operators on singular chains of a space $X$ be written as pushforwards of a model subdivision on standard simplices. Downstream, gen_pushSimplex_comp_sdOp uses exactly this intertwining: "$\mathrm{sdOp}$ on a pushed generator computes the subdivision of the pushed tuple," which is the heart of transporting the abstract operator to geometric singular chains.
In the Recognition foundation stack this sits under singular-homology scaffolding (imports from Mathlib singular homology and the local SingularPrism development). It does not itself invoke the forcing chain T0–T8 or the $J$-cost; it is pure chain-level infrastructure needed before homology-level recognition statements can move across maps of spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.