The Kaehler 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) : Basis σ (MvPolynomial σ R) (Ω[MvPolynomial σ R⁄R])

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

Equations

• KaehlerDifferential.mvPolynomialBasis R σ = { repr := KaehlerDifferential.mvPolynomialEquiv R σ }

theorem KaehlerDifferential.mvPolynomialBasis_repr_comp_D (R : Type u) [CommRing R] (σ : Type u_1) : (↑(KaehlerDifferential.mvPolynomialBasis R σ).repr).compDer (KaehlerDifferential.D R (MvPolynomial σ R)) = MvPolynomial.mkDerivation R fun (x : σ) => Finsupp.single x 1

theorem KaehlerDifferential.mvPolynomialBasis_repr_D (R : Type u) [CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) : (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x) = (MvPolynomial.mkDerivation R fun (x : σ) => Finsupp.single x 1) x

@[simp]

theorem KaehlerDifferential.mvPolynomialBasis_repr_D_X (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) : (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1

@[simp]

theorem KaehlerDifferential.mvPolynomialBasis_repr_apply (R : Type u) [CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) (i : σ) : ((KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.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) : (KaehlerDifferential.mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)

@[simp]

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

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

Equations

• ⋯ = ⋯

theorem KaehlerDifferential.polynomial_D_apply (R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P • (KaehlerDifferential.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.

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

@[simp]

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