# Polynomials supported by a set of variables #

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

## Main definitions #

- `MvPolynomial.supported` : Given a set `s : Set σ`, `supported R s` is the subalgebra of `MvPolynomial σ R` consisting of polynomials whose set of variables is contained in `s`. This subalgebra is isomorphic to `MvPolynomial s R`.

## 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

- MvPolynomial.supported R s = Algebra.adjoin R (MvPolynomial.X '' s)

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

- One or more equations did not get rendered due to their size.

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