feat(RingTheory/Kaehler): The Kaehler differential module of polynomi…

…al algebras. (#11895)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/Algebra/Polynomial/Derivation.lean

@@ -118,7 +118,7 @@ def compAEval : Derivation R R[X] <| AEval R M a where
   toFun f          := AEval.of R M a (d (aeval a f))
   map_add'         := by simp
   map_smul'        := by simp
-  leibniz'         := by simp [AEval.of_aeval_smul]
+  leibniz'         := by simp [AEval.of_aeval_smul, -Derivation.map_aeval]
   map_one_eq_zero' := by simp
 
 /--

Mathlib/RingTheory/Derivation/Basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri, Andrew Yang
 -/
 import Mathlib.RingTheory.Adjoin.Basic
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.Algebra.Polynomial.Derivative
 
 #align_import ring_theory.derivation.basic from "leanprover-community/mathlib"@"b608348ffaeb7f557f2fd46876037abafd326ff3"
 
@@ -163,6 +165,15 @@ theorem leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a := by
         Nat.succ_eq_add_one, Nat.add_succ_sub_one, add_zero, one_nsmul]
 #align derivation.leibniz_pow Derivation.leibniz_pow
 
+open Polynomial in
+@[simp]
+theorem map_aeval (P : R[X]) (x : A) :
+    D (aeval x P) = aeval x (derivative P) • D x := by
+  induction P using Polynomial.induction_on
+  · simp
+  · simp [add_smul, *]
+  · simp [mul_smul, nsmul_eq_smul_cast A]
+
 theorem eqOn_adjoin {s : Set A} (h : Set.EqOn D1 D2 s) : Set.EqOn D1 D2 (adjoin R s) := fun x hx =>
   Algebra.adjoin_induction hx h (fun r => (D1.map_algebraMap r).trans (D2.map_algebraMap r).symm)
     (fun x y hx hy => by simp only [map_add, *]) fun x y hx hy => by simp only [leibniz, *]

Mathlib/RingTheory/Kaehler.lean

@@ -6,6 +6,8 @@ Authors: Nicolò Cavalleri, Andrew Yang
 import Mathlib.RingTheory.Derivation.ToSquareZero
 import Mathlib.RingTheory.Ideal.Cotangent
 import Mathlib.RingTheory.IsTensorProduct
+import Mathlib.Algebra.MvPolynomial.PDeriv
+import Mathlib.Algebra.Polynomial.Derivation
 
 #align_import ring_theory.kaehler from "leanprover-community/mathlib"@"4b92a463033b5587bb011657e25e4710bfca7364"
 
@@ -687,4 +689,117 @@ theorem KaehlerDifferential.mapBaseChange_tmul (x : B) (y : Ω[A⁄R]) :
 
 end ExactSequence
 
