Logarithmic derivations and logarithmic derivative ideals

[Kol07, 87]: for a smooth variety X and a smooth hypersurface S ⊂ X, the sheaf Der_X(−log S) ⊂ Der_X of logarithmic derivations along S is "the largest subsheaf that maps 𝒪_X(−S) into itself by derivations", and for an ideal sheaf I, D(−log S)(I) := im[Der_X(−log S) × I → 𝒪_X], D^{r+1}(−log S)(I) := D(−log S)(D^r(−log S)(I)). Bierstone and Milman use the same ideals D_E(I) for a normal-crossings divisor E [BM08, §3.2].

• Ring level. A derivation δ preserves an ideal J when δ(J) ⊆ J (Derivation.PreservesIdeal; the derivations preserving J form the A-submodule Derivation.preserving k J of Derivation k A A). The logarithmic derivative ideal Ideal.logDerivative k J I is generated by I and the δ f, δ a k-derivation preserving J, f ∈ I: Ideal.derivative of Hironaka/Algebra/Derivative/Basic.lean with the derivations restricted to those preserving J; Ideal.logDerivativeIter iterates. I ⊆ D(−log J)(I) ⊆ D(I), and D(−log ⊤)(I) = D(I): away from S every derivation is logarithmic.
• Sheaf level. IdealSheafData.logDerivative f S I is packaged, like derivative of Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean, through Mathlib's ofIdeals from the family U ↦ D(−log S(U))(I(U)) for the k-algebra structures f.sectionsAlgebra U; logDerivativeIter iterates. The compatibility of the family with restriction to basic opens is Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicLocalization.lean, the identification of the stalks Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean; Kollár's three properties (87.1)–(87.3) are Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicQuotient.lean, Hironaka/Algebra/Local/LogDeriv.lean (in coordinates) and Hironaka/Scheme/BlowUpSequence/TransformLogDerivative.lean.

Used in coordinates (Hironaka/Algebra/Local/LogDerivCoords.lean), for the blow-up chart (Hironaka/Algebra/Local/BlowUpLiftLog.lean, Hironaka/Algebra/Local/ChartLogDerivations.lean, Hironaka/Algebra/Local/TransformLogDerivMap.lean), for Theorem 88 and Corollary 89 on schemes (Hironaka/Scheme/BlowUpSequence/Theorem88Basic.lean, Hironaka/Resolution/Algebraic/Kol07/Corollary89.lean) and on manifolds (Hironaka/Manifold/IdealSheaf/LogDeriv.lean).

def Derivation.PreservesIdeal {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) (J : Ideal A) : Prop

