A generic point of codimension at least two is absorbed by some centre #
In the proof of [Kol07, Corollary 22] the ideal sheaf I of X, of codimension ≥ 2, is not
locally principal at η_X, so "some blow-up center must contain η_X". This file proves
the statement in a general form, per generic point and without integrality of V(I), as the
embedded desingularization needs it for each component of a reducible subscheme: for a blow-up
sequence S on a locally Noetherian scheme A whose composite makes I invertible (clause (2) of
[Kol07, Theorem 35], a hypothesis here), and a generic point η of an irreducible component of
V(I) with dim 𝒪_{A,η} ≥ 2, some centre of S has a point over η.
Proof. If no centre had a point over η, each blow-up would be an isomorphism near the unique
point over η (isIso_stalkMap_π_of_notMem_support), so the stalk map of the composite at the
point η' over η would be an isomorphism 𝒪_{A,η} ≅ 𝒪_{A_r,η'} carrying I_η to the stalk
of I·𝒪_{A_r}, which is principal since I·𝒪_{A_r} is invertible. So I_η would be principal;
the maximal ideal 𝔪_η is a minimal prime over I_η (η being a generic point of a component of
V(I)), hence of height ≤ 1 by Krull's principal ideal theorem, that is, dim 𝒪_{A,η} ≤ 1,
against the hypothesis.
For an integral V(I) the conclusion is sharpened to the existence of a centre containing the
whole strict transform (exists_centerContains_of_isInvertible_comap_composite): at the least
centre with a point over η, that point is the generic point of the strict transform
(Hironaka.Scheme.BlowUpSequence.StrictTransformIntegral), so the centre's support contains the
whole reduced irreducible strict transform and the ideal inequality CenterContains follows. The
embedded form exists_centerContains_BP_of_isInvertible, for the principalization sequence of the
ambient triple, is the input of Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36.
No center over η: the composite is a local isomorphism at the unique point over η #
If no center of S has a point over η, then at every stage there is a unique point η' over
η, and the stage map is an isomorphism of stalks at it (each blow-up is an isomorphism off its
center). Structural recursion on the sequence, ℕ-indexed.
The algebra: a principal I_η at a generic point of a component forces dim ≤ 1 #
Krull's principal ideal theorem at a generic point of a component of V(I): if the stalk I_η
is principal then dim 𝒪_{A,η} ≤ 1, the maximal ideal 𝔪_η being a minimal prime over I_η
(stalkIdeal_vanishingIdeal_mem_minimalPrimes at x = η), hence of height ≤ 1.
The absorption #
The absorption of a generic point of codimension ≥ 2 [Kol07, Corollary 22, proof], general
form: on a locally Noetherian scheme, if the composite of the blow-up sequence S makes I
invertible (clause (2) of [Kol07, Theorem 35] as a hypothesis) and η is a generic point of an
irreducible component of V(I) with dim 𝒪_{A,η} ≥ 2, then some centre of S has a point over
η.
From a center with a point over η to a center containing the strict transform #
From a centre with a point over the generic point to a centre containing the strict transform
[Kol07, Corollary 22, proof], for an integral V(I): if some centre has a point over the generic
point η of V(I), the least such centre contains the whole strict transform X̄_n. Before it no
centre contains the strict transform (its generic point η_m lies over η), so the point over
η at stage n is η_n, and X̄_n = closure {η_n} ⊆ Z_n gives the ideal inequality
CenterContains S I n (le_of_support_subset, X̄_n being reduced).
The absorption lemma in the composite form and the assembly #
A generic point of an irreducible closed subset is one of its generic points in the sense of
Closeds.genericPoints (the points maximal for specialisation).
The absorption of a generic point in the form used by the embedded desingularization
[Kol07, Corollary 22, proof]: at a generic point η of V(I) where 𝒪_{A,η} has dimension
≥ 2, if the pullback Π^* I along the composite Π of S is invertible, some centre of S has
a point over η. Neither A nor V(I) need be integral.
The absorption assembled for an integral V(I) [Kol07, Corollary 22, proof]: if the pullback
Π^* I along the composite of S is invertible (clause (2) of [Kol07, Theorem 35] for the
principalization sequence) and V(I) has codimension ≥ 2 at its generic point, some centre of
S contains the strict transform of V(I) at its stage.
The embedded situation X ↪ A #
The scheme-theoretic image of a closed immersion of an integral scheme is integral (the image
is isomorphic to the source, Mathlib's Scheme.Hom.toImage).
The image of the generic point of an irreducible X under a closed immersion is a generic point
of the support of its kernel V(I_X).
The generic point of an irreducible scheme is one of its generic points (Mathlib's
genericPoints, the set over which the codimension hypothesis is stated).
The absorption for the ambient triple TA = (A, I_X, E) of an integral closed subscheme
X ↪ A of codimension ≥ 2 at its generic point, with clause (2) of [Kol07, Theorem 35] as the
hypothesis (Π^* I_X is the ideal of a simple normal crossing divisor, hence invertible): some
centre of BP TA contains the strict transform of X. The boundary plays no role, the argument
being local at η_X.