D-balanced ideal sheaves: order m or 0, cosupport, restriction, going up

The remarks following [Kol07, Definition 83]: a D-balanced I has, at every point, "order either m or 0" — if ord_p I < m then (D^{m−1} I)_p = 𝒪_{p,X}, so I^{m−1} and I contain a unit at p — hence cosupp(I, m) = cosupp I and the maximal order commutes with restrictions; and a smooth blow-up of order ≥ m for I|_S "corresponds to a smooth blow-up of order ≥ m for I".

• The order dichotomy (IsDBalanced.ord_eq_zero_or_le, ord_eq_zero_or_eq) is Kollár's argument: [Kol07, Lemma 74 (3)] at the stalk (le_ord_iff_le_ord_derivativeIter) turns ord_x I < m into (D^{m−1} I)_x = 𝒪_x, and the D-balanced inclusion (D^{m−1} I)^m ≤ I makes I_x the unit ideal.
• cosupp(I, m) = cosupp I (cosupp_eq_support) follows, and so does the restriction statement (cosupp_restrict): the order never drops under the local homomorphism of stalks 𝒪_{X, ι s} → 𝒪_{S, s} (ord_le_ord_map, stalkIdeal_comap), and where ord_{ι s} I = 0 the stalk is the unit ideal on both sides.
• The going-up reformulation (isOrderBlowUp_of_restrict): a generic point η of the centre Z ⊆ S lies in S; the order of I|_S along Z is at least m at every point of Z (leOrdAlong_iff_forall_mem on the smooth S), so ord_η I ≥ m by cosupp_restrict, and ord_η I ≤ max-ord I = m.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_eq_top_of_ord_eq_zero {X : Scheme} {I : X.IdealSheafData} {x : ↥X} (h : I.ord x = 0) : I.stalkIdeal x = ⊤

A stalk of order 0 is the unit ideal (ord_eq_zero_iff at the stalk).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_le_ord_comap {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (g : Y ⟶ X) (y : ↥Y) : I.ord (g y) ≤ (I.comap g).ord y

The order of I at g y is at most the order of the pull-back g⁻¹ I at y: the stalk map is a local homomorphism (ord_le_ord_map; the inequality ord_p I ≤ ord_p (I|_S) noted before [Kol07, Definition 83]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced.ord_eq_zero_or_le {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {m : ℕ} (h : IsDBalanced f I m) (x : ↥X) : I.ord x = 0 ∨ ↑m ≤ I.ord x

A D-balanced ideal sheaf has order 0 or at least m at every point (the remark after [Kol07, Definition 83]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced.ord_eq_zero_or_eq {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {m : ℕ} (h : IsDBalanced f I m) (hmax : I.maxOrd = ↑m) (x : ↥X) : I.ord x = 0 ∨ I.ord x = ↑m

With m = max-ord I, a D-balanced ideal sheaf has order 0 or m at every point (the remark after [Kol07, Definition 83]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced.cosupp_eq_support {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {m : ℕ} (h : IsDBalanced f I m) (hm : 1 ≤ m) : {x : ↥X | ↑m ≤ I.ord x} = ↑I.support

"cosupp(I, m) = cosupp I" for a D-balanced ideal sheaf (the remark after [Kol07, Definition 83]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced.cosupp_restrict {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {m : ℕ} (h : IsDBalanced f I m) (S : X.IdealSheafData) (s : ↥S.subscheme) : ↑m ≤ (I.comap S.subschemeι).ord s ↔ ↑m ≤ I.ord (S.subschemeι s)

"The maximal order commutes with restrictions" (the remark after [Kol07, Definition 83]): cosupp(I|_S, m) = cosupp(I, m) ∩ S, pointwise on S.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced.isOrderBlowUp_of_restrict {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {m : ℕ} (h : IsDBalanced f I m) (hmax : I.maxOrd = ↑m) (S : X.IdealSheafData) [SmoothOfRelativeDimension (n - 1) (CategoryTheory.CategoryStruct.comp S.subschemeι f)] (Z : X.IdealSheafData) (hZS : S ≤ Z) (hZ : (I.comap S.subschemeι).LeOrdAlong (Z.comap S.subschemeι).support ↑m) : I.OrdAlongEq Z.support ↑m

The going-up remark after [Kol07, Definition 83]: for I D-balanced with m = max-ord I, S a smooth hypersurface and Z ⊆ S a centre with ord_Z (I|_S) ≥ m, ord_Z I = m.