The pullback of a smooth blow-up sequence is smooth

"If B is a smooth blow-up sequence then so is h^* B" [Kol07, 30.1]. The center Z_i ×_X Y of the pulled-back sequence is (Z_i).comap h_i (center_pullback), and the closed subscheme V(Z.comap g) is the base change of V(Z) along g: the square

V(Z.comap g) ⟶ Y, V(Z.comap g) ⟶ V(Z), g : Y ⟶ X, V(Z) ⟶ X

is cartesian (Mathlib's isPullback_of_isClosedImmersion). So the structure morphism of V(Z.comap g) factors as the base change V(Z.comap g) ⟶ V(Z) of g, smooth when g is and of the same relative dimension, followed by the structure morphism of V(Z), and smoothness (and the relative dimension, additively) follows by composition. Applied at every stage with g = h_i (smooth by smooth_pullbackStageHom) this gives the statement in both forms, IsSmooth and IsSmoothOfRelativeDimension; see also [Wlo05, Proposition 2.4.2 (1)].

theorem AlgebraicGeometry.smooth_subschemeι_comap_comp {X Y W : Scheme} (Z : X.IdealSheafData) (g : Y ⟶ X) [Smooth g] (φ : X ⟶ W) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι φ)] : Smooth (CategoryTheory.CategoryStruct.comp (Z.comap g).subschemeι (CategoryTheory.CategoryStruct.comp g φ))

If V(Z) → W is smooth and g is smooth, then V(Z.comap g) → W through g is smooth: the base change of g followed by the structure morphism of V(Z).

theorem AlgebraicGeometry.smoothOfRelativeDimension_subschemeι_comap_comp {X Y W : Scheme} (Z : X.IdealSheafData) (g : Y ⟶ X) {d : ℕ} [SmoothOfRelativeDimension d g] (φ : X ⟶ W) {e : ℕ} [SmoothOfRelativeDimension e (CategoryTheory.CategoryStruct.comp Z.subschemeι φ)] : SmoothOfRelativeDimension (d + e) (CategoryTheory.CategoryStruct.comp (Z.comap g).subschemeι (CategoryTheory.CategoryStruct.comp g φ))

The equidimensional form: relative dimensions add along the factorisation through the base change.

theorem AlgebraicGeometry.IsSmooth.pullback {k : Type u} [Field k] {X Y : Scheme} (f : X ⟶ Spec ↧k) (h : Y ⟶ X) [Smooth h] {S : X.BlowUpSequence} (hS : S.IsSmooth f) : (S.pullback h).IsSmooth (CategoryTheory.CategoryStruct.comp h f)

The pullback along a smooth h of a sequence whose centers are smooth over k has centers smooth over k: "if B is a smooth blow-up sequence then so is h^* B" [Kol07, 30.1].

theorem AlgebraicGeometry.IsSmoothOfRelativeDimension.pullback {k : Type u} [Field k] {X Y : Scheme} (f : X ⟶ Spec ↧k) (h : Y ⟶ X) {d : ℕ} [SmoothOfRelativeDimension d h] {S : X.BlowUpSequence} {n : ℕ} (hS : S.IsSmoothOfRelativeDimension f n) : (S.pullback h).IsSmoothOfRelativeDimension (CategoryTheory.CategoryStruct.comp h f) (n + d)

The equidimensional form: for h smooth of relative dimension d, the pullback of a sequence smooth of relative dimension n is smooth of relative dimension n + d, the codimensions of the centers unchanged.