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.
Equations
- One or more equations did not get rendered due to their size.
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 - Finsupp.single 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 ∈ 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 ∈ 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.
Equations
- MvPolynomial.mkDerivation R f = { toLinearMap := MvPolynomial.mkDerivationₗ R f, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
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 - Finsupp.single 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.
Equations
- One or more equations did not get rendered due to their size.