The local cosupport lemma in stalk form

[Kol07, Lemma 74 (3)], cosupp(I, m) = cosupp(Dʳ(I), m − r) for r < m, "char. 0 only!", and [Wlo05, Lemma 2.6.2], supp(I, μ) = V(D^{μ−1}(I)) is closed: in a regular local ℚ-algebra R with coordinates c (RegularCoords), for r < m,

I ⊆ 𝔪ᵐ ⟺ Dʳ(I) ⊆ 𝔪^(m−r), in particular I ⊆ 𝔪ᵐ ⟺ D^{m−1}(I) ⊆ 𝔪 ⟺ D^{m−1}(I) ≠ R,

equivalently ord I ≥ m ⟺ D^{m−1}(I) ⊆ 𝔪. This is le_ord_iff_le_ord_Dpow of Hironaka/Algebra/Local/Derivative.lean (proved there through the Euler identity) read through le_ord_iff of Hironaka/Algebra/Local/Order.lean; the module restates it in the forms the sheaf-level cosupport transfer consumes at a stalk 𝒪_{X,x} (Hironaka/Scheme/IdealSheaf/Derivative/Cosupport.lean): the derivative ideal sheaf has, at a stalk, Kollár's image ideal over all derivations, which contains the coordinate derivative c.D (giving ⟹ from the lemma here) and whose members lower the 𝔪-adic order by at most one (derivation_mem_pow, giving ⟸ without coordinates).

Used by Hironaka/Algebra/Derivative/Basic.lean and Hironaka/Scheme/IdealSheaf/Derivative/Cosupport.lean.

Any derivation lowers the adic order by at most one

theorem IsLocalRing.derivation_mem_pow {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) (J : Ideal A) (N : ℕ) {f : A} (hf : f ∈ J ^ (N + 1)) : δ f ∈ J ^ N

Leibniz: a derivation maps J^(N+1) into J^N for every ideal J (the coordinate-free half of the cosupport lemma).

theorem IsLocalRing.span_image_derivation_pow_le {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) (J : Ideal A) (N : ℕ) : Ideal.span (⇑δ '' ↑(J ^ (N + 1))) ≤ J ^ N

The ideal generated by the derivatives of J^(N+1) lies in J^N.

The cosupport lemma at a regular local ring with coordinates

theorem IsLocalRing.RegularCoords.le_maximalIdeal_pow_iff_Dpow_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) {r m : ℕ} (h : r < m) : I ≤ maximalIdeal R ^ m ↔ c.Dpow r I ≤ maximalIdeal R ^ (m - r)

[Kol07, Lemma 74 (3)]; [Wlo05, Lemma 2.6.2]: for r < m, I ⊆ 𝔪ᵐ ⟺ Dʳ(I) ⊆ 𝔪^(m−r); le_ord_iff_le_ord_Dpow in ideal form.

theorem IsLocalRing.RegularCoords.le_maximalIdeal_pow_iff_Dpow_le_maximalIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) {m : ℕ} (hm : 1 ≤ m) : I ≤ maximalIdeal R ^ m ↔ c.Dpow (m - 1) I ≤ maximalIdeal R

I ⊆ 𝔪ᵐ ⟺ D^{m−1}(I) ⊆ 𝔪 for m ≥ 1.

theorem IsLocalRing.le_maximalIdeal_iff_ne_top {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {J : Ideal R} : J ≤ maximalIdeal R ↔ J ≠ ⊤

An ideal of a local ring is proper exactly when it lies in the maximal ideal.

theorem IsLocalRing.RegularCoords.le_maximalIdeal_pow_iff_Dpow_ne_top {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) {m : ℕ} (hm : 1 ≤ m) : I ≤ maximalIdeal R ^ m ↔ c.Dpow (m - 1) I ≠ ⊤

I ⊆ 𝔪ᵐ ⟺ D^{m−1}(I) ≠ R for m ≥ 1 ([Wlo05, Lemma 2.6.2], supp(I, μ) = V(D^{μ−1}(I))).

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

ord I ≥ m ⟺ D^{m−1}(I) ⊆ 𝔪 for m ≥ 1.