The order of a sum of powers

The second step of the proof of [Kol07, Theorem 107] ([Kol07, 111]): "the following simple observation reduces the general case to a single ideal", ord_Z J₁ ≥ s and ord_Z J₂ ≥ m iff ord_Z (J₁^m + J₂^s) ≥ ms. The order of a sum is the minimum ([Kol07, Definition 59 (4)], IsLocalRing.ord_sup of Hironaka/Algebra/Local/Order.lean at the stalk) and the order of a power is the multiple ([Kol07, Definition 59 (3)], ord_pow of Hironaka/Resolution/Algebraic/Kol07/Tuning.lean on a smooth scheme, where the stalks are regular local rings containing ℚ), so ord_x (J₁^m + J₂^s) = min (m · ord_x J₁, s · ord_x J₂) and, for m, s ≥ 1, this is ≥ ms iff both ord_x J₁ ≥ s and ord_x J₂ ≥ m. Hence cosupp(J₁^m + J₂^s, ms) = cosupp(J₁, s) ∩ cosupp(J₂, m), and the same along a centre Z (at its generic points, Kollár's ord_Z).

• stalkIdeal_sup, ord_sup_eq_min: the sum at the stalk and its order (the sum of ideal sheaves is their supremum).
• le_ord_pow_sup_pow_iff: the observation at a point; setOf_le_ord_pow_sup_pow: its cosupport form; leOrdAlong_pow_sup_pow_iff: its form along a closed set (LeOrdAlong).

Used in the second step of the proof of Theorem 107 (Hironaka/Resolution/Algebraic/Kol07/MarkedSupPow.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step2Separation.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothLoop.lean).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_sup {X : Scheme} (I J : X.IdealSheafData) (x : ↥X) : (I ⊔ J).stalkIdeal x = I.stalkIdeal x ⊔ J.stalkIdeal x

The stalk of a sum of ideal sheaves is the sum of the stalks: an identity of stalks on any scheme, with no smoothness and no structure morphism.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_sup_eq_min {X : Scheme} (I J : X.IdealSheafData) (x : ↥X) : (I ⊔ J).ord x = min (I.ord x) (J.ord x)

[Kol07, Definition 59 (4)]: the order of a sum is the minimum of the orders. ord is the order in the local ring 𝒪_{X,x}, and in any local ring the order of a sum of ideals is the minimum (IsLocalRing.ord_sup); no smoothness enters — it is the power ord_pow that needs the regular stalks.

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ord_pow_sup_pow_iff {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (J₁ J₂ : X.IdealSheafData) {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) (x : ↥X) : ↑(m * s) ≤ (J₁ ^ m ⊔ J₂ ^ s).ord x ↔ ↑s ≤ J₁.ord x ∧ ↑m ≤ J₂.ord x

Kollár's observation in the proof of Theorem 107 ([Kol07, 111]), ord_Z J₁ ≥ s and ord_Z J₂ ≥ m iff ord_Z (J₁^m + J₂^s) ≥ ms, at a point: for m, s ≥ 1, ms ≤ ord_x (J₁^m + J₂^s) iff s ≤ ord_x J₁ and m ≤ ord_x J₂ — the order of the sum is the minimum, the order of a power is the multiple ([Kol07, Definition 59 (3), (4)]), and m, s cancel in ℕ∞.

theorem AlgebraicGeometry.Scheme.IdealSheafData.setOf_le_ord_pow_sup_pow {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (J₁ J₂ : X.IdealSheafData) {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) : {x : ↥X | ↑(m * s) ≤ (J₁ ^ m ⊔ J₂ ^ s).ord x} = {x : ↥X | ↑s ≤ J₁.ord x} ∩ {x : ↥X | ↑m ≤ J₂.ord x}

The cosupport of the sum of powers at the mark ms is the intersection of the two cosupports, for m, s ≥ 1: in the use of [Kol07, 111], cosupp(N(I)^m + I^s, ms) = cosupp(N(I), s) ∩ cosupp(I, m).

theorem AlgebraicGeometry.Scheme.IdealSheafData.leOrdAlong_pow_sup_pow_iff {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (J₁ J₂ : X.IdealSheafData) (Z : TopologicalSpace.Closeds ↥X) {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) : (J₁ ^ m ⊔ J₂ ^ s).LeOrdAlong Z ↑(m * s) ↔ J₁.LeOrdAlong Z ↑s ∧ J₂.LeOrdAlong Z ↑m

Kollár's observation along a closed set Z (Kollár's ord_Z, the order at the generic points; [Kol07, 111]): ord_Z (J₁^m + J₂^s) ≥ ms iff ord_Z J₁ ≥ s and ord_Z J₂ ≥ m, for m, s ≥ 1.