+section MvPolynomial
+
+/-- The relative differential module of a polynomial algebra `R[σ]` is the free module generated by
+`{ dx | x ∈ σ }`. Also see `KaehlerDifferential.mvPolynomialBasis`. -/
+def KaehlerDifferential.mvPolynomialEquiv (σ : Type*) :
+    Ω[MvPolynomial σ R⁄R] ≃ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R where
+  __ := (MvPolynomial.mkDerivation _ (Finsupp.single · 1)).liftKaehlerDifferential
+  invFun := Finsupp.total σ _ _ (fun x ↦ D _ _ (MvPolynomial.X x))
+  right_inv := by
+    intro x
+    induction' x using Finsupp.induction_linear with _ _ _ _ a b
+    · simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]; rw [map_zero, map_zero]
+    · simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *; simp only [*]
+    · simp [LinearMap.map_smul, -map_smul]
+  left_inv := by
+    intro x
+    obtain ⟨x, rfl⟩ := total_surjective _ _ x
+    induction' x using Finsupp.induction_linear with _ _ _ _ a b
+    · simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]; rw [map_zero, map_zero, map_zero]
+    · simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom] at *; simp only [*]
+    · simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Finsupp.total_single,
+        LinearMap.map_smul, Derivation.liftKaehlerDifferential_comp_D]
+      congr 1
+      induction a using MvPolynomial.induction_on
+      · simp only [MvPolynomial.derivation_C, map_zero]
+      · simp only [map_add, *]
+      · simp [*]
+
+/-- `{ dx | x ∈ σ }` forms a basis of the relative differential module
+of a polynomial algebra `R[σ]`. -/
+def KaehlerDifferential.mvPolynomialBasis (σ) :
+    Basis σ (MvPolynomial σ R) (Ω[MvPolynomial σ R⁄R]) :=
+  ⟨mvPolynomialEquiv R σ⟩
+
+lemma KaehlerDifferential.mvPolynomialBasis_repr_comp_D (σ) :
+    (mvPolynomialBasis R σ).repr.toLinearMap.compDer (D _ _) =
+      MvPolynomial.mkDerivation _ (Finsupp.single · 1) :=
+  Derivation.liftKaehlerDifferential_comp _
+
+lemma KaehlerDifferential.mvPolynomialBasis_repr_D (σ) (x) :
+    (mvPolynomialBasis R σ).repr (D _ _ x) =
+      MvPolynomial.mkDerivation R (Finsupp.single · (1 : MvPolynomial σ R)) x :=
+  Derivation.congr_fun (mvPolynomialBasis_repr_comp_D R σ) x
+
+@[simp]
+lemma KaehlerDifferential.mvPolynomialBasis_repr_D_X (σ) (i) :
+    (mvPolynomialBasis R σ).repr (D _ _ (.X i)) = Finsupp.single i 1 := by
+  simp [mvPolynomialBasis_repr_D]
+
+@[simp]
+lemma KaehlerDifferential.mvPolynomialBasis_repr_apply (σ) (x) (i) :
+    (mvPolynomialBasis R σ).repr (D _ _ x) i = MvPolynomial.pderiv i x := by
+  classical
+  suffices ((Finsupp.lapply i).comp
+    (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
+    rw [← this]; rfl
+  apply MvPolynomial.derivation_ext
+  intro j
+  simp [Finsupp.single_apply, Pi.single_apply]
+
+lemma KaehlerDifferential.mvPolynomialBasis_repr_symm_single (σ) (i) (x) :
+    (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • D _ _ (.X i) := by
+  apply (mvPolynomialBasis R σ).repr.injective; simp [LinearEquiv.map_smul, -map_smul]
+
+
+@[simp]
+lemma KaehlerDifferential.mvPolynomialBasis_apply (σ) (i) :
+    mvPolynomialBasis R σ i = D _ _ (.X i) :=
+  (mvPolynomialBasis_repr_symm_single R σ i 1).trans (one_smul _ _)
+
+instance (σ) : Module.Free (MvPolynomial σ R) (Ω[MvPolynomial σ R⁄R]) :=
+  .of_basis (KaehlerDifferential.mvPolynomialBasis R σ)
+
+end MvPolynomial
+
+section Polynomial
+
+open Polynomial
+
+lemma KaehlerDifferential.polynomial_D_apply (P : R[X]) :
+    D R R[X] P = derivative P • D R R[X] X := by
+  rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]
+
+/-- The relative differential module of the univariate polynomial algebra `R[X]` is isomorphic to
+  `R[X]` as an `R[X]`-module. -/
+def KaehlerDifferential.polynomialEquiv : Ω[R[X]⁄R] ≃ₗ[R[X]] R[X] where
+  __ := derivative'.liftKaehlerDifferential
+  invFun := (Algebra.lsmul R R _).toLinearMap.flip (D R R[X] X)
+  left_inv := by
+    intro x
+    obtain ⟨x, rfl⟩ := total_surjective _ _ x
+    induction' x using Finsupp.induction_linear with x y hx hy x y
+    · simp
+    · simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.flip_apply,
+        AlgHom.toLinearMap_apply, lsmul_coe] at *; simp only [*]
+    · simp [polynomial_D_apply _ x]
+  right_inv x := by simp
+
+lemma KaehlerDifferential.polynomialEquiv_comp_D :
+    (polynomialEquiv R).compDer (D R R[X]) = derivative' :=
+  Derivation.liftKaehlerDifferential_comp _
+
+@[simp]
+lemma KaehlerDifferential.polynomialEquiv_D (P) :
+    polynomialEquiv R (D R R[X] P) = derivative P :=
+  Derivation.congr_fun (polynomialEquiv_comp_D R) P
+
+@[simp]
+lemma KaehlerDifferential.polynomialEquiv_symm (P) :
+    (polynomialEquiv R).symm P = P • D R R[X] X := rfl
+
+end Polynomial
+
 end KaehlerDifferential