One blow-up along an admissible chain stratum (CP4)

The statement CP4 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): blowing up an admissible chain stratum Z (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAdmissibleStratum) of a protected component Γ keeps the strict transform Γ̃ smooth and with simple normal crossings with the total transform of the boundary, and transports the K-shape of K (and the un-isolated form of I, also along a terminal-normal stratum) to the mark-1 transforms along Γ̃ (chainRelativeKAt_strictTransform, chainRelativeAt_strictTransform).

The proof. Everything is pointwise at a point q of the blow-up on Γ̃, over p = π(q) ∈ Γ. Off the exceptional divisor π^* is an isomorphism of stalks and the forms transport verbatim (chainRelativeKAt_totalTransform_of_notMem, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4NewCoords). On the exceptional divisor p ∈ Z ∩ Γ and admissibility gives chain coordinates z at p with Z_p = (f_i : i < l) + (e_j : j ∈ s); the chart datum of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Chart (the pivot e_{j₀}, the induced coordinates w, the new parameters z') computes Γ̃_q = (w ∘ σ) and the members' strict transforms, and — with the ε-order bookkeeping of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Algebra under the admissibility condition (★) — the mark-1 transforms as chain forms in the new parameters. The local rings of the blow-up are regular by the chart theorem in its pointwise form (exists_totalTransformData_of_mem_support_of_specializes: the snc data are needed only at the points of Z below p, all in Z ∩ Γ). Smoothness of Γ̃ over k is regularity of its local rings — 𝒪_{B,q}/Γ̃_q with Γ̃_q generated by part of a regular system of parameters (isRegularLocalRing_stalk_subscheme) — through Scheme.smooth_iff_isRegular.

The chart is that of [Kol07, Definition 60]. CP4 is not in the literature; it is consumed by the loop invariant CP5 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5).

snc data with the stratum as a coordinate subspace

def Hironaka.Resolution.SncDataWith {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) (x : ↥X) : Prop

Kollár's snc data at x with Z a coordinate subspace ([Kol07, Definition 24]) — the pointwise hypothesis of the chart theorem.

Equations

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

