The predicates of CP3: the classification of the centres, universal over the coordinates

The statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) classifies the centres of a run of BMO_1 on a protected state. This module states it in a form universal over the chain-coordinate systems: chain coordinates without the tracked subvariety (ChainCoordsFree); the classification of one centre at one of its points — in EVERY chain-coordinate system at the point in which the current ideal has the K-shape the centre is an admissible stratum, and in every system in which it has the un-isolated form it is an admissible stratum, a terminal-normal stratum, or the absorption (f) (CenterClassifiedAt); its form along a run (CP3For) and along the tower of order reductions (CP3BOAt, CP3BMOAt, CP3BOFor); and the bridges to the existential predicates of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAdmissibleStratum (AdmissibleChainStratumKAt, AdmissibleChainStratumAt, TerminalNormalStratumAt), which are the universal ones instantiated at the coordinates that the persistence of the chain form provides. The coordinates are those of [Kol07, Definition 24]. The predicates are proved along the tower in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1 to Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower and consumed by CP5 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5).

def Hironaka.Resolution.ChainCoordsFree {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (p : ↥X) {n : ℕ} (z : Fin n → ↑(X.presheaf.stalk p)) (c : { j : E.ι // p ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) : Prop

Chain coordinates at p for the family E WITHOUT the tracked subvariety (the coordinates of [Kol07, Definition 24] at p) — ChainCoords minus its last clause: a regular system of parameters z, the members through p given by z (c j), the chain coordinates z ∘ σ off the members, the exponents supported on the members' coordinates.

Equations

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

theorem Hironaka.Resolution.chainCoords_iff_free {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {Γ : X.IdealSheafData} {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} : ChainCoords E Γ p z c σ a ↔ ChainCoordsFree E p z c σ a ∧ Γ.stalkIdeal p = Ideal.span (Set.range (z ∘ σ))

ChainCoords is ChainCoordsFree together with the tracked subvariety's stalk being the chain's span.

theorem Hironaka.Resolution.admissibleChainStratumKAt_of_stratumIn {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {K Γ Z : X.IdealSheafData} {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} {b : Fin n → ℕ} (hc : ChainCoords E Γ p z c σ a) (hb : ∀ (k : Fin n), b k ≠ 0 → k ∈ Set.range c) (hK : K.stalkIdeal p = Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (h : StratumIn z (Set.range c) σ a b (Z.stalkIdeal p)) : AdmissibleChainStratumKAt E K Γ Z p

Admissibility in given K-shape coordinates gives the existential predicate AdmissibleChainStratumKAt.

theorem Hironaka.Resolution.admissibleChainStratumAt_of_stratumIn {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {I Γ Z : X.IdealSheafData} {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} {b : Fin n → ℕ} (hc : ChainCoords E Γ p z c σ a) (hb : ∀ (k : Fin n), b k ≠ 0 → k ∈ Set.range c) (hI : I.stalkIdeal p = Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (h : StratumIn z (Set.range c) σ a b (Z.stalkIdeal p)) : AdmissibleChainStratumAt E I Γ Z p

The same for the un-isolated form.

theorem Hironaka.Resolution.terminalNormalStratumAt_of_terminalIn {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {I Γ Z : X.IdealSheafData} {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} {b : Fin n → ℕ} (hc : ChainCoords E Γ p z c σ a) (hb : ∀ (k : Fin n), b k ≠ 0 → k ∈ Set.range c) (hI : I.stalkIdeal p = Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (h : TerminalIn z (Set.range c) σ (Z.stalkIdeal p)) : TerminalNormalStratumAt E I Γ Z p

A terminal-normal stratum in given coordinates gives TerminalNormalStratumAt.

def Hironaka.Resolution.CenterClassifiedAt {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (K Z : X.IdealSheafData) (q : ↥X) : Prop

CP3's classification at a point, universal over the coordinates: for the current ideal K, the boundary E and a centre Z at a point q ∈ Z, in EVERY chain-coordinate system at q in which K_q has the K-shape, Z_q is an admissible stratum in those coordinates; in every system in which it has the un-isolated form, Z_q is an admissible stratum, a terminal-normal stratum, or the absorption (f).

Equations

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

def Hironaka.Resolution.CP3For {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) : Prop

CP3 along a run: every centre of S (for the input (I, E) at mark 1) is classified at each of its points, for the mark-1 transforms and the total transform of the boundary at its stage.

Equations

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

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

CP3 along the stage-n order reduction BO_{n,1} of the tower ([Kol07, 70]) on every triple of its class.

Equations

• Hironaka.Resolution.CP3BOAt k n = ∀ (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n 1 T), Hironaka.Resolution.CP3For (Hironaka.Resolution.boRun k n T hT) T.I T.E

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

CP3 along the stage-n marked order reduction BMO_{n,1} on every marked triple of its class.

Equations

• Hironaka.Resolution.CP3BMOAt k n = ∀ (T : Hironaka.MarkedTriple k) (hT : Hironaka.MarkedTriple.BMOClass n 1 T), Hironaka.Resolution.CP3For (Hironaka.Resolution.bmoRun k n T hT) T.I T.E

def Hironaka.Resolution.CP3BOFor (k : Type u) [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) : Prop

CP3 along the value of the order-1 reduction bo 1 on every triple of class BOClass n 1 (the hypothesis for the reduction through Step 1).

Equations

• Hironaka.Resolution.CP3BOFor k bo = ∀ (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n 1 T), Hironaka.Resolution.CP3For (((bo 1).functor k).seq T hT) T.I T.E