The weak transform along a flat pull-back of order sequences

Along a change of fields [Kol07, 34.2] the induced ideals of the base-changed sequence of order m [Kol07, Definition 66] are the pull-backs of the induced ideals. Hironaka/Scheme/BlowUpSequence/Pullback.lean proves this for a smooth h (IsOrderSeq.weakTransformSeq_pullback) and Hironaka/Scheme/BlowUpSequence/BaseChange.lean for the base-change square with Spec.map σ (weakTransformSeq_pullback_of_isPullback_specMap). This module states the common core for a flat p : Y ⟶ X between two smooth equidimensional bases, both sequences being sequences of order m: at every step the weak transform is the marked transform with mark m (weakTransform_eq_markedTransform_of_smooth, on both sides; the order condition on the pulled-back side is a hypothesis, not derived), and the marked transform commutes with flat pull-back where it is defined [Kol07, Definition 60] (markedTransform_comap_blowUpMap_of_pow_dvd). The main statement is weakTransformSeq_pullback_of_isOrderSeq.

theorem AlgebraicGeometry.weakTransform_comap_of_orderAlong_of_flat {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {X Y : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (f' : Y ⟶ Spec ↧L) (n' : ℕ) [SmoothOfRelativeDimension n' f'] (p : Y ⟶ X) (D I : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp D.subschemeι f)] [Smooth (CategoryTheory.CategoryStruct.comp (D.comap p).subschemeι f')] {m : ℕ} (hm : I.OrdAlongEq D.support ↑m) (hm' : (I.comap p).OrdAlongEq (D.comap p).support ↑m) : (I.comap p).weakTransform (D.comap p) = (I.weakTransform D).comap (Scheme.Hom.blowUpMap p D)

One step of the flat transport: for a smooth center D of order m on both sides, the weak transform of the pulled-back ideal along the pulled-back center is the pull-back of the weak transform along the morphism of blow-ups (both are marked transforms with mark m).

theorem AlgebraicGeometry.IsOrderSeq.weakTransformSeq_pullback_mk_of_flat {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {X Y : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (f' : Y ⟶ Spec ↧L) (n' : ℕ) [SmoothOfRelativeDimension n' f'] (p : Y ⟶ X) [Flat p] {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} (hS : S.IsOrderSeq f I E m) (hS' : (S.pullback p).IsOrderSeq f' (I.comap p) (E.comap p) m) (j : ℕ) (hj : j < S.length + 1) : (S.pullback p).weakTransformSeq (I.comap p) (S.pullbackStageIdx p ⟨j, hj⟩) = (S.weakTransformSeq I ⟨j, hj⟩).comap (S.pullbackStageHom p ⟨j, hj⟩)

The ⟨j, hj⟩ form of weakTransformSeq_pullback_of_isOrderSeq, by induction on the sequence peeling one blow-up on each side with isOrderSeq_cons_iff.

theorem AlgebraicGeometry.weakTransformSeq_pullback_of_isOrderSeq {k : Type u} [Field k] [CharZero k] {m : ℕ} {L : Type u} [Field L] [CharZero L] {X Y : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (f' : Y ⟶ Spec ↧L) (n' : ℕ) [SmoothOfRelativeDimension n' f'] (p : Y ⟶ X) [Flat p] {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} (hS : S.IsOrderSeq f I E m) (hS' : (S.pullback p).IsOrderSeq f' (I.comap p) (E.comap p) m) (i : Fin (S.length + 1)) : (S.pullback p).weakTransformSeq (I.comap p) (S.pullbackStageIdx p i) = (S.weakTransformSeq I i).comap (S.pullbackStageHom p i)

Along a flat pull-back of a smooth blow-up sequence of order m whose pull-back is again one of order m, the induced ideals of the pull-back are the pull-backs of the induced ideals under the stage lifts ([Kol07, 34.2] with [Kol07, Definition 66]; the marked transform commutes with flat pull-back, markedTransform_comap_blowUpMap_of_pow_dvd).