The order of a sum of powers of ideal sheaves

Step 2 of the proof of [Kol07, Theorem 107] (item 111) reduces order reduction for the pair of marked ideals (N(I), s), (I, m) to order reduction for the single ideal N(I)^m + I^s at the mark ms, by the observation that a centre Z satisfies ord_Z N(I) ≥ s and ord_Z I ≥ m if and only if ord_Z (N(I)^m + I^s) ≥ ms. This file proves the pointwise form of that equivalence on an analytic manifold: the order of a sum of ideal sheaves is the minimum of the orders and the order of a power is the multiple of the order (the cosupport identities cosupp(I₁ + I₂, m) = cosupp(I₁, m) ∩ cosupp(I₂, m) and cosupp(I, m) = cosupp(I^c, mc) of [Kol07, Definition 59 (4), (3)], read on orders; IdealSheaf.ord_pow), and the factors m, s cancel in ℕ∞. The sum of ideal sheaves is the join of the stalks.

theorem Manifold.IdealSheaf.ord_add_eq_min {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (I J : IdealSheaf (structureSheaf 𝕜 E M)) (x : M) : (I + J).ord x = min (I.ord x) (J.ord x)

The order of a sum of ideal sheaves at a point is the minimum of the two orders ([Kol07, Definition 59 (4)], read on orders): the stalk of the sum is the join of the stalks, and the order of a join of ideals in a local ring is the minimum (IsLocalRing.ord_sup).

theorem Manifold.IdealSheaf.le_ord_pow_add_pow_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J₁ J₂ : IdealSheaf (structureSheaf 𝕜 E M)) {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) (x : M) : ↑(m * s) ≤ (J₁ ^ m + J₂ ^ s).ord x ↔ ↑s ≤ J₁.ord x ∧ ↑m ≤ J₂.ord x

For m, s ≥ 1, the order of J₁^m + J₂^s at x is at least ms if and only if the order of J₁ is at least s and the order of J₂ is at least m: the observation of [Kol07, 111, Step 2] that reduces the pair (N(I), s), (I, m) to the single ideal N(I)^m + I^s, here at a point. The order of the sum is the minimum, the order of a power is the multiple, and the factors cancel in ℕ∞.