The data BD_{n,m,j} unfolded, and the closed set Z_{-1}

The data. BDData n m j is a structure; the lemmas here read its fields as Kollár prints [Kol07, Lemma 102]: the value on a triple of the class is a smooth blow-up sequence of order m starting with (X, I, E) (seq_isOrderSeq, the functor's own field), it contains no empty blow-up (seq_noEmptyCenters, [Kol07, 32]), and clause (1), cosupp(I_r, m) disjoint from Π^{-1}_* E^j, says that at every point of the birational transform of E^j the final ideal has order < m (ord_lt_of_mem_strictTransformSeq). The three unfolding lemmas of the domain are definitional.

The closed set Z_{-1}. Zminus1 I m D is the vanishing ideal sheaf of ⨆ η, closure {η} over the generic points η of V(D) with ord_η I ≥ m. On a Noetherian space the generic points are finitely many (Closeds.genericPoints_finite, Hironaka/Scheme/Snc/Dictionary.lean), so the ⨆ is a finite union of closures, itself closed, and a point lies on Z_{-1} iff some selected generic point specializes to it (mem_support_Zminus1_iff: Kollár's union of the irreducible components of E^j contained in cosupp(I, m); a component is contained in cosupp(I, m) iff its generic point is, since the order can only grow under specialization, Hironaka/Scheme/IdealSheaf/Order/Specialization.lean). Hence Z_{-1} ⊆ cosupp(I, m) (support_Zminus1_subset_cosupp) and Z_{-1} ⊆ E^j (support_Zminus1_le_support; support_Zminus1_le for a triple). With max-ord I = m the selected components are exactly those along which I has order m (mem_support_Zminus1_iff_ord_eq: ord_η I ≤ max-ord I).

The dichotomy of a D-balanced ideal. Kollár's remark after [Kol07, Definition 83], that a D-balanced ideal with max-ord I = m has order 0 or m at every point, is IsDBalanced.ord_eq_zero_or_eq (Hironaka/Resolution/Algebraic/Balanced/Order.lean); at the generic points of the components of E^j it is ord_eq_zero_or_eq_of_mem_genericPoints.

Used by Center.lean and, outside this directory, by Hironaka/Resolution/Algebraic/Wlo05/Embedded.lean and Hironaka/Resolution/Algebraic/Wlo05/EmbeddedComponentTools.lean.

The domain and the data unfolded

theorem AlgebraicGeometry.Triple.hasDimLE_iff {k : Type u} [Field k] (T : Triple k) (n : ℕ) : T.HasDimLE n ↔ ∃ n' ≤ n, T.HasDim n'

HasDimLE T n unfolds to some HasDim n' with n' ≤ n.

theorem AlgebraicGeometry.Triple.bdClass_iff {k : Type u} [Field k] (n m j : ℕ) (T : Triple k) : BDClass n m j T ↔ T.HasDimLE n ∧ T.I.maxOrd ≤ ↑m ∧ j < Fintype.card T.E.ι

The domain of BD_{n,m,j} unfolds to its three conditions.

theorem AlgebraicGeometry.Scheme.DivisorFamily.nth_eq {X : Scheme} (E : X.DivisorFamily) (j : Fin (Fintype.card E.ι)) : E.nth j = E.component ((monoEquivOfFin E.ι ⋯) j)

E^j is the component at position j of the linear order of the index set.

theorem Hironaka.BDData.seq_isOrderSeq {k : Type u} [Field k] [CharZero k] {n m j : ℕ} (B : BDData n m j) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) : ((B.functor k).seq T hT).IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m

The value of the data on a triple of the class is a smooth blow-up sequence of order m starting with (X, I, E) ([Kol07, Lemma 102]): the functor's own field.

theorem Hironaka.BDData.seq_noEmptyCenters {k : Type u} [Field k] [CharZero k] {n m j : ℕ} (B : BDData n m j) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) : ((B.functor k).seq T hT).NoEmptyCenters

The output contains no empty blow-up ([Kol07, 32]).

