Base change of the resolution functor #
Clause (4b) of the functorial resolution theorem, commutation with change of fields [Kol07, 34.2],
for the resolution functor BR (Hironaka.Resolution.Algebraic.Kol07.Thm36.BR), following the
proof of [Kol07, Theorem 36]: an embedding i : X ↪ A over K and σ : K ↪ L give the embedding
i_{σ,L} : X_{σ,L} ↪ A_{σ,L} of the base changes, and the principalization sequence commutes
with change of fields [Kol07, Theorem 35 (4)].
The exact two-field form of the pullback lemma #
BRAffine_eq_eraseEmpty_pullback_of_admissible
(Hironaka.Resolution.Algebraic.Kol07.Thm36.BRAffinePullback) compares two admissible pairs over
the SAME field along a smooth g of ambients, up to the deletion of empty steps, because g need
not be surjective. When the runs are related on the nose, BP TZ = g^* BP TX, and the morphism f : Z ⟶ X is flat and SURJECTIVE, no deletion is needed and the fields may differ
(BRAffine_eq_pullback_of_BP_eq_pullback): the truncation index of Z is the absorbing index of
any component D of Z (firstCenterIndex_eq_componentIndex), which is the absorbing index in
BP TX of the component of X into which f maps D (generic points transported along the flat
f, firstCenterIndex_pullback_of_flat_of_le), the truncation index of X; so the affine
resolution of Z is the pullback of that of X, and the deletion commutes with the flat
surjective pullback.
The base-changed admissible pair #
For an admissible pair (TA, emb) of X and the pullback square XL = X ×_{Spec k} Spec L, the
base-changed triple Triple.baseChange TA σ (ambient TA.X.left ×_{Spec k} Spec L, ideal and
boundary pulled back) with the embedding baseChangeEmbedding emb is an admissible pair of XL
(admissibleEmbedding_baseChange): the square XL = X ×_{TA.X.left} (TA.baseChange σ).X.left
(pasting, IsPullback.of_right) makes emb' a closed immersion with emb'.ker = TA.I.comap p_A
(ker_eq_comap_of_isPullback), the ambient is affine (a fibre product of affines), and the
boundary stays empty. Then BP (TA.baseChange σ) = p_A^* BP TA (BP_baseChange), p_A is flat
(flat_of_isBaseChangeOf), p is flat and surjective (the base change of Spec L → Spec k), and
the exact pullback lemma gives BRAffine L XL = p^* BRAffine k X for affine members
(BRAffine_baseChange_of_class).
Clause (4b) for the resolution functor #
For members X over k and XL over L in a pullback square over Spec σ
(BR_baseChange_of_class): cover X by its finite affine cover Uᵢ and XL by the preimages
p⁻¹Uᵢ = Uᵢ ×_k L (coverPreimage of Hironaka.Resolution.Algebraic.Kol07.Thm36.BRDescent); the
coproduct ∐ p⁻¹Uᵢ → ∐ Uᵢ is again a base change over Spec σ (a coproduct of pullback squares is
a pullback square, isPullback_sigmaMap_sigmaDesc), so the affine (4b) computes BRAffine L (∐ p⁻¹Uᵢ) from BRAffine k (∐ Uᵢ) = g^* BR X; the affine (34.1) over L for the étale surjection ∐ p⁻¹Uᵢ → XL computes it from BR XL; cancelling the flat surjection gives BR XL = p^* BR X.
The exact two-field form of the pullback lemma: for admissible pairs of X over k and Z
over L whose global runs are related by BP TZ = g^* BP TX along a flat g, and a flat
SURJECTIVE f : Z ⟶ X compatible with the embeddings, BRAffine L Z = f^* BRAffine k X on the
nose.
The base change of an embedding (the proof of [Kol07, Theorem 36]: i : X ↪ A over K and
σ : K ↪ L give i_{σ,L} : X_{σ,L} ↪ A_{σ,L}): the base change of an admissible pair of
X along σ, through a pullback square XL = X ×_{Spec k} Spec L, is an admissible pair of XL
in the base-changed triple, compatible with the projections.
Clause (4b) for affine members of the class [Kol07, Theorem 36, proof; 34.2]: for affine
members X over k and XL over L in a pullback square over Spec σ,
BRAffine L XL = p^* BRAffine k X.
Clause (4b) for the resolution functor #
Clause (4b) of the functorial resolution theorem [Kol07, Theorem 36 (4); 34.2]: for members X
over k and XL over L of the class in a pullback square over Spec σ, BR XL = p^* BR X,
through the coproduct ∐ p⁻¹Uᵢ of the preimages of the finite affine cover of X (a base change of
∐ Uᵢ, the affine (4b)), the cover descent of X, the affine (34.1) over L for the étale
surjection ∐ p⁻¹Uᵢ → XL, and the cancellation of that flat surjection.