Documentation

Mathlib.RingTheory.Kaehler.Polynomial

The Kähler 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
  • One or more equations did not get rendered due to their size.
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
      • One or more equations did not get rendered due to their size.
      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