Canonical resolutions commute with smooth morphisms

The projection case: direct branches. For $\pi \text{\hspace{0.17em}⁣}:X\times {\mathbb{A}}^n\to X$, induct on the dimension of the base $X$, for all positive-marked, componentwise generically nonzero inputs. Dimension zero has empty support. Consider first a maximal-order pass of the algorithm in [F3]. Orders and boundary counts agree under projection by [F1], and boundary strata pull back to their products with ${\mathbb{A}}^n$. In the contained-stratum Step 1aa, containment in the support is preserved and reflected by this surjective projection. The stratum is regular and SNC with the boundary; its blowup and controlled division commute with projection by [F2]. Both sides give it the same encoded count/infinity primary value, $\nu =0$ and $\rho =\mathrm{\varnothing }$. Its restricted ideal may be zero, so no lower-dimensional induction is used here. In the nonboundary Step 1ba, the isolated codimension-one support components likewise pull back to their products. The proposition proves their SNC with the current boundary and their local equation $\mathcal{J}=(u^{\mu })$; the labelled Cartier blowup divides by $u^{\mu }$ and gives the unit ideal near the component on both sides. Its encoded infinity branch and zero auxiliary values therefore agree directly.

The projection case: inductive branches and general inputs. After the contained strata are removed, each retained boundary-stratum restriction is generically nonzero; after the codimension-one components are removed, the coefficient restriction to each maximal-contact hypersurface is generically nonzero. Indeed, the support identities in the proposition identify these restricted supports with proper subsets of their respective components. Projection preserves these identities, and the products of the components remain generically outside the restricted supports. These restrictions have base dimension smaller than $\dim X$, so induction now compares their resolutions with their products, including all three invariants. The homogenization and coefficient operations commute with projection by [F4]; derivatives in the new coordinates add no generators, since local extended ideals are generated by functions from $X$ and Leibniz's rule differentiates only their coefficients in those directions. The chosen maximal-contact hypersurfaces can therefore be their products, and [F3] ensures independence of those choices. For a general input, the monomial exponents, residual orders and threshold subsets are unchanged by projection, so companion passes reduce to the compared maximal-order passes and the monomial branch has identical values and centers. The proposition's successive assignment transports the remaining values through unchanged lifts on both sides. Thus at every stage ${\mathrm{inv}}_{{\pi }^{\ast }\mathcal{I}}(z)={\mathrm{inv}}_{\mathcal{I}}(\pi (z))$, and likewise for $\nu$ and $\rho$; [F5] gives the same centers, while [F2] identifies their blowups and transforms. Hence the canonical sequence is $(X_i\times {\mathbb{A}}^n)$.

The étale case and conclusion. For an étale morphism $\psi$ this is [F3]: the induced resolution is an extension of the canonical one and the invariants agree. For a general smooth $\phi$ with local factorization $\phi =\pi \circ \psi$, $\psi$ étale and $\pi$ the projection, the canonical resolution of ${\phi }^{\ast }\mathcal{I}={\psi }^{\ast }{\pi }^{\ast }\mathcal{I}$ is obtained by first taking the projection case for ${\pi }^{\ast }\mathcal{I}$ and then the étale case for $\psi$; both steps preserve the invariants, so $\mathrm{inv}(\phi (x^{\mathrm{\prime }}))=\mathrm{inv}(\pi (\psi (x^{\mathrm{\prime }})))=\mathrm{inv}(\psi (x^{\mathrm{\prime }}))=\mathrm{inv}(x^{\mathrm{\prime }})$, and analogously for $\nu$ and $\rho$.