Restriction of the logarithmic derivative ideal to the hypersurface

[Kol07, (87.1)]: D^r(−log S)(I)|_S = D^r(I|_S), the logarithmic derivations along S restrict to all the derivations of S. At the level of rings: for a surjection ψ : A → B of k-algebras with kernel J and Ω_{A/k} projective (for instance A formally smooth over k, as the stalks of a smooth scheme are), ψ(D(−log J)(I)) = D(ψ(I)) (Ideal.logDerivative_map_of_surjective; logDerivative_map_mk for B = A/J), and likewise for the iterates (logDerivativeIter_map_of_surjective).

• ⊆: a k-derivation δ of A preserving J = ker ψ descends to B, δ_B(ψ a) = ψ(δ a) (Derivation.descendOfSurjective: the quotient derivation quotientOfMapLE of Hironaka/Algebra/Local/QuotientCoords.lean on A/J, conjugated along the first isomorphism theorem A/J ≅ B); so ψ(δ f) = δ_B(ψ f) ∈ D(ψ(I)).
• ⊇: a k-derivation δ' of B lifts to a k-derivation δ of A preserving ker ψ with ψ ∘ δ = δ' ∘ ψ (Derivation.exists_preservesIdeal_ker_of_surjective): through Der_k(A, B) ≅ Hom_A(Ω_{A/k}, B), the A-linear map Ω_{A/k} → B of δ' ∘ ψ lifts along the surjection A → B because Ω_{A/k} is projective (Mathlib's projective_lifting_property); the lift preserves the kernel since ψ(δ a) = δ'(ψ a) = 0 for a ∈ ker ψ. Then δ'(ψ f) = ψ(δ f) ∈ ψ(D(−log J)(I)) for f ∈ I, and Leibniz extends this to ψ(I).

In coordinates with S = (x₁), the logarithmic generators x₁ ∂₁, ∂₂, … restrict to 0, ∂̄₂, …, which is Dlog_map_quotient of Hironaka/Algebra/Local/LogDeriv.lean; the proof here needs no coordinates. The conjugation of a derivation by an algebra isomorphism is Derivation.conjAlgEquiv of Hironaka/Algebra/Derivative/Equiv.lean.

Used for the logarithmic derivative ideal sheaf (Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean) and for Corollary 89 (Hironaka/Resolution/Algebraic/Kol07/Corollary89.lean).

noncomputable def Derivation.descendOfSurjective {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (ψ : A →ₐ[k] B) (hψ : Function.Surjective ⇑ψ) {δ : Derivation k A A} (hδ : δ.PreservesIdeal (RingHom.ker ψ)) : Derivation k B B

A derivation of A preserving the kernel of the surjection ψ : A → B descends to a derivation of B, δ_B(ψ a) = ψ(δ a) (quotientOfMapLE on A / ker ψ, transported along A / ker ψ ≅ B).

Equations

• Derivation.descendOfSurjective ψ hψ hδ = Derivation.conjAlgEquiv (Ideal.quotientKerAlgEquivOfSurjective hψ) (δ.quotientOfMapLE (RingHom.ker ψ) ⋯)

theorem Derivation.descendOfSurjective_apply {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (ψ : A →ₐ[k] B) (hψ : Function.Surjective ⇑ψ) {δ : Derivation k A A} (hδ : δ.PreservesIdeal (RingHom.ker ψ)) (a : A) : (descendOfSurjective ψ hψ hδ) (ψ a) = ψ (δ a)

theorem Derivation.exists_preservesIdeal_ker_of_surjective {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (ψ : A →ₐ[k] B) [Module.Projective A Ω[A⁄k]] (hψ : Function.Surjective ⇑ψ) (δ' : Derivation k B B) : ∃ (δ : Derivation k A A), δ.PreservesIdeal (RingHom.ker ψ) ∧ ∀ (a : A), ψ (δ a) = δ' (ψ a)

When Ω_{A/k} is projective, every k-derivation of B lifts through the surjection ψ : A → B to a k-derivation of A preserving ker ψ.

theorem Ideal.logDerivative_map_of_surjective {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Module.Projective A Ω[A⁄k]] (ψ : A →ₐ[k] B) (hψ : Function.Surjective ⇑ψ) (I : Ideal A) : map ψ (logDerivative k (RingHom.ker ψ) I) = derivative k (map ψ I)

[Kol07, (87.1)] at the level of rings: for a surjection ψ : A → B of k-algebras with Ω_{A/k} projective, ψ(D(−log (ker ψ))(I)) = D(ψ(I)).

theorem Ideal.logDerivativeIter_map_of_surjective {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Module.Projective A Ω[A⁄k]] (ψ : A →ₐ[k] B) (hψ : Function.Surjective ⇑ψ) (r : ℕ) (I : Ideal A) : map ψ (logDerivativeIter k (RingHom.ker ψ) r I) = derivativeIter k r (map ψ I)

The iterates: ψ(D^r(−log (ker ψ))(I)) = D^r(ψ(I)).

theorem Ideal.logDerivativeIter_map_of_surjective' {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Module.Projective A Ω[A⁄k]] (ψ : A →+* B) (hc : ∀ (c : k), ψ ((algebraMap k A) c) = (algebraMap k B) c) (hψ : Function.Surjective ⇑ψ) (r : ℕ) (I : Ideal A) : map ψ (logDerivativeIter k (RingHom.ker ψ) r I) = derivativeIter k r (map ψ I)

The same for a ring map ψ compatible with the k-structures (the stalk map of a closed immersion of k-schemes).

theorem Ideal.logDerivative_map_mk {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] [Algebra.FormallySmooth k A] (J I : Ideal A) : map (Quotient.mk J) (logDerivative k J I) = derivative k (map (Quotient.mk J) I)

[Kol07, (87.1)] for a quotient: for A formally smooth over k and any ideal J, D(−log J)(I) · (A/J) = D(I · (A/J)).