The first-centre index along a flat morphism meeting the generic point

The first-centre index firstCenterIndex S I (Hironaka.Resolution.Algebraic.Kol07.Thm36.Affine), the first stage whose centre contains the strict transform of V(I), is intrinsic to V(I) and transports along flat pullbacks of the sequence [Kol07, Corollary 22, proof; Definition 30, 30.1]. Hironaka.Resolution.Algebraic.Kol07.Thm36.FlatTransport proves this along a flat SURJECTION for every ideal sheaf; the functoriality of the affine resolution functor (Hironaka.Resolution.Algebraic.Kol07.Thm36.BRAffinePullback) and its change of fields (Hironaka.Resolution.Algebraic.Kol07.Thm36.BaseChangeAffine) need it component by component, along a flat morphism that need not be surjective but whose image contains the generic point of the component. This file proves that form: for an integral closed subscheme V(I) whose generic point lies in the image of a flat h, firstCenterIndex (S.pullback h) (I.comap h) = firstCenterIndex S I (firstCenterIndex_pullback_of_flat_of_mem_range), and likewise for an integral component V(I') of the preimage of V(I) dominating it (firstCenterIndex_pullback_of_flat_of_le).

The mechanism: downstairs to upstairs is monotonicity of CenterContains under pullback (centerContains_pullback_of_le); upstairs to downstairs, before the first downstairs absorption, uses the generic point η_n of the strict transform X̄_n: it lies over the generic point η of V(I), hence in the image of the stage lift h_n (range_pullbackStageHom: h_n(X_n ×_X Y) = Π_n⁻¹(h(Y))), so a pulled-back centre h_n⁻¹(Z_n) containing h_n⁻¹(X̄_n) forces Z_n ∋ η_n, that is, Z_n ⊇ X̄_n. Neither surjectivity nor smoothness of h is needed: flatness suffices (open immersions are the case used).

theorem Hironaka.Resolution.mem_range_pullbackStageHom_of_stageMap_mem_range {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (i : Fin (S.length + 1)) {x : ↥(S.stage i)} (hx : (S.stageMap i) x ∈ Set.range ⇑h) : x ∈ Set.range ⇑(S.pullbackStageHom h i)

A point of stage n lying over a point of the image of h lies in the image of the stage lift h_n [Kol07, Definition 30, 30.1] (range_pullbackStageHom).

theorem Hironaka.Resolution.centerContains_of_centerContains_pullback_of_mem_range {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] [AlgebraicGeometry.IsLocallyNoetherian X] (I : X.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑I.support) (hmem : η ∈ Set.range ⇑h) {n : ℕ} (hhist : ∀ m < n, ¬CenterContains S I m) (hc' : CenterContains (S.pullback h) (I.comap h) n) : CenterContains S I n

Along a flat h whose image contains the generic point η of the integral V(I): before any absorption of V(I), a pulled-back centre containing the strict transform of h⁻¹(V(I)) forces the centre to contain the strict transform of V(I), because the generic point η_n of X̄_n lies over η and hence in the image of the stage lift [Kol07, Corollary 22, proof].

theorem Hironaka.Resolution.not_centerContains_pullback_of_lt_firstCenterIndex {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsLocallyNoetherian Y] (I : X.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑I.support) (I' : Y.IdealSheafData) [AlgebraicGeometry.IsReduced I'.subscheme] {η' : ↥Y} (hη' : IsGenericPoint η' ↑I'.support) (hηη' : h η' = η) (n : ℕ) : n < firstCenterIndex S I → ¬CenterContains (S.pullback h) I' n

Below the first downstairs absorption of V(I) there is no upstairs absorption of a component V(I') of its preimage dominating it (strong induction on the stage, the histories of both sides carried along).

theorem Hironaka.Resolution.firstCenterIndex_pullback_of_flat_of_le {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsLocallyNoetherian Y] (I : X.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑I.support) (I' : Y.IdealSheafData) [AlgebraicGeometry.IsIntegral I'.subscheme] (hle : I.comap h ≤ I') {η' : ↥Y} (hη' : IsGenericPoint η' ↑I'.support) (hηη' : h η' = η) : firstCenterIndex (S.pullback h) I' = firstCenterIndex S I

Along a flat h, for an integral V(I) with generic point η and an integral component V(I') of its preimage (I.comap h ≤ I', with generic point η' over η), the first-centre index of the pulled-back sequence for V(I') is the first-centre index of V(I) Kol07, Corollary 22, proof; Definition 30, 30.1: downstairs to upstairs by monotonicity through I.comap h ≤ I' (centerContains_pullback_of_le), upstairs to downstairs before the first downstairs absorption by the generic points (not_centerContains_pullback_of_lt_firstCenterIndex). This is the form used for the components of the affine resolution functor.

theorem Hironaka.Resolution.firstCenterIndex_pullback_of_flat_of_mem_range {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] [AlgebraicGeometry.IsLocallyNoetherian X] (I : X.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑I.support) (hmem : η ∈ Set.range ⇑h) : firstCenterIndex (S.pullback h) (I.comap h) = firstCenterIndex S I

Along a flat h whose image contains the generic point of the integral V(I), the first-centre index of the pulled-back sequence for h⁻¹(V(I)) is the first-centre index of V(I) Kol07, Corollary 22, proof: the counterpart of firstCenterIndex_pullback_of_flat_surjective for a flat morphism that need not be surjective.