Documentation

Mathlib.Algebra.MvPolynomial.Derivation

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

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 s.sum 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 : σ) :
    @[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) :
    MvPolynomial.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₁ : 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 : if.vars, 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 : if.vars, D (MvPolynomial.X i) = 0) :
    D f = 0
    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₁ : Derivation R (MvPolynomial σ R) A} {D₂ : Derivation R (MvPolynomial σ R) A} :
    D₁ = D₂ ∀ (i : σ), D₁ (MvPolynomial.X i) = D₂ (MvPolynomial.X i)
    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) :

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

    Equations
    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 : σ) :
      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 s.sum 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.
      Instances For