# 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

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

theorem
MvPolynomial.supported_eq_range_rename
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
(s : Set σ)
:

MvPolynomial.supported R s = (MvPolynomial.rename Subtype.val).range

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

↥(MvPolynomial.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

@[simp]

theorem
MvPolynomial.supportedEquivMvPolynomial_symm_C
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
(s : Set σ)
(x : R)
:

(MvPolynomial.supportedEquivMvPolynomial s).symm (MvPolynomial.C x) = (algebraMap R ↥(MvPolynomial.supported R s)) x

@[simp]

theorem
MvPolynomial.supportedEquivMvPolynomial_symm_X
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
(s : Set σ)
(i : ↑s)
:

↑((MvPolynomial.supportedEquivMvPolynomial s).symm (MvPolynomial.X i)) = MvPolynomial.X ↑i

theorem
MvPolynomial.mem_supported
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
{p : MvPolynomial σ R}
{s : Set σ}
:

p ∈ MvPolynomial.supported R s ↔ ↑p.vars ⊆ s

theorem
MvPolynomial.supported_eq_vars_subset
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
{s : Set σ}
:

↑(MvPolynomial.supported R s) = {p : MvPolynomial σ R | ↑p.vars ⊆ s}

@[simp]

theorem
MvPolynomial.mem_supported_vars
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
(p : MvPolynomial σ R)
:

p ∈ MvPolynomial.supported R ↑p.vars

theorem
MvPolynomial.supported_eq_adjoin_X
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
(s : Set σ)
:

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

@[simp]

theorem
MvPolynomial.supported_univ
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
:

MvPolynomial.supported R Set.univ = ⊤

@[simp]

theorem
MvPolynomial.supported_mono
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
{s : Set σ}
{t : Set σ}
(st : s ⊆ t)
:

@[simp]

theorem
MvPolynomial.X_mem_supported
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
{s : Set σ}
[Nontrivial R]
{i : σ}
:

MvPolynomial.X i ∈ MvPolynomial.supported R s ↔ i ∈ s

@[simp]

theorem
MvPolynomial.supported_le_supported_iff
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
{s : Set σ}
{t : Set σ}
[Nontrivial R]
:

MvPolynomial.supported R s ≤ MvPolynomial.supported R t ↔ s ⊆ t

theorem
MvPolynomial.supported_strictMono
{σ : Type u_1}
{R : Type u}
[CommSemiring R]
[Nontrivial R]
:

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) = (MvPolynomial.aeval x) F