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.

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.

    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