The derivative of an ideal under a formally smooth extension

[Kol07, Lemma 74 (4)]: "if f : Y → X is smooth, then D(f^*I) = f^*(D(I))". This module is the affine-local layer: for a scalar tower k → A → B of commutative rings with φ = algebraMap A B and an ideal J of A, D(J B) = D(J) B when B is formally smooth over A and Ω_{A/k} is finite projective (Ideal.derivative_map_of_formallySmooth).

• D(J) B ⊆ D(J B) holds as soon as every k-derivation δ of A extends to a k-derivation δ̃ of B, δ̃ ∘ φ = φ ∘ δ: then φ(δ f) = δ̃(φ f) ∈ D(J B) (Ideal.map_derivative_le_of_forall_exists_extension). For B formally smooth over A such extensions exist (Derivation.exists_extension_of_formallySmooth): the Jacobi–Zariski sequence H¹(L_{B/A}) → B ⊗_A Ω_{A/k} → Ω_{B/k} → Ω_{B/A} → 0 is exact ([TSPA, Tag 00S2]; Mathlib's Algebra.H1Cotangent.exact_δ_mapBaseChange and KaehlerDifferential.exact_mapBaseChange_map), H¹(L_{B/A}) = 0 and Ω_{B/A} is projective for B formally smooth over A ([TSPA, Tag 00TI]), so B ⊗_A Ω_{A/k} → Ω_{B/k} is a split injection (Derivation.exists_retraction_mapBaseChange), and composing a retraction with B ⊗_A Ω_{A/k} → B, b ⊗ da ↦ b φ(δ a), gives δ̃ through Der_k(B, B) ≅ Hom_B(Ω_{B/k}, B).
• D(J B) ⊆ D(J) B holds as soon as every k-derivation A → B is a B-combination of the φ ∘ ∂, ∂ ∈ Der_k(A, A) (Ideal.derivative_map_le_of_forall_mem_span): for a k-derivation δ of B and f ∈ J, δ(φ f) = ∑ bᵢ φ(∂ᵢ f) ∈ D(J) B, and Leibniz extends this from the generators φ f to all of J B. The spanning holds when Ω_{A/k} is finite projective (Derivation.mem_span_range_compDer_of_projective): Ω_{A/k} is a retract of a finite free module Aⁿ, so an A-linear map Ω_{A/k} → B is ∑ᵢ bᵢ · (φ ∘ ℓᵢ) with ℓᵢ : Ω_{A/k} → A. This inclusion needs no hypothesis on B, only that Ω_{A/k} is finite projective (Kollár's X is smooth over k); the étale case is [Wlo05, Lemma 2.6.5], proved there through the completions.
• The polynomial algebra B = A[y₁, …, y_m] is formally smooth over A (Ideal.derivative_map_mvPolynomial).

The sheaf form is Hironaka/Scheme/IdealSheaf/Derivative/Pullback.lean; the extension of derivations is also used for étale parameters (Hironaka/Scheme/Snc/EtaleParameters.lean).

theorem Derivation.exists_retraction_mapBaseChange {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallySmooth A B] : ∃ (r : Ω[B⁄k] →ₗ[B] TensorProduct A B Ω[A⁄k]), r ∘ₗ KaehlerDifferential.mapBaseChange k A B = LinearMap.id

For B formally smooth over A, the base-change map B ⊗_A Ω_{A/k} → Ω_{B/k} is a split injection: it is injective because H¹(L_{B/A}) = 0 (the Jacobi–Zariski sequence, [TSPA, Tag 00S2]), its cokernel Ω_{B/A} is projective, and a section of Ω_{B/k} → Ω_{B/A} gives a retraction (Mathlib's splitting lemma).

theorem Derivation.exists_extension_of_formallySmooth {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallySmooth A B] (δ : Derivation k A A) : ∃ (δ' : Derivation k B B), ∀ (a : A), δ' ((algebraMap A B) a) = (algebraMap A B) (δ a)

For B formally smooth over A, every k-derivation δ of A extends to a k-derivation δ̃ of B, δ̃ ∘ φ = φ ∘ δ: compose a retraction of B ⊗_A Ω_{A/k} → Ω_{B/k} with b ⊗ da ↦ b φ(δ a).

theorem Derivation.mem_span_range_compDer_of_projective {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Module.Finite A Ω[A⁄k]] [Module.Projective A Ω[A⁄k]] (d : Derivation k A B) : d ∈ Submodule.span B (Set.range fun (δ : Derivation k A A) => (Algebra.linearMap A B).compDer δ)

When Ω_{A/k} is finite projective, every k-derivation d : A → B is a B-linear combination of the φ ∘ ∂, ∂ ∈ Der_k(A, A), that is, Der_k(A, B) = B ⊗_A Der_k(A, A). Through Der_k(A, B) ≅ Hom_A(Ω_{A/k}, B): Ω_{A/k} is a retract of a finite free module Aⁿ (g ∘ s = id), so ℓ = ℓ ∘ g ∘ s = ∑ᵢ ℓ(g eᵢ) · (φ ∘ (prᵢ ∘ s)).

theorem Ideal.map_derivative_le_of_forall_exists_extension {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] (h : ∀ (δ : Derivation k A A), ∃ (δ' : Derivation k B B), ∀ (a : A), δ' ((algebraMap A B) a) = (algebraMap A B) (δ a)) (J : Ideal A) : map (algebraMap A B) (derivative k J) ≤ derivative k (map (algebraMap A B) J)

If every k-derivation of A extends to B, then D(J) B ⊆ D(J B): φ(δ f) = δ̃(φ f) is a derivative of an element of J B.

theorem Ideal.map_derivative_le_derivative_map_of_formallySmooth {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallySmooth A B] (J : Ideal A) : map (algebraMap A B) (derivative k J) ≤ derivative k (map (algebraMap A B) J)

D(J) B ⊆ D(J B) for B formally smooth over A.

theorem Ideal.derivative_map_le_of_forall_mem_span {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] (h : ∀ (d : Derivation k A B), d ∈ Submodule.span B (Set.range fun (δ : Derivation k A A) => (Algebra.linearMap A B).compDer δ)) (J : Ideal A) : derivative k (map (algebraMap A B) J) ≤ map (algebraMap A B) (derivative k J)

If every k-derivation A → B is a B-combination of the φ ∘ ∂, then D(J B) ⊆ D(J) B: on the generators δ(φ f) = ∑ bᵢ φ(∂ᵢ f), and δ(φ(f) b) = b δ(φ f) + φ(f) δ(b) ∈ φ(D(J)) B.

theorem Ideal.derivative_map_le_map_derivative_of_projective {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Module.Finite A Ω[A⁄k]] [Module.Projective 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 when Ω_{A/k} is finite projective, for every A-algebra B; the étale case and the polynomial case are instances.

theorem Ideal.derivative_map_of_formallySmooth {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FormallySmooth A B] [Module.Finite A Ω[A⁄k]] [Module.Projective A Ω[A⁄k]] (J : Ideal A) : derivative k (map (algebraMap A B) J) = map (algebraMap A B) (derivative k J)

[Kol07, Lemma 74 (4)], affine-local form: for B formally smooth over A and Ω_{A/k} finite projective, D(J B) = D(J) B.

theorem Ideal.derivative_map_mvPolynomial {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {σ : Type u_4} [Module.Finite A Ω[A⁄k]] [Module.Projective A Ω[A⁄k]] (J : Ideal A) : derivative k (map (algebraMap A (MvPolynomial σ A)) J) = map (algebraMap A (MvPolynomial σ A)) (derivative k J)

The polynomial case: for B = A[yⱼ : j ∈ σ] and Ω_{A/k} finite projective, D(J B) = D(J) B.