Documentation

Mathlib.RingTheory.Kaehler.Polynomial

The Kaehler differential module of polynomial algebras #

source
noncomputable def KaehlerDifferential.mvPolynomialEquiv (R : Type u) [CommRing R] (σ : Type u_1) :
Ω[MvPolynomial σ R⁄R] ≃ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R

The relative differential module of a polynomial algebra R[σ] is the free module generated by { dx | x ∈ σ }. Also see KaehlerDifferential.mvPolynomialBasis.

Equations
    Instances For
      source
      noncomputable def KaehlerDifferential.mvPolynomialBasis (R : Type u) [CommRing R] (σ : Type u_1) :
      Module.Basis σ (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]

      { dx | x ∈ σ } forms a basis of the relative differential module of a polynomial algebra R[σ].

      Equations
        Instances For
          source
          theorem KaehlerDifferential.mvPolynomialBasis_repr_comp_D (R : Type u) [CommRing R] (σ : Type u_1) :
          (↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.mkDerivation R fun (x : σ) => Finsupp.single x 1
          source
          theorem KaehlerDifferential.mvPolynomialBasis_repr_D (R : Type u) [CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) :
          (mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x) = (MvPolynomial.mkDerivation R fun (x : σ) => Finsupp.single x 1) x
          source
          @[simp]
          theorem KaehlerDifferential.mvPolynomialBasis_repr_D_X (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) :
          (mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1
          source
          @[simp]
          theorem KaehlerDifferential.mvPolynomialBasis_repr_apply (R : Type u) [CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) (i : σ) :
          ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x
          source
          theorem KaehlerDifferential.mvPolynomialBasis_repr_symm_single (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) (x : MvPolynomial σ R) :
          (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • (D R (MvPolynomial σ R)) (MvPolynomial.X i)
          source
          @[simp]
          theorem KaehlerDifferential.mvPolynomialBasis_apply (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) :
          (mvPolynomialBasis R σ) i = (D R (MvPolynomial σ R)) (MvPolynomial.X i)
          source
          instance instFreeMvPolynomialKaehlerDifferential (R : Type u) [CommRing R] (σ : Type u_1) :
          Module.Free (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]
          source
          theorem KaehlerDifferential.polynomial_D_apply (R : Type u) [CommRing R] (P : Polynomial R) :
          (D R (Polynomial R)) P = Polynomial.derivative P • (D R (Polynomial R)) Polynomial.X
          source
          noncomputable def KaehlerDifferential.polynomialEquiv (R : Type u) [CommRing R] :
          Ω[Polynomial R⁄R] ≃ₗ[Polynomial R] Polynomial R

          The relative differential module of the univariate polynomial algebra R[X] is isomorphic to R[X] as an R[X]-module.

          Equations
            Instances For
              source
              theorem KaehlerDifferential.polynomialEquiv_comp_D (R : Type u) [CommRing R] :
              (polynomialEquiv R).compDer (D R (Polynomial R)) = Polynomial.derivative'
              source
              @[simp]
              theorem KaehlerDifferential.polynomialEquiv_D (R : Type u) [CommRing R] (P : Polynomial R) :
              (polynomialEquiv R) ((D R (Polynomial R)) P) = Polynomial.derivative P
              source
              @[simp]
              theorem KaehlerDifferential.polynomialEquiv_symm (R : Type u) [CommRing R] (P : Polynomial R) :
              (polynomialEquiv R).symm P = P • (D R (Polynomial R)) Polynomial.X