The Kähler differential module of polynomial algebras

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.

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[σ].

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 : σ) => fun₀ | x => 1

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 : σ) => fun₀ | x => 1) x

@[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)) = fun₀ | i => 1

@[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

theorem KaehlerDifferential.mvPolynomialBasis_repr_symm_single (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) (x : MvPolynomial σ R) : ((mvPolynomialBasis R σ).repr.symm fun₀ | i => x) = x • (D R (MvPolynomial σ R)) (MvPolynomial.X i)

@[simp]

theorem KaehlerDifferential.mvPolynomialBasis_apply (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) : (mvPolynomialBasis R σ) i = (D R (MvPolynomial σ R)) (MvPolynomial.X i)

instance instFreeMvPolynomialKaehlerDifferential (R : Type u) [CommRing R] (σ : Type u_1) : Module.Free (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]

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

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.

theorem KaehlerDifferential.polynomialEquiv_comp_D (R : Type u) [CommRing R] : (polynomialEquiv R).compDer (D R (Polynomial R)) = Polynomial.derivative'

@[simp]

theorem KaehlerDifferential.polynomialEquiv_D (R : Type u) [CommRing R] (P : Polynomial R) : (polynomialEquiv R) ((D R (Polynomial R)) P) = Polynomial.derivative P

@[simp]

theorem KaehlerDifferential.polynomialEquiv_symm (R : Type u) [CommRing R] (P : Polynomial R) : (polynomialEquiv R).symm P = P • (D R (Polynomial R)) Polynomial.X