Transport of the generic point before the first containing centre

In the proof of [Kol07, Corollary 22] there is a unique j such that π_0 ⋯ π_{j−1} is a local isomorphism around η_X while the centre Z_j of π_j contains η_X. Hironaka.Resolution.Algebraic.Kol07.Thm36.FirstCenter proves that at a stage i ≤ firstCenterIndex S I the strict transform of the integral V(I) has a generic point η_i which is the unique point over the generic point η of V(I), and that no earlier centre has a point over η; Hironaka.Resolution.Algebraic.Kol07.OffCenters proves the pointwise transport along a sequence: at a point over no earlier centre the stage map is an isomorphism on stalks and the stalk of the strict transform is the image of the stalk of the subscheme. This file composes the two, in the form needed by Włodarczyk's embedded desingularization, whose components are transported until the first stage at which a centre contains them (Hironaka.Resolution.Algebraic.Wlo05.Embedded).

• le_firstCenterIndex_of_forall_lt_not: if no centre before n contains the strict transform, then n ≤ firstCenterIndex S I;
• stageMapBetween_notMem_center_support_of_le_firstCenterIndex: the transports of a point over η avoid every earlier centre;
• stalkIdeal_markedTransformSeq_of_forall_notMem: over no earlier centre the stalk of the marked transform is the image of the stalk of the ideal (the exceptional stalks are the unit ideal there), the marked counterpart of stalkIdeal_strictTransformSeq_of_forall_notMem;
• notMem_support_totalTransformSeq_of_forall_notMem: such a point lies on no member of the total transform of a family it did not lie on [Kol07, Definition 25];
• mem_genericPoints_markedTransformSeq_support_of_forall_notMem: the unique point over a generic point of V(I) at which I agrees with an integral J is a generic point of the support of the marked transform (its stalk is the image of J's, and any specialisation to it lies over η);
• exists_isGenericPoint_strictTransformSeq_and_isIso_of_le_firstCenterIndex: the packaged form at a stage ≤ firstCenterIndex.

The results hold on any scheme, locally Noetherian where the integrality of the strict transforms is needed.

The first containing centre

theorem Hironaka.Resolution.le_firstCenterIndex_of_forall_lt_not {A : AlgebraicGeometry.Scheme} (S : A.BlowUpSequence) (I : A.IdealSheafData) {n : ℕ} (hn : n ≤ S.length) (h : ∀ m < n, ¬CenterContains S I m) : n ≤ firstCenterIndex S I

If no centre before n ≤ S.length contains the strict transform of V(I), then n ≤ firstCenterIndex S I (when no centre contains it at all, firstCenterIndex S I = S.length). This is how the minimal absorbing stage of the embedded desingularization loop is compared with the first-centre index of each of its components.

theorem Hironaka.Resolution.stageMapBetween_notMem_center_support_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) {y : ↥(S.stage i)} (hy : (S.stageMap i) y = η) (m : Fin S.length) (hmi : ↑m < ↑i) : (S.stageMapBetween i m.castSucc ⋯) y ∉ (S.center m).support

At a stage i ≤ firstCenterIndex S I, a point y over the generic point η of the integral V(I) is carried by the intermediate stage maps to no earlier centre Kol07, Corollary 22, proof: notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex and the cocycle identity Π_m ∘ Π_{im} = Π_i.

The marked transform off the centres

theorem Hironaka.Resolution.stalkIdeal_markedTransformSeq_of_forall_notMem_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (c j : ℕ) (hj : j < S.length + 1) (p : ↥(S.stage ⟨j, hj⟩)) : (∀ (m : ℕ) (hm : m < S.length) (hmj : m < j), (S.stageMapBetween ⟨j, hj⟩ ⟨m, ⋯⟩ ⋯) p ∉ (S.center ⟨m, hm⟩).support) → (S.markedTransformSeq J c ⟨j, hj⟩).stalkIdeal p = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap ⟨j, hj⟩) p)) (J.stalkIdeal ((S.stageMap ⟨j, hj⟩) p))

The marked transform along a sequence [Kol07, Warning 63, (63.1)] at a point over no earlier centre, in the ⟨j, hj⟩ form of the indices: the stalk of the marked transform of (J, c) at a point of the j-th stage lying over no earlier centre is the image of the stalk of J under the stalk map of the stage map, the exceptional stalk of each step being the unit ideal there (stalkIdeal_markedTransform_of_notMem). The marked counterpart of isIso_stalkMap_stageMap_and_stalkIdeal_strictTransformSeq_mk.

