The first center Z_{-1} is a trivial smooth blow-up of order m

In the proof of [Kol07, Lemma 102], Z_{-1} is the union of the irreducible components of E^j contained in cosupp(I, m), and π_{-1} : X_0 → X its blow-up, an isomorphism. This module shows that the blow-up is a smooth blow-up of order m of (X, I, E) in the sense of [Kol07, Definition 65]: its center is smooth, has simple normal crossings with E, and ord_{Z_{-1}} I = m.

The stalks of Z_{-1}. E^j is a component of the snc family E of a triple, so it is reduced (its subscheme is regular, hence its stalks are domains) and equals the vanishing ideal of its support; since Z_{-1} ⊆ E^j as closed sets, E^j ⊆ Z_{-1} as ideal sheaves (component_le_Zminus1). At a point x of Z_{-1} some selected generic point η of E^j specializes to x; the stalk of Z_{-1} at x lies in that of the reduced component closure {η}, which is a minimal prime of E^j_x (stalkIdeal_vanishingIdeal_mem_minimalPrimes, Hironaka/Resolution/Algebraic/Snc/DictionaryComponents.lean); and E^j_x = (z_c) for one member of a regular system of parameters (Kollár's snc coordinates, [Kol07, Definition 24]; IsSncAt), a prime ideal. A prime is its own only minimal prime, so (Z_{-1})_x ⊆ E^j_x, and with the reverse inclusion (Z_{-1})_x = E^j_x = (z_c) (stalkIdeal_Zminus1_eq): near a point of Z_{-1} the two subschemes coincide, the components of the regular E^j being pairwise disjoint.

Consequences. Z_{-1} has simple normal crossings with E (the same coordinates, s = {c}; hasSncWith_Zminus1), hence is smooth over k (smooth_of_hasSncWith, Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Center.lean, k perfect); its stalks are the unit ideal off its support and (z_c) on it, z_c ∈ 𝔪_x ∖ 𝔪_x² a nonzerodivisor of the regular local ring 𝒪_{X,x} (a domain), so Z_{-1} is a Cartier divisor (isInvertible_Zminus1, by the stalkwise criterion of Hironaka/Scheme/IdealSheaf/Invertible.lean) and π_{-1} is an isomorphism (isIso_blowUpπ_Zminus1; blowUp.isIso_π_of_isInvertible, Hironaka/Scheme/BlowUp/Glue/Trivial.lean; [Kol07, Warning 20]). The generic points of Z_{-1} are exactly the selected generic points of E^j (mem_genericPoints_support_Zminus1_iff), along which ord I ≥ m by selection and ≤ max-ord I = m: ord_{Z_{-1}} I = m (ordAlongEq_Zminus1). Together: Definition 65 for the center (isOrderBlowUp_Zminus1) and [Kol07, Definition 66] for the one-step sequence π_{-1} (isOrderSeq_piMinusOne).

Used by Transform.lean and Restriction.lean, and outside this directory by Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP3Raw.lean; imported (for BD.Zminus1) by Hironaka/Resolution/Algebraic/MarkedOrderReduction/Split.lean and Hironaka/Resolution/Algebraic/Wlo05/EmbeddedNilCoreTools.lean.

E^j is reduced, hence contained in Z_{-1} as an ideal sheaf

theorem Hironaka.BD.isReduced_component {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) : AlgebraicGeometry.IsReduced (T.E.component j).subscheme

The subscheme of a component of the snc family of a triple is reduced: its stalks are regular local rings (each E^i is smooth, [Kol07, Definition 24]), hence domains.

theorem Hironaka.BD.support_Zminus1_eq {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : (Zminus1 T.I m (T.E.component j)).support = ⨆ (η : { η : ↥T.X.left // η ∈ (T.E.component j).support.genericPoints ∧ ↑m ≤ T.I.ord η }), TopologicalSpace.Closeds.closure {↑η}

The closed set of Z_{-1} as a Closeds: the ⨆ of the closures of the selected generic points (the support of a vanishing ideal sheaf is the closed set).

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

E^j ⊆ Z_{-1} as ideal sheaves: E^j is reduced and Z_{-1} ⊆ E^j as closed sets.

The stalks of Z_{-1}

theorem Hironaka.BD.exists_stalkIdeal_component_eq_span {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) {x : ↥T.X.left} (hx : x ∈ (T.E.component j).support) : ∃ (n : ℕ) (z : Fin n → ↑(T.X.left.presheaf.stalk x)), T.E.IsSncAt x z ∧ ∃ (c : Fin n), (T.E.component j).stalkIdeal x = Ideal.span {z c}

Kollár's snc coordinates at a point of E^j: E^j_x = (z_c) for a regular system of parameters z of 𝒪_{X,x} ([Kol07, Definition 24, (2)]).

theorem Hironaka.BD.isPrime_stalkIdeal_component {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) {x : ↥T.X.left} (hx : x ∈ (T.E.component j).support) : ((T.E.component j).stalkIdeal x).IsPrime

The stalk of E^j at a point of E^j is prime: it is generated by one member of a regular system of parameters of the regular local ring 𝒪_{X,x} (isPrime_span_singleton_of_parameters, Hironaka/Scheme/Snc/TrivialTotalTransform.lean).

theorem Hironaka.BD.stalkIdeal_Zminus1_eq {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) {x : ↥T.X.left} (hx : x ∈ (Zminus1 T.I m (T.E.component j)).support) : (Zminus1 T.I m (T.E.component j)).stalkIdeal x = (T.E.component j).stalkIdeal x

At a point of Z_{-1} the stalks of Z_{-1} and of E^j coincide (the components of the regular E^j are pairwise disjoint).

theorem Hironaka.BD.exists_stalkIdeal_Zminus1_eq_span {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) {x : ↥T.X.left} (hx : x ∈ (Zminus1 T.I m (T.E.component j)).support) : ∃ (n : ℕ) (z : Fin n → ↑(T.X.left.presheaf.stalk x)), T.E.IsSncAt x z ∧ ∃ (c : Fin n), (Zminus1 T.I m (T.E.component j)).stalkIdeal x = Ideal.span {z c}

At a point of Z_{-1} its stalk is (z_c) for Kollár's snc coordinates z at that point.

Simple normal crossings with E

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

Z_{-1} has simple normal crossings with E ([Kol07, Definition 24, (4)]): at each of its points it is (z_c = 0) in Kollár's coordinates.

Smooth, Cartier, ord_{Z_{-1}} I = m, the sequence

theorem Hironaka.BD.smooth_Zminus1 {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (Zminus1 T.I m (T.E.component j)).subschemeι (T.X.left ↘ AlgebraicGeometry.Spec ↧k))

Z_{-1} is smooth over k ([Kol07, Definition 65, (1)]; [Kol07, Notation 19]): a subscheme with simple normal crossings with an snc family is smooth over a perfect field (smooth_of_hasSncWith).

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

Z_{-1} is a Cartier divisor ([Kol07, Warning 20]): its stalk at every point is the unit ideal or (z_c), a nonzerodivisor of the regular local ring 𝒪_{X,x}.

theorem Hironaka.BD.isIso_blowUpπ_Zminus1 {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : CategoryTheory.IsIso (Zminus1 T.I m (T.E.component j)).blowUpπ

π_{-1} : X_0 → X is an isomorphism ("The blow-up is an isomorphism", the proof of [Kol07, Lemma 102]; [Kol07, Warning 20]).

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

The generic points of Z_{-1} are exactly the selected generic points of E^j.

theorem Hironaka.BD.ordAlongEq_Zminus1 {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) : T.I.OrdAlongEq (Zminus1 T.I m (T.E.component j)).support ↑m

For max-ord I = m, ord_{Z_{-1}} I = m ([Kol07, Definition 65, (2)]): ≥ m at the selected generic points, ≤ max-ord I everywhere.

theorem Hironaka.BD.isOrderBlowUp_Zminus1 {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) : T.IsOrderBlowUp (Zminus1 T.I m (T.E.component j)) m

For max-ord I = m, Z_{-1} is a smooth blow-up of order m of (X, I, E) ([Kol07, Definition 65]; the proof of [Kol07, Lemma 102]).

theorem Hironaka.BD.isOrderSeq_piMinusOne {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) : (piMinusOne T.I m (T.E.component j)).IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m

For max-ord I = m, the one-step sequence π_{-1} is a smooth blow-up sequence of order m starting with (X, I, E) ([Kol07, Definition 66]).