Documentation

Mathlib.Algebra.MvPolynomial.Supported

Polynomials supported by a set of variables #

This file contains the definition and lemmas about MvPolynomial.supported.

Main definitions #

Tags #

variables, polynomial, vars

source
noncomputable def MvPolynomial.supported {σ : Type u_1} (R : Type u) [CommSemiring R] (s : Set σ) :
Subalgebra R (MvPolynomial σ R)

The set of polynomials whose variables are contained in s as a Subalgebra over R.

Equations
    Instances For
      source
      theorem MvPolynomial.supported_eq_range_rename {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :
      supported R s = (rename Subtype.val).range
      source
      noncomputable def MvPolynomial.supportedEquivMvPolynomial {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :
      ↥(supported R s) ≃ₐ[R] MvPolynomial (↑s) R

      The isomorphism between the subalgebra of polynomials supported by s and MvPolynomial s R.

      Equations
        Instances For
          source
          @[simp]
          theorem MvPolynomial.supportedEquivMvPolynomial_symm_C {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) (x : R) :
          (supportedEquivMvPolynomial s).symm (C x) = (algebraMap R ↥(supported R s)) x
          source
          @[simp]
          theorem MvPolynomial.supportedEquivMvPolynomial_symm_X {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) (i : ↑s) :
          ↑((supportedEquivMvPolynomial s).symm (X i)) = X ↑i
          source
          theorem MvPolynomial.mem_supported {σ : Type u_1} {R : Type u} [CommSemiring R] {p : MvPolynomial σ R} {s : Set σ} :
          p ∈ supported R s ↔ ↑p.vars ⊆ s
          source
          theorem MvPolynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} :
          ↑(supported R s) = {p : MvPolynomial σ R | ↑p.vars ⊆ s}
          source
          @[simp]
          theorem MvPolynomial.mem_supported_vars {σ : Type u_1} {R : Type u} [CommSemiring R] (p : MvPolynomial σ R) :
          p ∈ supported R ↑p.vars
          source
          theorem MvPolynomial.supported_eq_adjoin_X {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :
          supported R s = Algebra.adjoin R (X '' s)
          source
          @[simp]
          theorem MvPolynomial.supported_univ {σ : Type u_1} {R : Type u} [CommSemiring R] :
          supported R Set.univ = ⊤
          source
          @[simp]
          theorem MvPolynomial.supported_empty {σ : Type u_1} {R : Type u} [CommSemiring R] :
          supported R ∅ = ⊥
          source
          theorem MvPolynomial.supported_mono {σ : Type u_1} {R : Type u} [CommSemiring R] {s t : Set σ} (st : s ⊆ t) :
          supported R s ≤ supported R t
          source
          @[simp]
          theorem MvPolynomial.X_mem_supported {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} [Nontrivial R] {i : σ} :
          X i ∈ supported R s ↔ i ∈ s
          source
          @[simp]
          theorem MvPolynomial.supported_le_supported_iff {σ : Type u_1} {R : Type u} [CommSemiring R] {s t : Set σ} [Nontrivial R] :
          supported R s ≤ supported R t ↔ s ⊆ t
          source
          theorem MvPolynomial.supported_strictMono {σ : Type u_1} {R : Type u} [CommSemiring R] [Nontrivial R] :
          StrictMono (supported R)
          source
          theorem MvPolynomial.exists_restrict_to_vars {σ : Type u_1} {s : Set σ} (R : Type u_2) [CommRing R] {F : MvPolynomial σ ℤ} (hF : ↑F.vars ⊆ s) :
          ∃ (f : (↑s → R) → R), ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F