theorem Hironaka.Resolution.stalkIdeal_markedTransformSeq_of_forall_notMem {A : AlgebraicGeometry.Scheme} (S : A.BlowUpSequence) (J : A.IdealSheafData) (c : ℕ) (i : Fin (S.length + 1)) (p : ↥(S.stage i)) (h : ∀ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) p ∉ (S.center m).support) : (S.markedTransformSeq J c i).stalkIdeal p = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap i) p)) (J.stalkIdeal ((S.stageMap i) p))

At a point over no earlier centre, the stalk of the marked transform of (J, c) is the image of the stalk of J under the stalk map of the stage map [Kol07, Warning 63, (63.1)].

Off the boundary

theorem Hironaka.Resolution.notMem_component_support_of_notMem_support {X : AlgebraicGeometry.Scheme} (F : X.DivisorFamily) {p : ↥X} (hp : p ∉ F.support) (l : F.ι) : p ∉ (F.component l).support

A point off the support of a family lies on none of its members.

theorem Hironaka.Resolution.notMem_support_totalTransformSeq_of_forall_notMem {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (E : A.DivisorFamily) (i : Fin (S.length + 1)) (p : ↥(S.stage i)) (h : ∀ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) p ∉ (S.center m).support) (hE : (S.stageMap i) p ∉ E.support) : p ∉ (S.totalTransformSeq E i).support

A point over no earlier centre whose image lies on no member of E lies on no member of the total transform of E at its stage [Kol07, Definition 25] (mem_support_totalTransformSeq_iff).

The generic point of the marked transform's support

theorem Hironaka.Resolution.mem_genericPoints_markedTransformSeq_support_of_forall_notMem {A : AlgebraicGeometry.Scheme} (S : A.BlowUpSequence) (I J : A.IdealSheafData) (c : ℕ) {η : ↥A} (hη : IsGenericPoint η ↑J.support) (hηI : η ∈ I.support.genericPoints) (hIJ : I.stalkIdeal η = J.stalkIdeal η) (i : Fin (S.length + 1)) {η' : ↥(S.stage i)} (hη' : (S.stageMap i) η' = η) (huniq : ∀ (y : ↥(S.stage i)), (S.stageMap i) y = η → y = η') (h : ∀ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) η' ∉ (S.center m).support) : η' ∈ (S.markedTransformSeq I c i).support.genericPoints

Let η be a generic point of supp I at which I agrees with an integral J whose support has generic point η, and let η' be a point over η at stage i which lies over no earlier centre and is the unique point over η. Then η' is a generic point of the support of the marked transform of (I, c) at stage i: its stalk is the image of the proper stalk of J under an isomorphism, and a point of that support specialising to η' lies over a point of supp I specialising to η, hence over η, hence equals η'. (This carries along the sequence the hypothesis "I = I_{Y₁} near a generic point of Y₁" of the Claim in the proof of [Wlo05, Theorem 4.7.1].)

The packaged form

theorem Hironaka.Resolution.exists_isGenericPoint_strictTransformSeq_and_isIso_of_le_firstCenterIndex {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (J : A.IdealSheafData) [AlgebraicGeometry.IsIntegral J.subscheme] {η : ↥A} (hη : IsGenericPoint η ↑J.support) (i : Fin (S.length + 1)) (hi : ↑i ≤ firstCenterIndex S J) : ∃ (η' : ↥(S.stage i)), IsGenericPoint η' ↑(S.strictTransformSeq J i).support ∧ (S.stageMap i) η' = η ∧ (∀ (y : ↥(S.stage i)), (S.stageMap i) y = η → y = η') ∧ (∀ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) η' ∉ (S.center m).support) ∧ CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap i) η')

The transport of the generic point, packaged [Kol07, Corollary 22, proof]: at a stage i ≤ firstCenterIndex S J the strict transform of the integral V(J) has a generic point η', the unique point over the generic point η of V(J); its transports avoid every earlier centre and the stage map is an isomorphism on stalks at it (exists_isGenericPoint_strictTransformSeq_of_le_firstCenterIndex with isIso_stalkMap_stageMap_of_forall_notMem).