Lemma 102 at the mark m = 0

On BDClass n 0 j the ideal I is the unit ideal (max-ord I ≤ 0), so cosupp(I, 0) is all of X and clause (1) of [Kol07, Lemma 102] asks that the birational transform of E^j be EMPTY at the end. The functor BD.zeroFunctor (Assembly.lean) is π_{-1}, the blow-up of Z_{-1}, which at mark 0 is the union of ALL components of E^j, with its empty blow-up deleted. Kollár's marks are ≥ 1, so this case is not in the source; this module proves its clauses:

• eq_top_of_bdClass_zero: I = O_X (eq_top_of_maxOrd_le_zero: every point of the support would have order ≥ 1).
• disjoint_cosupp_zeroFunctor (clause (1)): every point of E^j lies in Z_{-1} (support_component_subset_support_Zminus1_zero: it specializes from a generic point of E^j, all of which are selected at mark 0), so the saturation of E^j by Z_{-1} has empty support and the strict transform of E^j along π_{-1} is the unit ideal (mem_support_saturate_iff, strictTransform_eq_comap_saturate of Transform.lean). If Z_{-1} itself is the unit ideal then so is E^j, the blow-up is deleted and the sequence is empty; either way the final strict transform of E^j is the unit ideal, whose support is empty.
• zeroFunctor_commutesWithSmooth, zeroFunctor_commutesWithBaseChange (clause (2)): Z_{-1} pulls back along smooth morphisms and changes of fields (Zminus1_pullback, Zminus1_baseChange, stated for every mark), and deleting empty blow-ups commutes with a flat surjective pull-back (eraseEmpty_pullback_of_flat_surjective) and is idempotent under any flat pull-back (eraseEmpty_pullback_eraseEmpty').
• bdDataZero, exists_bdDataZero: the assembled BDData n 0 j.

Used by AssemblyTuned.lean, and outside this directory by Hironaka/Resolution/Algebraic/Kol07/Thm35/Principalization/Monomial.lean, Hironaka/Resolution/Algebraic/Hir64/MainTheoremIIN.lean, Hironaka/Resolution/Algebraic/Stage/ClosedEmbeddingHypersurface.lean and Hironaka/Resolution/Algebraic/Stage/Congr.lean.

theorem Hironaka.BD.eq_top_of_maxOrd_le_zero {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (h : I.maxOrd ≤ ↑0) : I = ⊤

An ideal sheaf of maximal order ≤ 0 is the unit ideal.

theorem Hironaka.BD.eq_top_of_bdClass_zero {k : Type u} [Field k] (n j : ℕ) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n 0 j T) : T.I = ⊤

On BDClass n 0 j, max-ord I ≤ 0 forces I to be the unit ideal; the fact needs no hypothesis on the characteristic.

theorem Hironaka.BD.support_component_subset_support_Zminus1_zero {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (i : T.E.ι) : ↑(T.E.component i).support ⊆ ↑(Zminus1 T.I 0 (T.E.component i)).support

At mark 0 every component of E^j is selected: E^j ⊆ Z_{-1} as closed sets.

theorem Hironaka.BD.zeroFunctor_seq {k : Type u} [Field k] [CharZero k] (n j : ℕ) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n 0 j T) : (zeroFunctor n j).seq T hT = (piMinusOne T.I 0 (T.E.nth ⟨j, ⋯⟩)).eraseEmpty

The value of BD_{n,0,j} is π_{-1}, the blow-up of Z_{-1}, with its empty blow-up deleted ([Kol07, 32]).

theorem Hironaka.BD.strictTransform_Zminus1_zero_eq_top {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (i : T.E.ι) : (T.E.component i).strictTransform (Zminus1 T.I 0 (T.E.component i)) = ⊤

At mark 0 the strict transform of E^j along π_{-1} is the unit ideal: the saturation of E^j by Z_{-1} ⊇ E^j has empty support (mem_support_saturate_iff, Transform.lean).

theorem Hironaka.BD.disjoint_cosupp_zeroFunctor {k : Type u} [Field k] [CharZero k] (n j : ℕ) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n 0 j T) : Disjoint {x : ↥(((zeroFunctor n j).seq T hT).stage (Fin.last ((zeroFunctor n j).seq T hT).length)) | ↑0 ≤ (((zeroFunctor n j).seq T hT).weakTransformSeq T.I (Fin.last ((zeroFunctor n j).seq T hT).length)).ord x} ↑(((zeroFunctor n j).seq T hT).strictTransformSeq (T.E.nth ⟨j, ⋯⟩) (Fin.last ((zeroFunctor n j).seq T hT).length)).support

Clause (1) of [Kol07, Lemma 102] at m = 0: cosupp(I_r, 0) is everything and the birational transform of E^j under the blow-up of Z_{-1} = E^j is empty, so the two are disjoint (the form BDData.disjoint_cosupp takes).

theorem Hironaka.BD.zeroFunctor_commutesWithSmooth {k : Type u} [Field k] [CharZero k] (n j : ℕ) : (zeroFunctor n j).CommutesWithSmooth

BD_{n,0,j} commutes with smooth morphisms ([Kol07, 34.1]; clause (2) of [Kol07, Lemma 102] at m = 0): Z_{-1} pulls back (Zminus1_pullback) and deleting empty blow-ups commutes with a flat surjective pull-back.

theorem Hironaka.BD.zeroFunctor_commutesWithBaseChange {k : Type u} [Field k] [CharZero k] (n j : ℕ) {L : Type u} [Field L] [CharZero L] (σ : k →+* L) : (zeroFunctor n j).CommutesWithBaseChange (zeroFunctor n j) σ

BD_{n,0,j} commutes with change of fields ([Kol07, 34.2]; clause (2) of [Kol07, Lemma 102] at m = 0): Zminus1_baseChange.

noncomputable def Hironaka.BD.bdDataZero (n j : ℕ) : BDData n 0 j

BD_{n,0,j} over every field of characteristic zero (clauses (1)–(2) of [Kol07, Lemma 102] at m = 0), assembled from zeroFunctor and its clauses.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.BD.exists_bdDataZero (n j : ℕ) : ∃ (D : BDData n 0 j), ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n 0 j T), (D.functor k).seq T hT = (zeroFunctor n j).seq T hT

Clauses (1)–(2) of [Kol07, Lemma 102] at the mark 0: a BDData n 0 j whose functor over every field is zeroFunctor (existential form of bdDataZero).