The first-centre index along a flat surjection

The proof of [Kol07, Theorem 36] derives the functoriality of the resolution BR(X) of an affine scheme under change of fields [Kol07, 34.2] and under smooth morphisms [Kol07, 34.1] from the same properties of the principalization sequence BP(A, I_X, ∅) of the ambient: a change of fields and (through [Kol07, Lemma 41]) a smooth morphism of the schemes are covered by flat surjections of the ambients, along which the truncated restriction transports. This file proves the transport, for an arbitrary flat surjection p of the ambients.

• comap_le_comap_iff_of_flat_surjective: the inverse image of ideal sheaves along a flat surjective morphism reflects inclusions (a descent lemma for flat morphisms whose range hypothesis a surjection satisfies trivially).
• centerContains_pullback_iff_of_flat_surjective, firstCenterIndex_pullback_of_flat_surjective: the pullback of a blow-up sequence along a flat surjection [Kol07, Definition 30, 30.1] transports the predicate "the n-th centre contains the strict transform" exactly, the centres and strict transforms of the pullback being the inverse images of those of the original and the stage lifts being flat and surjective; firstCenterIndex_pullback_of_isIso is the special case of an isomorphism.
• BR_affine_eq_of_BP_eq_pullback_of_flat: BR_affine TA' emb = BR_affine TA (emb ≫ p) for triples over two fields k and L, granted BP TA' = (BP TA).pullback p and TA'.I = TA.I.comap p.
• flat_of_isBaseChangeOf, surjective_of_isBaseChangeOf: the base-change morphism of a triple along a field extension is flat and surjective, being the base change of Spec L → Spec k; so the transport applies to it (the change-of-fields clause for BR_affine).

These lemmas are used for the change-of-fields and smooth-morphism clauses of Kollár's resolution functor (Hironaka.Resolution.Algebraic.Kol07.Thm36.BaseChangeAffine) and for the transport of the first centre along flat covers (Hironaka.Resolution.Algebraic.Kol07.Thm36.FirstCenterPullback).

Inverse images along a flat surjection reflect inclusions

theorem Hironaka.Resolution.comap_le_comap_iff_of_flat_surjective {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.Flat f] (hs : Function.Surjective ⇑f) {A B : X.IdealSheafData} : A.comap f ≤ B.comap f ↔ A ≤ B

Along a flat surjective morphism the inverse image of ideal sheaves reflects and preserves inclusions (the descent lemma le_of_comap_le_of_flat; a surjection satisfies its range hypothesis).

The first-centre index along a flat surjection

theorem Hironaka.Resolution.centerContains_pullback_iff_of_flat_surjective {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (p : Y ⟶ X) [AlgebraicGeometry.Flat p] (hs : Function.Surjective ⇑p) (I : X.IdealSheafData) (n : ℕ) : CenterContains (S.pullback p) (I.comap p) n ↔ CenterContains S I n

The predicate "the n-th centre contains the strict transform" transports exactly along the pullback of a sequence along a flat surjective morphism [Kol07, Definition 30, 30.1]: the centres and strict transforms of the pullback are the inverse images of those of the original.

theorem Hironaka.Resolution.firstCenterIndex_pullback_of_flat_surjective {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (p : Y ⟶ X) [AlgebraicGeometry.Flat p] (hs : Function.Surjective ⇑p) (I : X.IdealSheafData) : firstCenterIndex (S.pullback p) (I.comap p) = firstCenterIndex S I

The first-centre index of the pullback of a sequence along a flat surjection, for the pulled-back ideal sheaf, is the first-centre index of the original; firstCenterIndex_pullback_of_isIso is the special case of an isomorphism.

BR_affine along a flat surjection of the ambients

theorem Hironaka.Resolution.BR_affine_eq_of_BP_eq_pullback_of_flat {k L : Type u} [Field k] [CharZero k] [Field L] [CharZero L] (TA : AlgebraicGeometry.Triple k) (TA' : AlgebraicGeometry.Triple L) (p : TA'.X.left ⟶ TA.X.left) [AlgebraicGeometry.Flat p] (hs : Function.Surjective ⇑p) (hBP : Sequence.BP TA' = (Sequence.BP TA).pullback p) (hI : TA'.I = TA.I.comap p) {Z : AlgebraicGeometry.Scheme} (emb : Z ⟶ TA'.X.left) : BR_affine TA' emb = BR_affine TA (CategoryTheory.CategoryStruct.comp emb p)

BR_affine transports along a flat surjection p of the ambients of two triples, over two fields, granted that the principalization sequences correspond: if BP TA' = (BP TA).pullback p and TA'.I = TA.I.comap p, then BR_affine TA' emb = BR_affine TA (emb ≫ p). The first-centre index is the same (firstCenterIndex_pullback_of_flat_surjective) and truncation commutes with the pullback. This is how [Kol07, Theorem 36, proof] derives 34.1 and 34.2 for BR from BP.

theorem Hironaka.Resolution.flat_of_isBaseChangeOf {k L : Type u} [Field k] [Field L] (σ : k →+* L) (TA : AlgebraicGeometry.Triple k) (TA' : AlgebraicGeometry.Triple L) (p : TA'.X.left ⟶ TA.X.left) (h : TA'.IsBaseChangeOf TA σ p) : AlgebraicGeometry.Flat p

The base-change morphism of a triple along a change of fields σ : k → L (Triple.IsBaseChangeOf) is flat: it is the base change of the flat morphism Spec L → Spec k (flat_of_isPullback_specMap).

theorem Hironaka.Resolution.surjective_of_isBaseChangeOf {k L : Type u} [Field k] [Field L] (σ : k →+* L) (TA : AlgebraicGeometry.Triple k) (TA' : AlgebraicGeometry.Triple L) (p : TA'.X.left ⟶ TA.X.left) (h : TA'.IsBaseChangeOf TA σ p) : Function.Surjective ⇑p

The base-change morphism of a triple along a change of fields is surjective: it is the base change of the surjective morphism Spec L → Spec k (surjective_of_isPullback_specMap).