From 7c80fcc7d539578394dac22e7d27bbe7df1602e3 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Thu, 20 Jun 2024 07:22:13 +0000 Subject: [PATCH] chore: split RingTheory/Kaehler (#13978) Put materials about (Mv)Polynomial into Kaehler/Polynomial and the others into Kaehler/Basic --- Mathlib.lean | 3 +- .../{Kaehler.lean => Kaehler/Basic.lean} | 118 +-------------- Mathlib/RingTheory/Kaehler/Polynomial.lean | 135 ++++++++++++++++++ .../RingTheory/Unramified/Derivations.lean | 2 +- 4 files changed, 139 insertions(+), 119 deletions(-) rename Mathlib/RingTheory/{Kaehler.lean => Kaehler/Basic.lean} (88%) create mode 100644 Mathlib/RingTheory/Kaehler/Polynomial.lean diff --git a/Mathlib.lean b/Mathlib.lean index 46217cd6ef43c..e52886f7a2609 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3596,7 +3596,8 @@ import Mathlib.RingTheory.IsAdjoinRoot import Mathlib.RingTheory.IsTensorProduct import Mathlib.RingTheory.Jacobson import Mathlib.RingTheory.JacobsonIdeal -import Mathlib.RingTheory.Kaehler +import Mathlib.RingTheory.Kaehler.Basic +import Mathlib.RingTheory.Kaehler.Polynomial import Mathlib.RingTheory.LaurentSeries import Mathlib.RingTheory.LittleWedderburn import Mathlib.RingTheory.LocalProperties diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler/Basic.lean similarity index 88% rename from Mathlib/RingTheory/Kaehler.lean rename to Mathlib/RingTheory/Kaehler/Basic.lean index 9cad54b08925a..d4ff115ea9228 100644 --- a/Mathlib/RingTheory/Kaehler.lean +++ b/Mathlib/RingTheory/Kaehler/Basic.lean @@ -7,8 +7,6 @@ import Mathlib.RingTheory.Derivation.ToSquareZero import Mathlib.RingTheory.Ideal.Cotangent import Mathlib.RingTheory.IsTensorProduct import Mathlib.Algebra.Exact -import Mathlib.Algebra.MvPolynomial.PDeriv -import Mathlib.Algebra.Polynomial.Derivation #align_import ring_theory.kaehler from "leanprover-community/mathlib"@"4b92a463033b5587bb011657e25e4710bfca7364" @@ -167,7 +165,7 @@ notation:100 "Ω[" S "⁄" R "]" => KaehlerDifferential R S instance : Nonempty (Ω[S⁄R]) := ⟨0⟩ instance KaehlerDifferential.module' {R' : Type*} [CommRing R'] [Algebra R' S] - [SMulCommClass R R' S] : + [SMulCommClass R R' S] : Module R' (Ω[S⁄R]) := Submodule.Quotient.module' _ #align kaehler_differential.module' KaehlerDifferential.module' @@ -767,118 +765,4 @@ lemma KaehlerDifferential.exact_mapBaseChange_map : 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] - -set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534 -lemma KaehlerDifferential.mvPolynomialBasis_repr_symm_single (σ) (i) (x) : - (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • D R (MvPolynomial σ R) (.X i) := by - apply (mvPolynomialBasis R σ).repr.injective; simp [LinearEquiv.map_smul, -map_smul] - -set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534 -@[simp] -lemma KaehlerDifferential.mvPolynomialBasis_apply (σ) (i) : - mvPolynomialBasis R σ i = D R (MvPolynomial σ R) (.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 diff --git a/Mathlib/RingTheory/Kaehler/Polynomial.lean b/Mathlib/RingTheory/Kaehler/Polynomial.lean new file mode 100644 index 0000000000000..5e99b0dd65beb --- /dev/null +++ b/Mathlib/RingTheory/Kaehler/Polynomial.lean @@ -0,0 +1,135 @@ +/- +Copyright (c) 2024 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import Mathlib.RingTheory.Kaehler.Basic +import Mathlib.Algebra.MvPolynomial.PDeriv +import Mathlib.Algebra.Polynomial.Derivation + +/-! +# The Kaehler differential module of polynomial algebras +-/ + +open scoped TensorProduct +open Algebra + +universe u v + +variable (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] + +suppress_compilation + +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] + +set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534 +lemma KaehlerDifferential.mvPolynomialBasis_repr_symm_single (σ) (i) (x) : + (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • D R (MvPolynomial σ R) (.X i) := by + apply (mvPolynomialBasis R σ).repr.injective; simp [LinearEquiv.map_smul, -map_smul] + +set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534 +@[simp] +lemma KaehlerDifferential.mvPolynomialBasis_apply (σ) (i) : + mvPolynomialBasis R σ i = D R (MvPolynomial σ R) (.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 diff --git a/Mathlib/RingTheory/Unramified/Derivations.lean b/Mathlib/RingTheory/Unramified/Derivations.lean index 35e25900388a5..096eee6fd664c 100644 --- a/Mathlib/RingTheory/Unramified/Derivations.lean +++ b/Mathlib/RingTheory/Unramified/Derivations.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ -import Mathlib.RingTheory.Kaehler +import Mathlib.RingTheory.Kaehler.Basic import Mathlib.RingTheory.Unramified.Basic /-!