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.

noncomputable 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.

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) : (mkDerivationₗ R f) ((monomial s) r) = r • s.sum fun (i : σ) (k : ℕ) => (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) : (mkDerivationₗ R f) (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 : σ) : (mkDerivationₗ R f) (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 (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) : C a • D f = a • D f

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₁ D₂ : Derivation R (MvPolynomial σ R) A} {s : Set σ} (h : Set.EqOn (⇑D₁ ∘ X) (⇑D₂ ∘ X) s) {f : MvPolynomial σ R} (hf : f ∈ 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₁ D₂ : Derivation R (MvPolynomial σ R) A} {f : MvPolynomial σ R} (h : ∀ i ∈ f.vars, D₁ (X i) = D₂ (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 ∈ f.vars, D (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₁ D₂ : Derivation R (MvPolynomial σ R) A} (h : ∀ (i : σ), D₁ (X i) = D₂ (X i)) : D₁ = D₂

theorem MvPolynomial.derivation_ext_iff {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (MvPolynomial σ R) A] {D₁ D₂ : Derivation R (MvPolynomial σ R) A} : D₁ = D₂ ↔ ∀ (i : σ), D₁ (X i) = D₂ (X i)

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 ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)

noncomputable 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.

@[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 : σ) : (mkDerivation R f) (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) : (mkDerivation R f) ((monomial s) r) = r • s.sum fun (i : σ) (k : ℕ) => (monomial (s - Finsupp.single i 1)) ↑k • f i

noncomputable 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.