D-balanced ideals and ideal sheaves

Kollár's D-balanced ideals [Kol07, Definition 83; also 52]: an ideal I with m = max-ord I is D-balanced if "(Dⁱ I)^m ⊂ I^{m−i} for all i < m", where D is the derivative ideal [Kol07, Definition 73]. Two forms of the definition, both with the mark m an explicit parameter (Kollár takes m = max-ord I; the statements that need that side condition carry it):

• Ideal.IsDBalanced k J m for an ideal J of a k-algebra A, with the intrinsic derivative ideals Ideal.derivativeIter k i J of Hironaka.Derivative (at a regular local ring with coordinates whose derivations span, this is RegularCoords.IsDBalanced of Hironaka.Local by Ideal.derivativeIter_eq_Dpow);
• AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced f I m for an ideal sheaf I on a k-scheme f : X ⟶ Spec k, with the derivative ideal sheaves derivativeIter f i I.

D-balanced ideals are the ideals whose order reduction can be pushed to a hypersurface of maximal contact [Kol07, Theorem 84]; the tuned ideal W_s(I) of Hironaka.Tuning is D-balanced [Kol07, Corollary 101], and Hironaka.Resolution.Algebraic.Balanced.Order proves the order dichotomy of D-balanced ideal sheaves.

def Ideal.IsDBalanced (k : Type u_1) {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (m : ℕ) : Prop

Kollár's D-balanced ideals [Kol07, Definition 83; 52], ring form: J is D-balanced with respect to m if (Dⁱ J)^m ≤ J^{m−i} for every i < m, with D the intrinsic derivative ideal Ideal.derivativeIter.

Equations

• Ideal.IsDBalanced k J m = ∀ i < m, Ideal.derivativeIter k i J ^ m ≤ J ^ (m - i)

theorem Ideal.isDBalanced_iff {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (m : ℕ) : IsDBalanced k J m ↔ ∀ i < m, derivativeIter k i J ^ m ≤ J ^ (m - i)

theorem Ideal.isDBalanced_top {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (m : ℕ) : IsDBalanced k ⊤ m

The unit ideal is D-balanced with respect to every mark.

theorem Ideal.isDBalanced_zero {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) : IsDBalanced k J 0

Every ideal is D-balanced with respect to the mark 0 (there is no i < 0).

def AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (m : ℕ) : Prop

Kollár's D-balanced ideals [Kol07, Definition 83; 52], sheaf form: the ideal sheaf I on the k-scheme f : X ⟶ Spec k is D-balanced with respect to m if (Dⁱ I)^m ≤ I^{m−i} for every i < m, with D the derivative ideal sheaf derivativeIter f. Kollár's side condition m = max-ord I is carried by the statements that use it.

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced f I m = ∀ i < m, AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f i I ^ m ≤ I ^ (m - i)

theorem AlgebraicGeometry.Scheme.IdealSheafData.isDBalanced_iff {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (m : ℕ) : IsDBalanced f I m ↔ ∀ i < m, derivativeIter f i I ^ m ≤ I ^ (m - i)

theorem AlgebraicGeometry.Scheme.IdealSheafData.isDBalanced_top {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (m : ℕ) : IsDBalanced f ⊤ m

The unit ideal sheaf is D-balanced with respect to every mark.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isDBalanced_zero {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) : IsDBalanced f I 0

Every ideal sheaf is D-balanced with respect to the mark 0.