The logarithmic derivative ideal commutes with localization

For a localization B = M⁻¹A of a k-algebra A and ideals J, I of A, D(−log (J B))(I B) = D(−log J)(I) · B, provided Ω_{A/k} is finitely presented and J is finitely generated (Ideal.logDerivative_map; logDerivativeIter_map for the iterates). This is the compatibility with restriction to basic opens that makes the affine family U ↦ D(−log S(U))(I(U)) of Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean an ideal sheaf (Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean); Kollár treats D(−log S)(I) as a sheaf from the start ([Kol07, 87]).

• Preservation passes to the localization (Derivation.PreservesIdeal.map_of_forall): if δ' ∘ φ = φ ∘ δ and δ(J) ⊆ J then δ'(J B) ⊆ J B, by Leibniz on the generators φ(J). So the extension δ̃ of a J-preserving derivation (extendToLocalization, Hironaka/Algebra/Derivative/Localization.lean) preserves J B, which gives ⊇ (map_logDerivative_le).
• ⊆: a k-derivation δ' of B preserving J B is, up to the unit φ(s), the extension of a derivation δ of A (exists_derivation_smul_eq); δ need not preserve J, only its M-saturation. Clearing denominators (exists_smul_preservesIdeal): for each of the finitely many generators g of J, φ(δ g) = φ(s) δ'(φ g) ∈ J B, so m_g · δ g ∈ J for some m_g ∈ M; with m = ∏ m_g, the derivation m δ maps the generators into J, hence preserves J (Leibniz), and φ(m δ f) = φ(m s) δ'(φ f) with φ(m s) a unit. So δ'(φ f) ∈ D(−log J)(I) B for f ∈ I, and Leibniz extends this to I B (logDerivative_map_le).

Used for the logarithmic derivative ideal sheaf (Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean), for Theorem 88 and (87.3) on schemes (Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean, Hironaka/Scheme/BlowUpSequence/TransformLogDerivative.lean) and for the blow-up chart (Hironaka/Algebra/Local/BlowUpLiftLog.lean). The statement is not in the sources.

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

A derivation preserves span s iff it maps the generators into span s (Leibniz).

theorem Derivation.PreservesIdeal.map_of_forall {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] {δ : Derivation k A A} {J : Ideal A} (hδ : δ.PreservesIdeal J) (φ : A →+* B) (δ' : Derivation k B B) (h : ∀ (a : A), δ' (φ a) = φ (δ a)) : δ'.PreservesIdeal (Ideal.map φ J)

If δ' extends δ along the ring map φ (δ' ∘ φ = φ ∘ δ) and δ preserves J, then δ' preserves the extended ideal J B = span (φ(J)).

theorem Ideal.map_logDerivative_le {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra A B] [Algebra k B] [IsScalarTower k A B] (M : Submonoid A) [IsLocalization M B] (J I : Ideal A) : map (algebraMap A B) (logDerivative k J I) ≤ logDerivative k (map (algebraMap A B) J) (map (algebraMap A B) I)

The inclusion D(−log J)(I) B ⊆ D(−log (J B))(I B): a J-preserving derivation of A extends to a J B-preserving derivation of B.

theorem Ideal.exists_smul_preservesIdeal {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra A B] [Algebra k B] (M : Submonoid A) [IsLocalization M B] {J : Ideal A} (hJ : J.FG) {δ' : Derivation k B B} (hδ' : δ'.PreservesIdeal (map (algebraMap A B) J)) {δ : Derivation k A A} {s : ↥M} (h : ∀ (a : A), (algebraMap A B) (δ a) = (algebraMap A B) ↑s * δ' ((algebraMap A B) a)) : ∃ (m : ↥M), (↑m • δ).PreservesIdeal J

Clearing denominators: if δ' preserves J B and φ ∘ δ = φ(s) · δ' ∘ φ, then for a finitely generated J some multiple m δ, m ∈ M, preserves J.

theorem Ideal.logDerivative_map_le {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra A B] [Algebra k B] [IsScalarTower k A B] (M : Submonoid A) [IsLocalization M B] [Module.FinitePresentation A Ω[A⁄k]] {J : Ideal A} (hJ : J.FG) (I : Ideal A) : logDerivative k (map (algebraMap A B) J) (map (algebraMap A B) I) ≤ map (algebraMap A B) (logDerivative k J I)

The inclusion D(−log (J B))(I B) ⊆ D(−log J)(I) B for a localization B = M⁻¹A, Ω_{A/k} finitely presented and J finitely generated.

theorem Ideal.logDerivative_map {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra A B] [Algebra k B] [IsScalarTower k A B] (M : Submonoid A) [IsLocalization M B] [Module.FinitePresentation A Ω[A⁄k]] {J : Ideal A} (hJ : J.FG) (I : Ideal A) : logDerivative k (map (algebraMap A B) J) (map (algebraMap A B) I) = map (algebraMap A B) (logDerivative k J I)

D(−log (J B))(I B) = D(−log J)(I) B for a localization B = M⁻¹A when Ω_{A/k} is finitely presented and J is finitely generated.

theorem Ideal.logDerivativeIter_map {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra A B] [Algebra k B] [IsScalarTower k A B] (M : Submonoid A) [IsLocalization M B] [Module.FinitePresentation A Ω[A⁄k]] {J : Ideal A} (hJ : J.FG) (r : ℕ) (I : Ideal A) : logDerivativeIter k (map (algebraMap A B) J) r (map (algebraMap A B) I) = map (algebraMap A B) (logDerivativeIter k J r I)

The iterates: D^r(−log (J B))(I B) = D^r(−log J)(I) B.