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
.
Instances For
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 σ }
Instances For
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)
theorem
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)
:
(KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X
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
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