The strict transform of an integral closed subscheme stays integral off the centers

In the proof of [Kol07, Corollary 22] the resolution of a variety is read off a principalization of its ideal sheaf in an ambient smooth variety: there is a unique j such that π_0 ⋯ π_{j−1} : P_j → P "is a local isomorphism around η_X", and then η_X is the generic point of the center Z_j. This module supplies the general facts behind that sentence. For a closed subscheme V(J) with V(J) integral and a center D not containing it (¬ D ≤ J):

• the generic point η of V(J) lies off the center, so the blow-up π is an isomorphism near it (blowUp.isIso_π_restrict_compl_support): exactly one point η' of the blow-up lies over η, and specializations between points off the exceptional divisor are reflected by π;
• the strict transform V(Jˢ) has support closure (π⁻¹(V(J)) ∖ π⁻¹(V(D))) (coe_support_saturate; this is the strict transform of [Hau14, Definition 6.2]), which is closure {η'}: η' is its generic point;
• V(Jˢ) is reduced (Hironaka/Scheme/BlowUp/Transform/Reduced.lean), hence integral.

Along a blow-up sequence the same holds at every stage i no earlier center of which contains the strict transform, by structural recursion on the sequence: the strict transform X̄_i is integral, its generic point η_i is the unique point of the stage over η, and Π_i η_i = η, which is Kollár's "π_0 ⋯ π_{j−1} is a local isomorphism around η_X" read on the fibre. The resolution functor of [Kol07, Theorem 36] uses this to locate its end result over the generic point.

Conventions

D.blowUp, D.blowUpπ and strictTransform D J are the definitions used in the statements of the main theorems, definitionally AlgebraicGeometry.Scheme.IdealSheafData.blowUp D, IdealSheafData.blowUpπ D and strictTransformAlong (IdealSheafData.blowUpπ D) (D.comap (IdealSheafData.blowUpπ D)) J. Containment of a center in the strict transform is the ideal inequality S.center i ≤ S.strictTransformSeq J i.castSucc (the stop rule CenterContains of Hironaka/Resolution/Algebraic/Kol07/Thm36/Affine.lean); "no center before i contains the strict transform" is the hypothesis ∀ m (hm : m < i), ¬ S.center ⟨m, _⟩ ≤ S.strictTransformSeq J ⟨m, _⟩.

One blow-up: the fibre over a point off the center, and specializations

theorem AlgebraicGeometry.mem_compl_support_iff {X : Scheme} (D : X.IdealSheafData) (x : ↥X) : x ∈ D.support.compl ↔ x ∉ D.support

A point of X lies in the open complement of the center iff it is not in its support.

theorem AlgebraicGeometry.specializes_of_π_specializes {X : Scheme} (D : X.IdealSheafData) {y y' : ↥D.blowUp} (hy : D.blowUpπ y ∉ D.support) (hy' : D.blowUpπ y' ∉ D.support) (h : D.blowUpπ y ⤳ D.blowUpπ y') : y ⤳ y'

The blow-up reflects specializations between points lying off the exceptional divisor (π is an isomorphism over the complement of the center).

theorem AlgebraicGeometry.π_eq_of_notMem_support {X : Scheme} (D : X.IdealSheafData) {y y' : ↥D.blowUp} (hy : D.blowUpπ y ∉ D.support) (h : D.blowUpπ y = D.blowUpπ y') : y = y'

The blow-up is injective on the points lying off the exceptional divisor.

One blow-up: the generic point of the strict transform

theorem AlgebraicGeometry.genericPoint_notMem_support_of_not_subset {X : Scheme} (D J : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑J.support) (hnot : ¬↑J.support ⊆ ↑D.support) : η ∉ D.support

The generic point of an irreducible closed subscheme V(J) not contained in V(D) lies off the center: otherwise V(J) = closure {η} ⊆ V(D).

theorem AlgebraicGeometry.isGenericPoint_strictTransform {X : Scheme} (D : X.IdealSheafData) [IsLocallyNoetherian X] (J : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑J.support) (hηD : η ∉ D.support) {η' : ↥D.blowUp} (hη' : D.blowUpπ η' = η) : IsGenericPoint η' ↑(J.strictTransform D).support

The one-blow-up case of "η_X is the generic point of Z_j" in the proof of [Kol07, Corollary 22]: the unique point η' over the generic point η of V(J) (off the center) is the generic point of the strict transform of V(J). Its support is closure (π⁻¹(V(J)) ∖ π⁻¹(V(D))) (coe_support_saturate), every point of which is a specialization of η' since π reflects specializations off the exceptional divisor.

theorem AlgebraicGeometry.irreducibleSpace_strictTransform_subscheme {X : Scheme} (D : X.IdealSheafData) [IsLocallyNoetherian X] (J : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑J.support) (hηD : η ∉ D.support) : IrreducibleSpace ↥(J.strictTransform D).subscheme

The strict transform of an irreducible closed subscheme not contained in the center is irreducible (its support has the generic point η').

One blow-up: integrality

theorem AlgebraicGeometry.le_of_support_subset {X : Scheme} (D J : X.IdealSheafData) [IsReduced J.subscheme] (h : ↑J.support ⊆ ↑D.support) : D ≤ J

For a reduced closed subscheme V(J), containment of the supports V(J) ⊆ V(D) is the ideal inequality D ≤ J (vanishingIdeal_support = radical, and J is radical).

theorem AlgebraicGeometry.exists_isGenericPoint_support {X : Scheme} (J : X.IdealSheafData) [IsIntegral J.subscheme] : ∃ (η : ↥X), IsGenericPoint η ↑J.support

The generic point of an integral closed subscheme V(J) (as a point of X): the image of the generic point of the scheme V(J).

theorem AlgebraicGeometry.isIntegral_strictTransform_subscheme {X : Scheme} (D : X.IdealSheafData) [IsLocallyNoetherian X] (J : X.IdealSheafData) [IsIntegral J.subscheme] (hnot : ¬D ≤ J) : IsIntegral (J.strictTransform D).subscheme

The strict transform of an integral closed subscheme V(J) along a blow-up whose center does not contain it (¬ D ≤ J) is integral: irreducible by isGenericPoint_strictTransform and reduced by isReduced_strictTransform_subscheme.

Along a blow-up sequence

theorem AlgebraicGeometry.isLocallyNoetherian_stage {X : Scheme} [IsLocallyNoetherian X] (S : X.BlowUpSequence) (i : Fin (S.length + 1)) : IsLocallyNoetherian (S.stage i)

Every stage of a blow-up sequence on a locally Noetherian scheme is locally Noetherian (blowUp.isLocallyNoetherian at each step).

theorem AlgebraicGeometry.isIntegral_strictTransformSeq_mk {X : Scheme} (hX : IsLocallyNoetherian X) (S : X.BlowUpSequence) (J : X.IdealSheafData) (hJ : IsIntegral J.subscheme) (n : ℕ) (hn : n < S.length + 1) (h : ∀ (m : ℕ) (hm : m < n), ¬S.center ⟨m, ⋯⟩ ≤ S.strictTransformSeq J ⟨m, ⋯⟩) : IsIntegral (S.strictTransformSeq J ⟨n, hn⟩).subscheme

The strict transform of an integral closed subscheme along a blow-up sequence stays integral at every stage n such that no earlier center contains the strict transform (in the ⟨n, hn⟩ form of the indices; structural recursion on the sequence).

theorem AlgebraicGeometry.isIntegral_strictTransformSeq {X : Scheme} [hX : IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [hJ : IsIntegral J.subscheme] (i : Fin (S.length + 1)) (h : ∀ (m : Fin S.length), ↑m < ↑i → ¬S.center m ≤ S.strictTransformSeq J m.castSucc) : IsIntegral (S.strictTransformSeq J i).subscheme

isIntegral_strictTransformSeq_mk in the Fin form of the indices: the strict transform of an integral closed subscheme is integral at every stage i no earlier center of which contains the strict transform.

theorem AlgebraicGeometry.exists_isGenericPoint_strictTransformSeq_mk {X : Scheme} (hX : IsLocallyNoetherian X) (S : X.BlowUpSequence) (J : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑J.support) (hJ : IsReduced J.subscheme) (n : ℕ) (hn : n < S.length + 1) (h : ∀ (m : ℕ) (hm : m < n), ¬S.center ⟨m, ⋯⟩ ≤ S.strictTransformSeq J ⟨m, ⋯⟩) : ∃ (η' : ↥(S.stage ⟨n, hn⟩)), IsGenericPoint η' ↑(S.strictTransformSeq J ⟨n, hn⟩).support ∧ (S.stageMap ⟨n, hn⟩) η' = η ∧ ∀ (y : ↥(S.stage ⟨n, hn⟩)), (S.stageMap ⟨n, hn⟩) y = η → y = η'

Along a sequence (the proof of [Kol07, Corollary 22]): if no center before stage n contains the strict transform of the integral V(J), the strict transform at stage n has a generic point η_n, which is the unique point of the stage over the generic point η of V(J) (the stage map Π_n is a local isomorphism around η).

theorem AlgebraicGeometry.exists_isGenericPoint_strictTransformSeq {X : Scheme} [hX : IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑J.support) [hJ : IsReduced J.subscheme] (i : Fin (S.length + 1)) (h : ∀ (m : Fin S.length), ↑m < ↑i → ¬S.center m ≤ S.strictTransformSeq J m.castSucc) : ∃ (η' : ↥(S.stage i)), IsGenericPoint η' ↑(S.strictTransformSeq J i).support ∧ (S.stageMap i) η' = η ∧ ∀ (y : ↥(S.stage i)), (S.stageMap i) y = η → y = η'

exists_isGenericPoint_strictTransformSeq_mk in the Fin form of the indices.

theorem AlgebraicGeometry.notMem_center_support_of_stageMap_eq_mk {X : Scheme} (hX : IsLocallyNoetherian X) (S : X.BlowUpSequence) (J : X.IdealSheafData) (hJ : IsIntegral J.subscheme) {η : ↥X} (hη : IsGenericPoint η ↑J.support) (m : ℕ) (hm : m < S.length) (h : ∀ (m' : ℕ) (hm' : m' ≤ m), ¬S.center ⟨m', ⋯⟩ ≤ S.strictTransformSeq J ⟨m', ⋯⟩) (y : ↥(S.stage ⟨m, ⋯⟩)) (hy : (S.stageMap ⟨m, ⋯⟩) y = η) : y ∉ (S.center ⟨m, hm⟩).support

"π_0 ⋯ π_{j−1} is a local isomorphism around η_X" (the proof of [Kol07, Corollary 22]), in the form the resolution functor uses: if no center up to stage m contains the strict transform of the integral V(J), no point of the m-th center lies over the generic point η of V(J). The only point of stage m over η is the generic point η_m of the strict transform X̄_m, and η_m ∉ Z_m since Z_m does not contain the irreducible reduced X̄_m.

theorem AlgebraicGeometry.notMem_center_support_of_stageMap_eq {X : Scheme} [hX : IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [hJ : IsIntegral J.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑J.support) (i : Fin S.length) (h : ∀ m ≤ i, ¬S.center m ≤ S.strictTransformSeq J m.castSucc) (y : ↥(S.stage i.castSucc)) (hy : (S.stageMap i.castSucc) y = η) : y ∉ (S.center i).support

notMem_center_support_of_stageMap_eq_mk in the Fin form of the indices: no restricted center over the generic point before the first containing center.