The core lemma of the smooth case, and the empty succession

The core lemma (core_bmoOneRun : Core k): for a marked triple (X, I, 1, ∅) whose V(I) is regular stalkwise and with I ≠ 𝒪_X, the run of BMO_1 starts with a blow-up whose centre contains a generic point of V(I). Proved for the tower of order reductions stage by stage (CoreAt n, induction on the stage as for Kollár's Claim 71.2 in [Kol07, 108]), for V(I) smooth over k:

• stage 0: I = 𝒪_X (Triple.I_eq_top_of_hasDimLE_zero), nothing to prove;
• stage n + 1: max-ord I = 1 (maxOrd_eq_one_of_smooth_of_ne_top); the local cover g : X' → X of [Kol07, Theorem 105] (globalizationData_localClass, Triple.exists_isLocalCover) carries a smooth hypersurface H ⊇ V(I') of maximal contact for (I', 1), and BMO_1 commutes with the smooth surjection g ([Kol07, Theorem 107 (2)]); on X', either (A) some component of H lies in V(I') (Z_{-1}(I', 1, H) ≠ 𝒪_{X'}): BMO_1 = BO_1 at the mark (Kollár's Claim 71.1, tower_bmo_eq_bo_of_maxOrd), BO_1 on X' is Step 2 for H (functor_seq_localClass) whose first blow-up is Z_{-1} itself (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCaseA) — a generic point of a selected component of H is a generic point of V(I') in the centre; or (B) Z_{-1} = 𝒪_{X'}: I' = j_* (I'|_H) with I'|_H nonzero on every component of H (isNonzeroEverywhere_comap_subschemeι_of_Zminus1_eq_top), so the hypersurface case of the descent along closed embeddings (tower_bmo_one_eq_pushforward_of_isSmoothDivisor_ker) brings the run down to (H, I'|_H, 1, ∅) at the stage n (coherence of the tower), where the induction hypothesis gives the centre; the generic point is carried back along j (mem_genericPoints_support_map_iff). Finally the centre and its generic point are carried back along the cover (mem_genericPoints_of_openImmersionCoprods).

The empty succession (bed_eq_nil_of_smooth): for a smooth reduced Y the embedded desingularization sequence BED(X, I_Y, ∅) is the empty succession ([Wlo05, 4.6]), by bed_eq_nil_of_smooth_of_core (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilSmooth) — the loop on (X, I_Y, ∅) absorbs a component at stage 0 of every round and never blows up. The clauses of the theorem do not need this statement; it records that the sequence does nothing on a smooth Y. The general tools are in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCoreTools.

def Hironaka.Resolution.CoreAt (k : Type u) [Field k] [CharZero k] (n : ℕ) : Prop

The core lemma at the stage n of the tower — for a marked triple of BMOClass n 1 with empty boundary, V(I) smooth over k and I ≠ 𝒪_X, the stage-n functor's run starts with a blow-up whose centre contains a generic point of V(I).

Equations

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

theorem Hironaka.Resolution.coreAt_zero {k : Type u} [Field k] [CharZero k] : CoreAt k 0

Stage 0: the ideal is the unit ideal (the base case of the tower), so there is nothing to prove.

theorem Hironaka.Resolution.mem_support_Zminus1_of_mem {X : AlgebraicGeometry.Scheme} (I H : X.IdealSheafData) {ξ : ↥X} (hgen : ξ ∈ H.support.genericPoints) (hord : ↑1 ≤ I.ord ξ) : ξ ∈ (BD.Zminus1 I 1 H).support

A selected generic point of H lies in Z_{-1}(I, 1, H).

theorem Hironaka.Resolution.exists_cons_of_pullback_eq_cons {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (g : Y ⟶ X) {D' : Y.IdealSheafData} {rest' : D'.blowUp.BlowUpSequence} (h : S.pullback g = AlgebraicGeometry.Scheme.BlowUpSequence.cons Y D' rest') : ∃ (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence), S = AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest ∧ D.comap g = D'

A sequence whose pullback starts with a blow-up starts with a blow-up, of the centre whose pullback is the given one.

theorem Hironaka.Resolution.coreAt_succ {k : Type u} [Field k] [CharZero k] (n : ℕ) (ih : CoreAt k n) : CoreAt k (n + 1)

The induction step — Kollár's local chain (the cover of [Kol07, Theorem 105] with a hypersurface of maximal contact), the absorbed-component case through the first blow-up of [Kol07, Lemma 102], the other case through the hypersurface descent to the stage below.

theorem Hironaka.Resolution.coreAt {k : Type u} [Field k] [CharZero k] (n : ℕ) : CoreAt k n

The core lemma at every stage of the tower.

theorem Hironaka.Resolution.core_bmoOneRun {k : Type u} [Field k] [CharZero k] : Core k

The core lemma of the smooth case — for a marked triple (X, I, 1, ∅) whose V(I) is regular stalkwise (hence smooth over k) and with I ≠ 𝒪_X, the run of BMO_1 (BMO_m 1 k, the tower at the stage dim X) starts with a blow-up whose centre contains a generic point of V(I).

theorem Hironaka.Resolution.bed_eq_nil_of_smooth {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (hE : IsEmpty TX.E.ι) (hY : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp TX.I.subschemeι (TX.X.left ↘ AlgebraicGeometry.Spec ↧k))) : BED TX = AlgebraicGeometry.Scheme.BlowUpSequence.nil TX.X.left

The empty succession for a smooth Y — for a smooth reduced Y the embedded desingularization sequence BED(X, I_Y, ∅) is the empty succession ([Wlo05, 4.6]).