Derivations of multivariate polynomials #
In this file we prove that a derivation of MvPolynomial σ R is determined by its values on all
monomials MvPolynomial.X i. We also provide a constructor MvPolynomial.mkDerivation that
builds a derivation from its values on X is and a linear equivalence
MvPolynomial.mkDerivationEquiv between σ → A and Derivation (MvPolynomial σ R) A.
def
MvPolynomial.mkDerivationₗ
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
(f : σ → A)
:
MvPolynomial σ R →ₗ[R] A
The derivation on MvPolynomial σ R that takes value f i on X i, as a linear map.
Use MvPolynomial.mkDerivation instead.
Instances For
theorem
MvPolynomial.mkDerivationₗ_monomial
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
(f : σ → A)
(s : σ →₀ ℕ)
(r : R)
:
↑(MvPolynomial.mkDerivationₗ R f) (↑(MvPolynomial.monomial s) r) = r • Finsupp.sum s fun i k => ↑(MvPolynomial.monomial (s - fun₀ | i => 1)) ↑k • f i
theorem
MvPolynomial.mkDerivationₗ_C
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
(f : σ → A)
(r : R)
:
↑(MvPolynomial.mkDerivationₗ R f) (↑MvPolynomial.C r) = 0
theorem
MvPolynomial.mkDerivationₗ_X
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
(f : σ → A)
(i : σ)
:
↑(MvPolynomial.mkDerivationₗ R f) (MvPolynomial.X i) = f i
@[simp]
theorem
MvPolynomial.derivation_C
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
(D : Derivation R (MvPolynomial σ R) A)
(a : R)
:
↑D (↑MvPolynomial.C a) = 0
@[simp]
theorem
MvPolynomial.derivation_C_mul
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
(D : Derivation R (MvPolynomial σ R) A)
(a : R)
(f : MvPolynomial σ R)
:
theorem
MvPolynomial.derivation_eqOn_supported
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
{D₁ : Derivation R (MvPolynomial σ R) A}
{D₂ : Derivation R (MvPolynomial σ R) A}
{s : Set σ}
(h : Set.EqOn (↑D₁ ∘ MvPolynomial.X) (↑D₂ ∘ MvPolynomial.X) s)
{f : MvPolynomial σ R}
(hf : f ∈ MvPolynomial.supported R s)
:
↑D₁ f = ↑D₂ f
If two derivations agree on X i, i ∈ s, then they agree on all polynomials from
MvPolynomial.supported R s.
theorem
MvPolynomial.derivation_eq_of_forall_mem_vars
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
{D₁ : Derivation R (MvPolynomial σ R) A}
{D₂ : Derivation R (MvPolynomial σ R) A}
{f : MvPolynomial σ R}
(h : ∀ (i : σ), i ∈ MvPolynomial.vars f → ↑D₁ (MvPolynomial.X i) = ↑D₂ (MvPolynomial.X i))
:
↑D₁ f = ↑D₂ f
theorem
MvPolynomial.derivation_eq_zero_of_forall_mem_vars
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
{D : Derivation R (MvPolynomial σ R) A}
{f : MvPolynomial σ R}
(h : ∀ (i : σ), i ∈ MvPolynomial.vars f → ↑D (MvPolynomial.X i) = 0)
:
↑D f = 0
theorem
MvPolynomial.derivation_ext
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
{D₁ : Derivation R (MvPolynomial σ R) A}
{D₂ : Derivation R (MvPolynomial σ R) A}
(h : ∀ (i : σ), ↑D₁ (MvPolynomial.X i) = ↑D₂ (MvPolynomial.X i))
:
D₁ = D₂
theorem
MvPolynomial.leibniz_iff_X
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
[IsScalarTower R (MvPolynomial σ R) A]
(D : MvPolynomial σ R →ₗ[R] A)
(h₁ : ↑D 1 = 0)
:
(∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p) ↔ ∀ (s : σ →₀ ℕ) (i : σ),
↑D (↑(MvPolynomial.monomial s) 1 * MvPolynomial.X i) = ↑(MvPolynomial.monomial s) 1 • ↑D (MvPolynomial.X i) + MvPolynomial.X i • ↑D (↑(MvPolynomial.monomial s) 1)
def
MvPolynomial.mkDerivation
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
[IsScalarTower R (MvPolynomial σ R) A]
(f : σ → A)
:
Derivation R (MvPolynomial σ R) A
The derivation on MvPolynomial σ R that takes value f i on X i.
Instances For
@[simp]
theorem
MvPolynomial.mkDerivation_X
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
[IsScalarTower R (MvPolynomial σ R) A]
(f : σ → A)
(i : σ)
:
↑(MvPolynomial.mkDerivation R f) (MvPolynomial.X i) = f i
theorem
MvPolynomial.mkDerivation_monomial
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
[IsScalarTower R (MvPolynomial σ R) A]
(f : σ → A)
(s : σ →₀ ℕ)
(r : R)
:
↑(MvPolynomial.mkDerivation R f) (↑(MvPolynomial.monomial s) r) = r • Finsupp.sum s fun i k => ↑(MvPolynomial.monomial (s - fun₀ | i => 1)) ↑k • f i
def
MvPolynomial.mkDerivationEquiv
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Module (MvPolynomial σ R) A]
[IsScalarTower R (MvPolynomial σ R) A]
:
(σ → A) ≃ₗ[R] Derivation R (MvPolynomial σ R) A
MvPolynomial.mkDerivation as a linear equivalence.