theorem Hironaka.Resolution.sncDataWith_of_admissibleK {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {K : X.IdealSheafData} {x : ↥X} (h : AdmissibleChainStratumKAt E K Γ Z x) : SncDataWith E Z x

An admissible chain stratum (K-form) carries snc data with Z a coordinate subspace.

theorem Hironaka.Resolution.sncDataWith_of_admissibleAt {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {I : X.IdealSheafData} {x : ↥X} (h : AdmissibleChainStratumAt E I Γ Z x) : SncDataWith E Z x

An admissible chain stratum (un-isolated form) carries snc data with Z a coordinate subspace.

theorem Hironaka.Resolution.span_range_comp_sup_eq {R : Type u_1} [CommRing R] {n r : ℕ} (z : Fin n → R) (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) : Ideal.span (Set.range (z ∘ σ)) ⊔ Ideal.span (z '' ↑s) = Ideal.span (z '' ↑(stratumCoords σ s (r + 1)))

The chain and the whole coordinate range agree at level r + 1.

theorem Hironaka.Resolution.sncDataWith_of_terminalNormal {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {I : X.IdealSheafData} {x : ↥X} (h : TerminalNormalStratumAt E I Γ Z x) : SncDataWith E Z x

A terminal-normal stratum carries snc data with Z a coordinate subspace.

theorem Hironaka.Resolution.isRegularLocalRing_stalk_blowUp_of_sncDataWith {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {q : ↥Z.blowUp} (hq : q ∈ (Z.comap Z.blowUpπ).support) (hΓ : Z.blowUpπ q ∈ Γ.support) (hdata : ∀ x ∈ Z.support, x ∈ Γ.support → SncDataWith E Z x) : IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)

The regularity of the blow-up's local rings, pointwise: at a point q of the exceptional divisor over a point of Γ, when every point of Z ∩ Γ carries snc data with Z.

The ε-order conditions from (★)

def Hironaka.Resolution.δAdm {r : ℕ} (l : ℕ) (i : Fin (r + 1)) : ℕ

The ε-order [i < l] of the i-th chain equation along the stratum (f_i : i < l) + (e_s).

Equations

• Hironaka.Resolution.δAdm l i = if ↑i < l then 1 else 0

theorem Hironaka.Resolution.δAdm_eq {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (hσ : Function.Injective σ) (hs : ∀ (i : Fin (r + 1)), σ i ∉ s) (l : ℕ) (i : Fin (r + 1)) : (if σ i ∈ stratumCoords σ s l then 1 else 0) = δAdm l i

theorem Hironaka.Resolution.one_le_sum_of_exists {n : ℕ} (s : Finset (Fin n)) {c : Fin n → ℕ} (h : ∃ k ∈ s, c k ≠ 0) : 1 ≤ ∑ k ∈ s, c k

A positive entry makes the total exponent positive.

theorem Hironaka.Resolution.one_le_epsOrderC_K {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) (hb : ∀ (k : Fin n), b k ≠ 0 → k ∉ Set.range σ) (l : ℕ) (hl : l ≤ r) (h₁ : l = 0 → ∃ k ∈ s, b k ≠ 0) : 1 ≤ epsOrderC (stratumCoords σ s l) a b (Function.update (δAdm l) (Fin.last r) 0) 0

(★) at level 0: the K-form's first ε-order is positive.

theorem Hironaka.Resolution.one_le_epsOrderC_I {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) (hb : ∀ (k : Fin n), b k ≠ 0 → k ∉ Set.range σ) (l : ℕ) (h₁ : l = 0 → ∃ k ∈ s, b k ≠ 0) : 1 ≤ epsOrderC (stratumCoords σ s l) a b (δAdm l) 0

(★) at level 0: the un-isolated form's first ε-order is positive.

theorem Hironaka.Resolution.epsOrderC_I_mono {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∉ Set.range σ) (l : ℕ) (hl : l ≤ r) (h₂ : 0 < l → ∃ k ∈ s, a ⟨l - 1, ⋯⟩ k ≠ 0) (i : Fin r) : epsOrderC (stratumCoords σ s l) a b (δAdm l) i.castSucc ≤ epsOrderC (stratumCoords σ s l) a b (δAdm l) i.succ

(★) at the stratum's level: the un-isolated form's ε-orders are non-decreasing.

theorem Hironaka.Resolution.epsOrderC_K_mono {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) (ha : ∀ (i : Fin (r + 1)) (k : Fin n), a i k ≠ 0 → k ∉ Set.range σ) (l : ℕ) (hl : l ≤ r) (h₂ : 0 < l → ∃ k ∈ s, a ⟨l - 1, ⋯⟩ k ≠ 0) (i : Fin r) : epsOrderC (stratumCoords σ s l) a b (Function.update (δAdm l) (Fin.last r) 0) i.castSucc ≤ epsOrderC (stratumCoords σ s l) a b (Function.update (δAdm l) (Fin.last r) 0) i.succ

(★) at the stratum's level: the K-form's ε-orders are non-decreasing (the last generator carries no equation).

theorem Hironaka.Resolution.δ_terminal_eq {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (hσ : Function.Injective σ) (hs : ∀ (i : Fin (r + 1)), σ i ∉ s) (i : Fin (r + 1)) : (if σ i ∈ stratumCoords σ s (r + 1) then 1 else 0) = 1

Along a terminal-normal stratum every chain equation is an equation of the centre.

theorem Hironaka.Resolution.one_le_epsOrderC_terminal {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) : 1 ≤ epsOrderC (stratumCoords σ s (r + 1)) a b (fun (x : Fin (r + 1)) => 1) 0

The un-isolated form's ε-orders along a terminal-normal stratum are positive and non-decreasing without any exponent condition.

theorem Hironaka.Resolution.epsOrderC_terminal_mono {n r : ℕ} (σ : Fin (r + 1) → Fin n) (s : Finset (Fin n)) (a : Fin (r + 1) → Fin n → ℕ) (b : Fin n → ℕ) (i : Fin r) : epsOrderC (stratumCoords σ s (r + 1)) a b (fun (x : Fin (r + 1)) => 1) i.castSucc ≤ epsOrderC (stratumCoords σ s (r + 1)) a b (fun (x : Fin (r + 1)) => 1) i.succ

def Hironaka.Resolution.Dexp {r : ℕ} (Efun : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : ℕ

The exponent increments E_{i+1} − E_i of a sequence of ε-orders (0 at the last index).

Equations

• Hironaka.Resolution.Dexp Efun i = if h : ↑i < r then Efun ⟨↑i + 1, ⋯⟩ - Efun i else 0

theorem Hironaka.Resolution.Dexp_castSucc {r : ℕ} (Efun : Fin (r + 1) → ℕ) (i : Fin r) : Dexp Efun i.castSucc = Efun i.succ - Efun i.castSucc

The pointwise transforms on the exceptional divisor

theorem Hironaka.Resolution.σ_notMem_of_subset_range {n r : ℕ} {σ : Fin (r + 1) → Fin n} {s : Finset (Fin n)} {ι : Type u_1} {c : ι → Fin n} (hσc : ∀ (i : Fin (r + 1)) (j : ι), σ i ≠ c j) (hs : ↑s ⊆ Set.range c) (i : Fin (r + 1)) : σ i ∉ s

The chain avoids s when s consists of members' coordinates.

theorem Hironaka.Resolution.notMem_range_of_ne_zero {n r : ℕ} {σ : Fin (r + 1) → Fin n} {ι : Type u_1} {c : ι → Fin n} (hσc : ∀ (i : Fin (r + 1)) (j : ι), σ i ≠ c j) {cc : Fin n → ℕ} (hcc : ∀ (k : Fin n), cc k ≠ 0 → k ∈ Set.range c) (k : Fin n) (hk : cc k ≠ 0) : k ∉ Set.range σ

Exponents supported on members' coordinates vanish on the chain.

theorem Hironaka.Resolution.chainRelativeKAt_of_mem_support {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {q : ↥Z.blowUp} (K : X.IdealSheafData) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hqΓ : q ∈ (Γ.strictTransform Z).support) (h : AdmissibleChainStratumKAt E K Γ Z (Z.blowUpπ q)) : ChainRelativeKAt (E.totalTransform Z) (K.markedTransform Z 1) (Γ.strictTransform Z) q ∧ ∃ (m : ℕ) (z' : Fin m → ↑(Z.blowUp.presheaf.stalk q)), (E.totalTransform Z).IsSncAt q z' ∧ ∃ (t : Finset (Fin m)), (Γ.strictTransform Z).stalkIdeal q = Ideal.span (z' '' ↑t)

CP4 for the K-shape at a point of the exceptional divisor: the K-shape transports, and Γ̃ has snc data with the total transform at q; the stalk is regular.

theorem Hironaka.Resolution.chainRelativeAt_of_mem_support_of_admissible {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {q : ↥Z.blowUp} (I : X.IdealSheafData) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hqΓ : q ∈ (Γ.strictTransform Z).support) (h : AdmissibleChainStratumAt E I Γ Z (Z.blowUpπ q)) : ChainRelativeAt (E.totalTransform Z) (I.markedTransform Z 1) (Γ.strictTransform Z) q

CP4 for the un-isolated form at a point of the exceptional divisor, admissible stratum.

theorem Hironaka.Resolution.chainRelativeAt_of_mem_support_of_terminal {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (Γ Z : X.IdealSheafData) {q : ↥Z.blowUp} (I : X.IdealSheafData) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hqΓ : q ∈ (Γ.strictTransform Z).support) (h : TerminalNormalStratumAt E I Γ Z (Z.blowUpπ q)) : ChainRelativeAt (E.totalTransform Z) (I.markedTransform Z 1) (Γ.strictTransform Z) q

CP4 for the un-isolated form at a point of the exceptional divisor, terminal-normal stratum.

The statements

theorem Hironaka.Resolution.mem_inf_support {X : AlgebraicGeometry.Scheme} {Z Γ : X.IdealSheafData} {p : ↥X} (hZ : p ∈ Z.support) (hΓ : p ∈ Γ.support) : p ∈ Z.support ⊓ Γ.support

Membership in the meet of two supports.

theorem Hironaka.Resolution.cp4K_pointwise {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (K Γ Z : X.IdealSheafData) (hΓ : E.HasSncWith Γ) (hK : ∀ p ∈ Γ.support, ChainRelativeKAt E K Γ p) (hZ : ∀ p ∈ Z.support ⊓ Γ.support, AdmissibleChainStratumKAt E K Γ Z p) (q : ↥Z.blowUp) (hqΓ : q ∈ (Γ.strictTransform Z).support) : IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q) ∧ ChainRelativeKAt (E.totalTransform Z) (K.markedTransform Z 1) (Γ.strictTransform Z) q ∧ ∃ (m : ℕ) (z' : Fin m → ↑(Z.blowUp.presheaf.stalk q)), (E.totalTransform Z).IsSncAt q z' ∧ ∃ (t : Finset (Fin m)), (Γ.strictTransform Z).stalkIdeal q = Ideal.span (z' '' ↑t)

The pointwise content of CP4-K at every point of Γ̃, with the regularity of the stalk.

theorem Hironaka.Resolution.chainRelativeKAt_strictTransform {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (K Γ Z : X.IdealSheafData) (hE : E.IsSnc) (hΓ : E.HasSncWith Γ) (hsm : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Γ.subschemeι f)) (hK : ∀ p ∈ Γ.support, ChainRelativeKAt E K Γ p) (hZ : ∀ p ∈ Z.support ⊓ Γ.support, AdmissibleChainStratumKAt E K Γ Z p) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (Γ.strictTransform Z).subschemeι (CategoryTheory.CategoryStruct.comp Z.blowUpπ f)) ∧ (E.totalTransform Z).HasSncWith (Γ.strictTransform Z) ∧ ∀ q ∈ (Γ.strictTransform Z).support, ChainRelativeKAt (E.totalTransform Z) (K.markedTransform Z 1) (Γ.strictTransform Z) q

CP4 for the K-shape: blowing up an admissible chain stratum Z — admissibility (★) at every point of Z ∩ Γ — keeps the protected component's strict transform smooth over k and snc with the total transform of the boundary, and transports the K-shape of K to the mark-1 transform along Γ̃.

theorem Hironaka.Resolution.chainRelativeAt_strictTransform {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (I Γ Z : X.IdealSheafData) (hE : E.IsSnc) (hΓ : E.HasSncWith Γ) (hI : ∀ p ∈ Γ.support, ChainRelativeAt E I Γ p) (hZ : ∀ p ∈ Z.support ⊓ Γ.support, AdmissibleChainStratumAt E I Γ Z p ∨ TerminalNormalStratumAt E I Γ Z p) (q : ↥Z.blowUp) : q ∈ (Γ.strictTransform Z).support → ChainRelativeAt (E.totalTransform Z) (I.markedTransform Z 1) (Γ.strictTransform Z) q

CP4 for the un-isolated form: the chain-relative form of I is transported along the blow-up of an admissible chain stratum (one unit of exponent consumed at the stratum's level) or of a terminal-normal stratum (no unit consumed) — one statement, two transform rules inside.