Derivations of multivariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that a derivation of mv_polynomial σ R is determined by its values on all
monomials mv_polynomial.X i. We also provide a constructor mv_polynomial.mk_derivation that
builds a derivation from its values on X is and a linear equivalence
mv_polynomial.equiv_derivation between σ → A and derivation (mv_polynomial σ R) A.
noncomputable
def
mv_polynomial.mk_derivationₗ
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
(f : σ → A) :
mv_polynomial σ R →ₗ[R] A
The derivation on mv_polynomial σ R that takes value f i on X i, as a linear map.
Use mv_polynomial.mk_derivation instead.
Equations
- mv_polynomial.mk_derivationₗ R f = ⇑(finsupp.lsum R) (λ (xs : σ →₀ ℕ), ⇑((linear_map.ring_lmap_equiv_self R R A).symm) (xs.sum (λ (i : σ) (k : ℕ), ⇑(mv_polynomial.monomial (xs - finsupp.single i 1)) ↑k • f i)))
theorem
mv_polynomial.mk_derivationₗ_monomial
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
(f : σ → A)
(s : σ →₀ ℕ)
(r : R) :
⇑(mv_polynomial.mk_derivationₗ R f) (⇑(mv_polynomial.monomial s) r) = r • s.sum (λ (i : σ) (k : ℕ), ⇑(mv_polynomial.monomial (s - finsupp.single i 1)) ↑k • f i)
theorem
mv_polynomial.mk_derivationₗ_C
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
(f : σ → A)
(r : R) :
⇑(mv_polynomial.mk_derivationₗ R f) (⇑mv_polynomial.C r) = 0
theorem
mv_polynomial.mk_derivationₗ_X
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
(f : σ → A)
(i : σ) :
⇑(mv_polynomial.mk_derivationₗ R f) (mv_polynomial.X i) = f i
@[simp]
theorem
mv_polynomial.derivation_C
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
(D : derivation R (mv_polynomial σ R) A)
(a : R) :
⇑D (⇑mv_polynomial.C a) = 0
@[simp]
theorem
mv_polynomial.derivation_C_mul
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
(D : derivation R (mv_polynomial σ R) A)
(a : R)
(f : mv_polynomial σ R) :
theorem
mv_polynomial.derivation_eq_on_supported
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
{D₁ D₂ : derivation R (mv_polynomial σ R) A}
{s : set σ}
(h : set.eq_on (⇑D₁ ∘ mv_polynomial.X) (⇑D₂ ∘ mv_polynomial.X) s)
{f : mv_polynomial σ R}
(hf : f ∈ mv_polynomial.supported R s) :
If two derivations agree on X i, i ∈ s, then they agree on all polynomials from
mv_polynomial.supported R s.
theorem
mv_polynomial.derivation_eq_of_forall_mem_vars
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
{D₁ D₂ : derivation R (mv_polynomial σ R) A}
{f : mv_polynomial σ R}
(h : ∀ (i : σ), i ∈ f.vars → ⇑D₁ (mv_polynomial.X i) = ⇑D₂ (mv_polynomial.X i)) :
theorem
mv_polynomial.derivation_eq_zero_of_forall_mem_vars
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
{D : derivation R (mv_polynomial σ R) A}
{f : mv_polynomial σ R}
(h : ∀ (i : σ), i ∈ f.vars → ⇑D (mv_polynomial.X i) = 0) :
@[ext]
theorem
mv_polynomial.derivation_ext
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
{D₁ D₂ : derivation R (mv_polynomial σ R) A}
(h : ∀ (i : σ), ⇑D₁ (mv_polynomial.X i) = ⇑D₂ (mv_polynomial.X i)) :
D₁ = D₂
theorem
mv_polynomial.leibniz_iff_X
{σ : Type u_1}
{R : Type u_2}
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
[is_scalar_tower R (mv_polynomial σ R) A]
(D : mv_polynomial σ R →ₗ[R] A)
(h₁ : ⇑D 1 = 0) :
(∀ (p q : mv_polynomial σ R), ⇑D (p * q) = p • ⇑D q + q • ⇑D p) ↔ ∀ (s : σ →₀ ℕ) (i : σ), ⇑D (⇑(mv_polynomial.monomial s) 1 * mv_polynomial.X i) = ⇑(mv_polynomial.monomial s) 1 • ⇑D (mv_polynomial.X i) + mv_polynomial.X i • ⇑D (⇑(mv_polynomial.monomial s) 1)
noncomputable
def
mv_polynomial.mk_derivation
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
[is_scalar_tower R (mv_polynomial σ R) A]
(f : σ → A) :
derivation R (mv_polynomial σ R) A
The derivation on mv_polynomial σ R that takes value f i on X i.
Equations
- mv_polynomial.mk_derivation R f = {to_linear_map := mv_polynomial.mk_derivationₗ R f, map_one_eq_zero' := _, leibniz' := _}
@[simp]
theorem
mv_polynomial.mk_derivation_X
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
[is_scalar_tower R (mv_polynomial σ R) A]
(f : σ → A)
(i : σ) :
⇑(mv_polynomial.mk_derivation R f) (mv_polynomial.X i) = f i
theorem
mv_polynomial.mk_derivation_monomial
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
[is_scalar_tower R (mv_polynomial σ R) A]
(f : σ → A)
(s : σ →₀ ℕ)
(r : R) :
⇑(mv_polynomial.mk_derivation R f) (⇑(mv_polynomial.monomial s) r) = r • s.sum (λ (i : σ) (k : ℕ), ⇑(mv_polynomial.monomial (s - finsupp.single i 1)) ↑k • f i)
noncomputable
def
mv_polynomial.mk_derivation_equiv
{σ : Type u_1}
(R : Type u_2)
{A : Type u_3}
[comm_semiring R]
[add_comm_monoid A]
[module R A]
[module (mv_polynomial σ R) A]
[is_scalar_tower R (mv_polynomial σ R) A] :
(σ → A) ≃ₗ[R] derivation R (mv_polynomial σ R) A
mv_polynomial.mk_derivation as a linear equivalence.
Equations
- mv_polynomial.mk_derivation_equiv R = {to_fun := λ (D : derivation R (mv_polynomial σ R) A) (i : σ), ⇑D (mv_polynomial.X i), map_add' := _, map_smul' := _, inv_fun := mv_polynomial.mk_derivation R _inst_5, left_inv := _, right_inv := _}.symm