The derivative of an ideal commutes with localization

For a localization B = M⁻¹A of a k-algebra A, D(J B) = D(J) B (Ideal.derivative_map): the compatibility that makes the derivative of an ideal a sheaf ([Kol07, Definition 73] defines D(I) through the sheaf Der_X; Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean).

• ⊇: a k-derivation of A extends to B by the quotient rule (as the ∂/∂uᵢ extend to the function field in the proof of [Wlo05, Lemma 2.6.3]): Derivation.localization of Hironaka/Algebra/DerivationLocalization.lean for Localization M, transported to an arbitrary B with IsLocalization M B along Mathlib's IsLocalization.algEquiv (Derivation.extendToLocalization, extendToLocalization_algebraMap); so φ (δ f) = δ̃ (φ f) ∈ D(J B) (derivative_map_le).
• ⊆: when Ω_{A/k} is finitely presented, every k-derivation δ' of B is, up to a unit, an extension: its restriction d : A → B corresponds under linearMapEquivDerivation to an A-linear map Ω_{A/k} → B, which by Mathlib's Module.FinitePresentation.exists_lift_of_isLocalizedModule is s⁻¹ · (φ ∘ h) for some h : Ω_{A/k} → A and s ∈ M (exists_derivation_smul_eq); so δ' (φ f) = φ(s)⁻¹ φ(δ_h f) ∈ D(J) B for f ∈ J, and Leibniz extends this to all of J B.

Used for the derivative ideal sheaf (Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean), its logarithmic version (Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicLocalization.lean), for Theorem 76 on schemes (Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean), on affine space (Hironaka/Scheme/IdealSheaf/Order/AffineSpace.lean) and on analytic spaces (Hironaka/Analytic/Rueckert/Hypersurface.lean). The statement is not in the sources.

noncomputable def Derivation.localizationAlgEquiv (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] : Localization M ≃ₐ[k] B

The k-algebra equivalence Localization M ≃ B of an abstract localization.

Equations

• Derivation.localizationAlgEquiv k M = AlgEquiv.restrictScalars k (IsLocalization.algEquiv M (Localization M) B)

theorem Derivation.localizationAlgEquiv_algebraMap (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] (a : A) : (localizationAlgEquiv k M) ((algebraMap A (Localization M)) a) = (algebraMap A B) a

theorem Derivation.localizationAlgEquiv_symm_algebraMap (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] (a : A) : (localizationAlgEquiv k M).symm ((algebraMap A B) a) = (algebraMap A (Localization M)) a

noncomputable def Derivation.extendToLocalization {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] (D : Derivation k A A) : Derivation k B B

Extension of a derivation to an abstract localization: Derivation.localization of Hironaka/Algebra/DerivationLocalization.lean transported along IsLocalization.algEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem Derivation.extendToLocalization_apply {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] (D : Derivation k A A) (b : B) : (extendToLocalization M D) b = (localizationAlgEquiv k M) ((localization M D) ((localizationAlgEquiv k M).symm b))

@[simp]

theorem Derivation.extendToLocalization_algebraMap {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] (D : Derivation k A A) (a : A) : (extendToLocalization M D) ((algebraMap A B) a) = (algebraMap A B) (D a)

The extension agrees with D on the image of A.

theorem Ideal.derivative_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] (J : Ideal A) : map (algebraMap A B) (derivative k J) ≤ derivative k (map (algebraMap A B) J)

The inclusion D(J) B ⊆ D(J B): derivations of A extend to B.

theorem Ideal.exists_derivation_smul_eq {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]] (δ' : Derivation k B B) : ∃ (δ : Derivation k A A) (s : ↥M), ∀ (a : A), (algebraMap A B) (δ a) = (algebraMap A B) ↑s * δ' ((algebraMap A B) a)

Every k-derivation of the localization B is, up to a unit φ s, the extension of a k-derivation of A, when Ω_{A/k} is finitely presented (Mathlib's Module.FinitePresentation.exists_lift_of_isLocalizedModule for Hom_A(Ω_{A/k}, B)).

theorem Ideal.derivative_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) : derivative k (map (algebraMap A B) J) = map (algebraMap A B) (derivative k J)

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