A derivation preserves the ideal J (Kollár's "maps 𝒪_X(−S) into itself by derivations", [Kol07, 87]).

Equations

• δ.PreservesIdeal J = ∀ a ∈ J, δ a ∈ J

theorem Derivation.preservesIdeal_top {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) : δ.PreservesIdeal ⊤

theorem Derivation.preservesIdeal_span_singleton_iff {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) (s : A) : δ.PreservesIdeal (Ideal.span {s}) ↔ δ s ∈ Ideal.span {s}

A derivation preserves a principal ideal (s) iff δ s ∈ (s) (Leibniz).

def Derivation.preserving {A : Type u_2} [CommRing A] (k : Type u_3) [CommRing k] [Algebra k A] (J : Ideal A) : Submodule A (Derivation k A A)

The derivations preserving J, as an A-submodule of the derivations: Kollár's Der_X(−log S) at the level of a ring.

Equations

• Derivation.preserving k J = { carrier := {δ : Derivation k A A | δ.PreservesIdeal J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem Derivation.mem_preserving {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J : Ideal A} {δ : Derivation k A A} : δ ∈ preserving k J ↔ δ.PreservesIdeal J

def Ideal.logDerivative (k : Type u_1) {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J I : Ideal A) : Ideal A

The logarithmic derivative ideal D(−log J)(I) of [Kol07, 87], generated by I and the δ f for the k-derivations δ preserving J and f ∈ I.

Equations

• Ideal.logDerivative k J I = I ⊔ ⨆ (δ : Derivation k A A), ⨆ (_ : δ.PreservesIdeal J), Ideal.span (⇑δ '' ↑I)

def Ideal.logDerivativeIter (k : Type u_1) {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (r : ℕ) (I : Ideal A) : Ideal A

D^r(−log J)(I) ([Kol07, 87]).

Equations

• Ideal.logDerivativeIter k J r I = (Ideal.logDerivative k J)^[r] I

theorem Ideal.le_logDerivative {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J I : Ideal A) : I ≤ logDerivative k J I

theorem Ideal.derivation_apply_mem_logDerivative {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J : Ideal A} {δ : Derivation k A A} (hδ : δ.PreservesIdeal J) {I : Ideal A} {f : A} (hf : f ∈ I) : δ f ∈ logDerivative k J I

theorem Ideal.logDerivative_le_iff {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J I K : Ideal A} : logDerivative k J I ≤ K ↔ I ≤ K ∧ ∀ (δ : Derivation k A A), δ.PreservesIdeal J → ∀ f ∈ I, δ f ∈ K

theorem Ideal.logDerivative_mono {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J I I' : Ideal A} (h : I ≤ I') : logDerivative k J I ≤ logDerivative k J I'

theorem Ideal.logDerivative_le_derivative {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J I : Ideal A) : logDerivative k J I ≤ derivative k I

D(−log J)(I) ⊆ D(I).

theorem Ideal.logDerivative_top {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (I : Ideal A) : logDerivative k ⊤ I = derivative k I

Away from S (the unit ideal) every derivation is logarithmic: D(−log ⊤)(I) = D(I).

@[simp]

theorem Ideal.logDerivativeIter_zero {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J I : Ideal A) : logDerivativeIter k J 0 I = I

@[simp]

theorem Ideal.logDerivativeIter_succ {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (r : ℕ) (I : Ideal A) : logDerivativeIter k J (r + 1) I = logDerivative k J (logDerivativeIter k J r I)

theorem Ideal.le_logDerivativeIter {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (r : ℕ) (I : Ideal A) : I ≤ logDerivativeIter k J r I

theorem Ideal.logDerivativeIter_mono {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (r : ℕ) {I I' : Ideal A} (h : I ≤ I') : logDerivativeIter k J r I ≤ logDerivativeIter k J r I'

theorem Ideal.logDerivativeIter_le_derivativeIter {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) (r : ℕ) (I : Ideal A) : logDerivativeIter k J r I ≤ derivativeIter k r I

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.logDerivative {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) : X.IdealSheafData

The logarithmic derivative ideal sheaf D(−log S)(I) on a scheme over k ([Kol07, 87]), packaged as derivative of Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean is: on each affine open U, D(−log S(U))(I(U)) for the k-algebra structure f.sectionsAlgebra U.

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.logDerivative f S I = AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals fun (U : ↑X.affineOpens) => Ideal.logDerivative k (S.ideal U) (I.ideal U)

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S : X.IdealSheafData) (r : ℕ) (I : X.IdealSheafData) : X.IdealSheafData

D^r(−log S)(I).

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter f S r I = (AlgebraicGeometry.Scheme.IdealSheafData.logDerivative f S)^[r] I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_zero {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) : logDerivativeIter f S 0 I = I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter_succ {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) (r : ℕ) : logDerivativeIter f S (r + 1) I = logDerivative f S (logDerivativeIter f S r I)

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_logDerivative_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) (U : ↑X.affineOpens) : (logDerivative f S I).ideal U ≤ Ideal.logDerivative k (S.ideal U) (I.ideal U)

On every affine open, (D(−log S)(I))(U) ⊆ D(−log S(U))(I(U)) (Mathlib's ideal_ofIdeals_le).

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_logDerivative {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) : I ≤ logDerivative f S I

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivative_mono {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S : X.IdealSheafData) {I I' : X.IdealSheafData} (h : I ≤ I') : logDerivative f S I ≤ logDerivative f S I'

theorem AlgebraicGeometry.Scheme.IdealSheafData.logDerivative_le_derivative {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (S I : X.IdealSheafData) : logDerivative f S I ≤ derivative f I

D(−log S)(I) ⊆ D(I).