Polynomials supported by a set of variables #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

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

Tags #

variables, polynomial, vars

source

noncomputable def mv_polynomial.supported {σ : Type u_1} (R : Type u) [comm_semiring R] (s : set σ) :

subalgebra R (mv_polynomial σ R)

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

Equations

mv_polynomial.supported R s = algebra.adjoin R (mv_polynomial.X '' s)

source

theorem mv_polynomial.supported_eq_range_rename {σ : Type u_1} {R : Type u} [comm_semiring R] (s : set σ) :

mv_polynomial.supported R s = (mv_polynomial.rename coe).range

source

noncomputable def mv_polynomial.supported_equiv_mv_polynomial {σ : Type u_1} {R : Type u} [comm_semiring R] (s : set σ) :

↥(mv_polynomial.supported R s) ≃ₐ[R] mv_polynomial ↥s R

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

Equations

mv_polynomial.supported_equiv_mv_polynomial s = ((mv_polynomial.supported R s).equiv_of_eq (mv_polynomial.rename coe).range _).trans (alg_equiv.of_injective (mv_polynomial.rename coe) _).symm

source

@[simp]

theorem mv_polynomial.supported_equiv_mv_polynomial_symm_C {σ : Type u_1} {R : Type u} [comm_semiring R] (s : set σ) (x : R) :

⇑((mv_polynomial.supported_equiv_mv_polynomial s).symm) (⇑mv_polynomial.C x) = ⇑(algebra_map R ↥(mv_polynomial.supported R s)) x

source

@[simp]

theorem mv_polynomial.supported_equiv_mv_polynomial_symm_X {σ : Type u_1} {R : Type u} [comm_semiring R] (s : set σ) (i : ↥s) :

↑(⇑((mv_polynomial.supported_equiv_mv_polynomial s).symm) (mv_polynomial.X i)) = mv_polynomial.X ↑i

source

theorem mv_polynomial.mem_supported {σ : Type u_1} {R : Type u} [comm_semiring R] {p : mv_polynomial σ R} {s : set σ} :

p ∈ mv_polynomial.supported R s ↔ ↑(p.vars) ⊆ s

source

theorem mv_polynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} [comm_semiring R] {s : set σ} :

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

source

@[simp]

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

p ∈ mv_polynomial.supported R ↑(p.vars)

source

theorem mv_polynomial.supported_eq_adjoin_X {σ : Type u_1} {R : Type u} [comm_semiring R] (s : set σ) :

mv_polynomial.supported R s = algebra.adjoin R (mv_polynomial.X '' s)

source

@[simp]

theorem mv_polynomial.supported_univ {σ : Type u_1} {R : Type u} [comm_semiring R] :

mv_polynomial.supported R set.univ = ⊤

source

@[simp]

theorem mv_polynomial.supported_empty {σ : Type u_1} {R : Type u} [comm_semiring R] :

mv_polynomial.supported R ∅ = ⊥

source

theorem mv_polynomial.supported_mono {σ : Type u_1} {R : Type u} [comm_semiring R] {s t : set σ} (st : s ⊆ t) :

mv_polynomial.supported R s ≤ mv_polynomial.supported R t

source

@[simp]

theorem mv_polynomial.X_mem_supported {σ : Type u_1} {R : Type u} [comm_semiring R] {s : set σ} [nontrivial R] {i : σ} :

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

source

@[simp]

theorem mv_polynomial.supported_le_supported_iff {σ : Type u_1} {R : Type u} [comm_semiring R] {s t : set σ} [nontrivial R] :

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

source

theorem mv_polynomial.supported_strict_mono {σ : Type u_1} {R : Type u} [comm_semiring R] [nontrivial R] :

strict_mono (mv_polynomial.supported R)

source

theorem mv_polynomial.exists_restrict_to_vars {σ : Type u_1} {s : set σ} (R : Type u_2) [comm_ring R] {F : mv_polynomial σ ℤ} (hF : ↑(F.vars) ⊆ s) :

∃ (f : (↥s → R) → R), ∀ (x : σ → R), f (x ∘ coe) = ⇑(mv_polynomial.aeval x) F