mathlib3 documentation

data.mv_polynomial.derivation

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) :

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
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) :
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) :
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 : σ) :
@[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) :
@[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) :
D₁ f = D₂ f

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)) :
D₁ f = D₂ f
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) :
D f = 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) :
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) :

The derivation on mv_polynomial σ R that takes value f i on X i.

Equations
@[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 : σ) :
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) :
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] :

mv_polynomial.mk_derivation as a linear equivalence.

Equations