D-balanced ideals

An ideal I with m = max-ord I is D-balanced if (Dⁱ I)^m ⊂ I^(m-i) for all i < m [Kol07, 52 and Definition 83]. Locally the parameter m is explicit. Kollár's consequence "at every point it has order either m or 0" is IsDBalanced.ord_eq_zero_or_le: if ord I < m then D^(m-1) I = R ([Kol07, Lemma 74(3)]), so R = (D^(m-1) I)^m ⊂ I. The D-balanced inclusions pass to any coordinate-compatible ring map (IsDBalanced.map), in particular to the restriction R → R/⟨x₁⟩ to a coordinate hypersurface. Two examples close the file: ⟨xᵢ^m⟩ is D-balanced with respect to m, and ⟨xᵢ xⱼ⟩ is not D-balanced with respect to 2, since D ⟨xᵢ xⱼ⟩ = ⟨xᵢ, xⱼ⟩ and xᵢ² ∉ ⟨xᵢ xⱼ⟩ in K⟦X⟧ (X_sq_notMem_span_X_mul_X); their instances in ℚ⟦x₀, x₁⟧ are HironakaExamples/Balanced/PowerSeriesTwoVariables.lean.

def IsLocalRing.RegularCoords.IsDBalanced {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) (m : ℕ) : Prop

I is D-balanced with respect to m if (Dⁱ I)^m ≤ I^(m-i) for all i < m [Kol07, 52 and Definition 83].

Equations

• c.IsDBalanced I m = ∀ i < m, c.Dpow i I ^ m ≤ I ^ (m - i)

theorem IsLocalRing.RegularCoords.IsDBalanced.eq_top_of_ord_lt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} {c : RegularCoords R n} {I : Ideal R} {m : ℕ} (h : c.IsDBalanced I m) (hm : 1 ≤ m) (hord : ord I < ↑m) : I = ⊤

A D-balanced ideal with respect to m ≥ 1 of order < m is the unit ideal ("(D^(m-1) I)_p = 𝒪_p, thus I^(m-1) and I both contain a unit at p", [Kol07, Definition 83]).

theorem IsLocalRing.RegularCoords.IsDBalanced.ord_eq_zero_or_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} {c : RegularCoords R n} {I : Ideal R} {m : ℕ} (h : c.IsDBalanced I m) (hm : 1 ≤ m) : ord I = 0 ∨ ↑m ≤ ord I

"At every point it has order either m or 0" [Kol07, Definition 83], locally: ord I = 0 or m ≤ ord I.

theorem IsLocalRing.RegularCoords.IsDBalanced.ord_eq_zero_or_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} {c : RegularCoords R n} {I : Ideal R} {m : ℕ} (h : c.IsDBalanced I m) (hm : 1 ≤ m) (hle : ord I ≤ ↑m) : ord I = 0 ∨ ord I = ↑m

If moreover ord I ≤ m then ord I ∈ {0, m}.

theorem IsLocalRing.RegularCoords.IsDBalanced.le_ord_iff_one_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} {c : RegularCoords R n} {I : Ideal R} {m : ℕ} (h : c.IsDBalanced I m) (hm : 1 ≤ m) : ↑m ≤ ord I ↔ 1 ≤ ord I

Kollár's "cosupp (I, m) = cosupp I" [Kol07, Definition 83], locally: m ≤ ord I ↔ 1 ≤ ord I.

theorem IsLocalRing.RegularCoords.IsDBalanced.map {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} {c : RegularCoords R n} {R' : Type u_2} [CommRing R'] [IsRegularLocalRing R'] [Algebra ℚ R'] {n' : ℕ} (c' : RegularCoords R' n') (φ : R →+* R') (e : Fin n' → Fin n) (hφ : ∀ (j : Fin n') (f : R), (c'.pderiv j) (φ f) = φ ((c.pderiv (e j)) f)) {I : Ideal R} {m : ℕ} (h : c.IsDBalanced I m) : c'.IsDBalanced (Ideal.map φ I) m

The D-balanced inclusions pass to the image under a ring map whose target derivations are induced by the source ones (∂'ⱼ ∘ φ = φ ∘ ∂_{e j}), such as the restriction to a coordinate hypersurface R/⟨x₁⟩: the algebra behind Kollár's remark that D-balanced ideals "behave very well with respect to restriction to smooth subvarieties" [Kol07, 52].

theorem IsLocalRing.RegularCoords.isDBalanced_span_singleton_x_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) (m : ℕ) : c.IsDBalanced (Ideal.span {c.x i ^ m}) m

⟨xᵢ^m⟩ is D-balanced with respect to m, since Dⁱ ⟨xᵢ^m⟩ = ⟨xᵢ^(m-i)⟩ and ⟨xᵢ^(m-i)⟩^m = ⟨xᵢ^m⟩^(m-i).

theorem IsLocalRing.RegularCoords.not_isDBalanced_span_singleton_x_mul_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {i j : Fin n} (hij : i ≠ j) (h : c.x i ^ 2 ∉ Ideal.span {c.x i * c.x j}) : ¬c.IsDBalanced (Ideal.span {c.x i * c.x j}) 2

⟨xᵢ xⱼ⟩ is not D-balanced with respect to 2 as soon as xᵢ² ∉ ⟨xᵢ xⱼ⟩ (which holds in ℚ⟦x₁, x₂⟧: X_sq_notMem_span_X_mul_X below), since D ⟨xᵢ xⱼ⟩ = ⟨xᵢ, xⱼ⟩.

theorem IsLocalRing.X_sq_notMem_span_X_mul_X {σ : Type u_1} {K : Type u_2} [Field K] {i j : σ} (hij : i ≠ j) : MvPowerSeries.X i ^ 2 ∉ Ideal.span {MvPowerSeries.X i * MvPowerSeries.X j}

In K⟦X⟧ (any field K, i ≠ j), Xᵢ² ∉ ⟨Xᵢ Xⱼ⟩: the coefficient of Xᵢ² in a multiple of Xⱼ vanishes.