theorem Hironaka.BDData.ord_lt_of_mem_strictTransformSeq {k : Type u} [Field k] [CharZero k] {n m j : ℕ} (B : BDData n m j) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) {x : ↥(((B.functor k).seq T hT).stage (Fin.last ((B.functor k).seq T hT).length))} (hx : x ∈ (((B.functor k).seq T hT).strictTransformSeq (T.E.nth ⟨j, ⋯⟩) (Fin.last ((B.functor k).seq T hT).length)).support) : (((B.functor k).seq T hT).weakTransformSeq T.I (Fin.last ((B.functor k).seq T hT).length)).ord x < ↑m

At every point of the birational transform of E^j on X_r the final induced ideal has order < m: the pointwise form of clause (1) of [Kol07, Lemma 102], cosupp(I_r, m) ∩ Π^{-1}_* E^j = ∅.

The closed set underlying Z_{-1}

theorem Hironaka.BD.coe_support_Zminus1 {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) : ↑(Zminus1 I m D).support = {x : ↥X | ∃ η ∈ D.support.genericPoints, ↑m ≤ I.ord η ∧ η ⤳ x}

On a Noetherian space the closed set of Z_{-1} is the union of the closures of the selected generic points, finitely many (Closeds.genericPoints_finite), so the ⨆ of Closeds is the plain union.

theorem Hironaka.BD.support_Zminus1_le_support {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) : (Zminus1 I m D).support ≤ D.support

Z_{-1} ⊆ V(D): the selected components are components of V(D).

theorem Hironaka.BD.noetherianSpace_triple {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) : TopologicalSpace.NoetherianSpace ↥T.X.left

A triple's ambient scheme is a Noetherian space: finite type and quasi-compact over the field (Scheme.Hom.isNoetherian_of_field, Hironaka/Scheme/IdealSheaf/Order/Constructible.lean).

theorem Hironaka.BD.mem_support_Zminus1_iff {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (x : ↥T.X.left) : x ∈ (Zminus1 T.I m (T.E.component j)).support ↔ ∃ η ∈ (T.E.component j).support.genericPoints, ↑m ≤ T.I.ord η ∧ η ⤳ x

A point lies on Z_{-1} iff it lies on the closure of a generic point of E^j of order ≥ m (Kollár's description of Z_{-1} in the proof of [Kol07, Lemma 102]).

theorem Hironaka.BD.support_Zminus1_subset_cosupp {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : ↑(Zminus1 T.I m (T.E.component j)).support ⊆ {x : ↥T.X.left | ↑m ≤ T.I.ord x}

Z_{-1} ⊆ cosupp(I, m): the order can only grow under specialization.

theorem Hironaka.BD.support_Zminus1_le {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : (Zminus1 T.I m (T.E.component j)).support ≤ (T.E.component j).support

Z_{-1} ⊆ E^j.

theorem Hironaka.BD.ord_eq_zero_or_eq_of_mem_genericPoints {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m) (hmax : T.I.maxOrd = ↑m) {η : ↥T.X.left} (_hη : η ∈ (T.E.component j).support.genericPoints) : T.I.ord η = 0 ∨ T.I.ord η = ↑m

For D-balanced I with max-ord I = m, ord_{E^{jk}} I ∈ {0, m} for every irreducible component E^{jk} of E^j (the remark after [Kol07, Definition 83]). The hypothesis hη is part of the statement so that it reads as Kollár's remark about the components of E^j, the order along a component being the order at its generic point, in the form Transform.lean uses; the proof does not need it, because the dichotomy of a D-balanced ideal (IsDBalanced.ord_eq_zero_or_eq) holds at every point, generic or not.

theorem Hironaka.BD.mem_support_Zminus1_iff_ord_eq {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) (x : ↥T.X.left) : x ∈ (Zminus1 T.I m (T.E.component j)).support ↔ ∃ η ∈ (T.E.component j).support.genericPoints, T.I.ord η = ↑m ∧ η ⤳ x

With max-ord I = m, the components of E^j contained in cosupp(I, m) are exactly those along which I has order m.