Before the first containing centre

Kollár's construction of the resolution of an embedded affine scheme X ⊆ A truncates the principalization sequence of I_X at the first index j whose centre Z_j contains the strict transform of X [Kol07, Corollary 22, proof]: before that index "π_0 ⋯ π_{j−1} is a local isomorphism around η_X". This file records what holds at the stages i ≤ j, on top of the definitions CenterContains, firstCenterIndex and BR_affine of Hironaka.Resolution.Algebraic.Kol07.Thm36.Affine:

• not_centerContains_of_lt_firstCenterIndex': no centre before firstCenterIndex S I contains the strict transform of V(I), whether or not a containing centre exists (if there is none, firstCenterIndex S I = S.length and the statement covers every centre of S);
• isIntegral_strictTransformSeq_of_le_firstCenterIndex: for an integral V(I) the strict transforms X̄_i, i ≤ firstCenterIndex S I, are integral; exists_isGenericPoint_strictTransformSeq_of_le_firstCenterIndex: their generic points η_i are the unique points of the stages over the generic point η of V(I); notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex: no point of a centre Z_i, i < firstCenterIndex S I, lies over η;
• ker_pullbackStageHom_last_BR_affine: the end result of BR_affine TA emb embeds in the last stage of the truncated principalization sequence with kernel the strict transform of I_X [Kol07, Definition 30, 30.2].

The identification of X̄_j with the irreducible component of the smooth centre Z_j through η_j is Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification; the transport of the generic point by local isomorphisms is Hironaka.Resolution.Algebraic.Wlo05.FirstCenterLocalIso.

Conventions

CenterContains S I n is the ideal inequality S.center ⟨n, _⟩ ≤ S.strictTransformSeq I ⟨n, _⟩ (Z_n ⊇ X̄_n as closed subschemes of the stage), and firstCenterIndex S I is the least such n, or S.length if there is none.

Before the first containing centre

theorem Hironaka.Resolution.not_centerContains_of_lt_firstCenterIndex' {A : AlgebraicGeometry.Scheme} (S : A.BlowUpSequence) (I : A.IdealSheafData) {n : ℕ} (hn : n < firstCenterIndex S I) : ¬CenterContains S I n

No centre before firstCenterIndex S I contains the strict transform, whether or not a containing centre exists.

theorem Hironaka.Resolution.not_center_le_strictTransformSeq_of_lt_firstCenterIndex {A : AlgebraicGeometry.Scheme} (S : A.BlowUpSequence) (I : A.IdealSheafData) {m : Fin S.length} (hm : ↑m < firstCenterIndex S I) : ¬S.center m ≤ S.strictTransformSeq I m.castSucc

The hypothesis of AlgebraicGeometry.isIntegral_strictTransformSeq at an index i ≤ firstCenterIndex S I: no earlier centre contains the strict transform.

theorem Hironaka.Resolution.isIntegral_strictTransformSeq_of_le_firstCenterIndex {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (I : A.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] (i : Fin (S.length + 1)) (hi : ↑i ≤ firstCenterIndex S I) : AlgebraicGeometry.IsIntegral (S.strictTransformSeq I i).subscheme

Before the first containing centre the strict transforms of an integral closed subscheme are integral [Kol07, Corollary 22, proof].

theorem Hironaka.Resolution.exists_isGenericPoint_strictTransformSeq_of_le_firstCenterIndex {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (I : A.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥A} (hη : IsGenericPoint η ↑I.support) (i : Fin (S.length + 1)) (hi : ↑i ≤ firstCenterIndex S I) : ∃ (η' : ↥(S.stage i)), IsGenericPoint η' ↑(S.strictTransformSeq I i).support ∧ (S.stageMap i) η' = η ∧ ∀ (y : ↥(S.stage i)), (S.stageMap i) y = η → y = η'

"π_0 ⋯ π_{j−1} is a local isomorphism around η_X" [Kol07, Corollary 22, proof]: before the first containing centre, the generic point η_i of the strict transform is the unique point of the stage over the generic point η of V(I).

theorem Hironaka.Resolution.notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (I : A.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥A} (hη : IsGenericPoint η ↑I.support) (i : Fin S.length) (hi : ↑i < firstCenterIndex S I) (y : ↥(S.stage i.castSucc)) (hy : (S.stageMap i.castSucc) y = η) : y ∉ (S.center i).support

No point of a centre before the first containing one lies over the generic point of V(I): the starting point of the proof that the affine resolution is an isomorphism over the smooth locus (Hironaka.Resolution.Algebraic.Kol07.Thm36.IsoOverSmoothLocus).

The end result of BR_affine

theorem Hironaka.Resolution.ker_pullbackStageHom_last_BR_affine {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) : AlgebraicGeometry.Scheme.Hom.ker (((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)).pullbackStageHom emb (Fin.last ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)).length)) = ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)).strictTransformSeq TA.I (Fin.last ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)).length)

The end result of BR_affine TA emb embeds in the last stage of the truncated principalization sequence with kernel the strict transform of I_X: the identification of S_{i+1} with the birational transform (π_i)^{-1}_* S_i ⊂ X_{i+1} of [Kol07, Definition 30, 30.2]. This is ker_pullbackStageHom at the truncated sequence (BP TA).take j, with emb.ker = TA.I.