The affine resolution along a smooth pullback of admissible pairs

Kollár's functoriality under smooth morphisms [Kol07, 34.1] for the affine resolution BRAffine (Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) on ONE smooth pullback pair of admissible pairs. Given admissible pairs (TX, embX) of X and (TZ, embZ) of Z, both reduced equidimensional (IsReducedEquidimensional) and affine, with TZ the pullback triple of TX along a smooth g : TZ.X.left ⟶ TX.X.left and a flat f : Z ⟶ X with embZ ≫ g = f ≫ embX,

BRAffine k Z = ((BRAffine k X).pullback f).eraseEmpty.

The proof is the mechanism Kollár states in one sentence — "(34.1) is a local property" ([Kol07, Theorem 36, proof]), for the functor "commutes with smooth morphisms" of [Kol07, 34.1]:

• BP TZ = ((BP TX).pullback g).eraseEmpty ([Kol07, Theorem 35 (4)], BP_pullback_eraseEmpty);
• the truncation index of Z is the absorbing index of any irreducible component D of Z (firstCenterIndex_eq_componentIndex, Hironaka.Resolution.Algebraic.Kol07.Thm36.EqualAbsorbingIndex), which after the deletion is the index eraseIdx of the absorbing index of D in V := (BP TX).pullback g (firstCenterIndex_eraseEmpty), and that is the absorbing index in BP TX of the component C of X into which f maps D (firstCenterIndex_pullback_of_flat_of_le: the generic point of D goes to the generic point of C because generalisations lift along flat maps), which is the truncation index of X;
• so BR_affine TZ embZ is the restriction to Z of the deletion of the truncation of V at the index of X (eraseEmpty_take, take_pullback), and the deletions agree (eraseEmpty_pullback_eraseEmpty', pullback_comp with the square embZ ≫ g = f ≫ embX).

The empty Z is its own case: every blow-up sequence on the empty scheme deletes to nil (eraseEmpty_eq_nil_of_isEmpty). The exact form for a flat surjective f with BP TZ = g^* BP TX on the nose, which the change of fields needs, is Hironaka.Resolution.Algebraic.Kol07.Thm36.BaseChangeAffine.

The file also records that the components of a member of the class HasDisjointIntegralComponents are integral (isIntegral_irreducibleComponentOpen, isIntegral_irreducibleComponent), used by Hironaka's Main Theorems (Hironaka.Resolution.Algebraic.Hir64).

The components of a member of HasDisjointIntegralComponents are integral

theorem Hironaka.Resolution.isIntegral_irreducibleComponentOpen {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (hX : X.HasDisjointIntegralComponents) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : AlgebraicGeometry.IsIntegral ↑(X.irreducibleComponentOpen C)

On the class the open component X.irreducibleComponentOpen C is the component itself (HasDisjointIntegralComponents.irreducibleComponentOpen_eq), hence an integral scheme: reduced as an open of the reduced X, irreducible as the component C.

theorem Hironaka.Resolution.isIntegral_irreducibleComponent {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (hX : X.HasDisjointIntegralComponents) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : AlgebraicGeometry.IsIntegral (X.irreducibleComponentIdeal C hC).subscheme

On the class the reduced closed subscheme of a component is integral: irreducibleComponentOpen C is closed (it is C), so its inclusion is a closed immersion and the subscheme of its kernel is isomorphic to it (Scheme.Hom.toImage).

The affine resolution along a smooth pullback of admissible pairs

theorem Hironaka.Resolution.BRAffine_eq_eraseEmpty_pullback_of_admissible {k : Type u} [Field k] [CharZero k] (X Z : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (X ↘ AlgebraicGeometry.Spec ↧k)] [Z.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (Z ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (Z ↘ AlgebraicGeometry.Spec ↧k)] (hX : AlgebraicGeometry.Scheme.IsReducedEquidimensional k X) (hZ : AlgebraicGeometry.Scheme.IsReducedEquidimensional k Z) (TX TZ : AlgebraicGeometry.Triple k) (embX : X ⟶ TX.X.left) (embZ : Z ⟶ TZ.X.left) (hadmX : AdmissibleEmbedding k X TX embX) (hadmZ : AdmissibleEmbedding k Z TZ embZ) (g : TZ.X.left ⟶ TX.X.left) [AlgebraicGeometry.Smooth g] (hpb : TZ.IsPullbackOf TX g) (f : Z ⟶ X) [AlgebraicGeometry.Flat f] (hsq : CategoryTheory.CategoryStruct.comp embZ g = CategoryTheory.CategoryStruct.comp f embX) : BRAffine k Z = ((BRAffine k X).pullback f).eraseEmpty

Kollár's "(34.1) is a local property" for the affine resolution on one smooth pullback pair [Kol07, Theorem 36, proof; 34.1]: for admissible pairs (TX, embX) of X and (TZ, embZ) of Z, reduced equidimensional, with TZ the pullback of TX along a smooth g and f : Z ⟶ X flat with embZ ≫ g = f ≫ embX, BRAffine Z is the deletion of the pullback of BRAffine X along f. The truncation indices agree through the components (firstCenterIndex_eq_componentIndex), the transport of the first-centre index along the flat g (firstCenterIndex_pullback_of_flat_of_le) and through the deletion (firstCenterIndex_eraseEmpty); the truncation commutes with the deletion (eraseEmpty_take) and with the restriction (take_pullback).