Cosupport forcing: the first center of an order sequence with a one-point cosupport #
Condition (4) of [Kol07, Definition 66] (ord_{Z_i} I_i = m) places every center of a smooth
blow-up sequence of order m inside the cosupport cosupp(I_i, m) = {x : ord_x I_i ≥ m}
([Kol07, Definition 59]; the order along a center is read at its generic points,
[Kol07, Definition 47]), the empty blow-up convention [Kol07, 32] forbids empty centers, and the
conclusion max-ord I_r < m of [Kol07, Theorem 103 (1)] makes the final maximal order drop below
m. When the cosupport of (I, m) is a single closed point x, these three clauses force the
first center: the sequence is not empty (else max-ord I ≥ ord_x I ≥ m), its first center Z₀
has every generic point of order m, hence equal to x, so Z₀ is supported at x and, being
smooth over k (a center with simple normal crossings has a regular, hence reduced, subscheme), is
the reduced point vanishingIdeal {x}.
This is the mechanism by which the worked example [Kol07, Example 106] reads "the first step is to
blow up the origin" from the properties of the order reduction functor alone (the fields of
OrderSeqFunctor and the bound on the final maximal order), without its construction. Nothing of
𝔸⁴, of the ideal of the example or of the origin appears here; the identification of the reduced
point with the ideal of the origin is in HironakaExamples/OrderReduction/Example106.lean. The
point x is any point with IsClosed {x} (a scheme point, not a rational point: the later stages
of the example need the lemma at points of the blown-up scheme), and the hypothesis is IsOrderSeq.
The topological input is Closeds.exists_mem_genericPoints_specializes
(Hironaka/Scheme/IdealSheaf/Order/Specialization.lean): in a sober T₀ space every point of a
closed set Z is a specialization of a generic point of Z.
Cosupport forcing, support form (condition (4) of [Kol07, Definition 66], the empty
blow-up convention [Kol07, 32], and the conclusion of [Kol07, Theorem 103 (1)]). Let S be a
smooth blow-up sequence of order m for (X, I, E) with no empty center whose final weak
transform has maximal order < m, and let the cosupport {y : ord_y I ≥ m} be a single closed
point x. Then S begins with a blow-up, of a center supported exactly at x: the sequence is
not empty (max-ord I ≥ ord_x I ≥ m), every generic point of the first center has order m, so
is x, and the center is nonempty.
The first center of a smooth blow-up sequence of order m over a smooth k-scheme is a
reduced closed subscheme: it has simple normal crossings with the boundary (condition (3) of
[Kol07, Definition 66]), so its subscheme is regular, its stalks are domains, and its ideal sheaf
is the vanishing ideal of its support.
Cosupport forcing, reduced-point form: under the hypotheses of
exists_eq_cons_of_ord_le_iff over a smooth k-scheme, S begins with the blow-up of the reduced
point x, vanishingIdeal {x}, given here through any ideal sheaf Z₀ equal to it (the worked
example supplies the ideal of the origin).