The Kaehler differential module of polynomial algebras #
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
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
Instances For
@[simp]
theorem
KaehlerDifferential.mvPolynomialBasis_apply
(R : Type u)
[CommRing R]
(σ : Type u_1)
(i : σ)
:
instance
instFreeMvPolynomialKaehlerDifferential
(R : Type u)
[CommRing R]
(σ : Type u_1)
:
Module.Free (MvPolynomial σ R) (Ω[MvPolynomial σ R⁄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
@[simp]