# Equivalences between polynomial rings #

This file establishes a number of equivalences between polynomial rings, based on equivalences between the underlying types.

## Notation #

As in other polynomial files, we typically use the notation:

- `σ : Type*` (indexing the variables)

- `R : Type*` `[CommSemiring R]` (the coefficients)

- `s : σ →₀ ℕ`, a function from `σ` to `ℕ` which is zero away from a finite set. This will give rise to a monomial in `MvPolynomial σ R` which mathematicians might call `X^s`

- `a : R`

- `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians

- `p : MvPolynomial σ R`

## Tags #

equivalence, isomorphism, morphism, ring hom, hom

source
def MvPolynomial.pUnitAlgEquiv (R : Type u) [CommSemiring R] :
MvPolynomial PUnit.{u_2 + 1} R ≃ₐ[R] Polynomial R

The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.

Equations

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

Instances For

source
@[simp]
theorem MvPolynomial.pUnitAlgEquiv_symm_apply (R : Type u) [CommSemiring R] (p : Polynomial R) :
(pUnitAlgEquiv R).symm p = Polynomial.eval₂ C (X PUnit.unit) p
source
@[simp]
theorem MvPolynomial.pUnitAlgEquiv_apply (R : Type u) [CommSemiring R] (p : MvPolynomial PUnit.{u_2 + 1} R) :
(pUnitAlgEquiv R) p = eval₂ Polynomial.C (fun (x : PUnit.{u_2 + 1}) => Polynomial.X) p
source
theorem MvPolynomial.pUnitAlgEquiv_monomial (R : Type u) [CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R} :
(pUnitAlgEquiv R) ((monomial d) r) = (Polynomial.monomial (d ())) r
source
theorem MvPolynomial.pUnitAlgEquiv_symm_monomial (R : Type u) [CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R} :
(pUnitAlgEquiv R).symm ((Polynomial.monomial (d ())) r) = (monomial d) r
source
def MvPolynomial.mapEquiv {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :
MvPolynomial σ S₁ ≃+* MvPolynomial σ S₂

If `e : A ≃+* B` is an isomorphism of rings, then so is `map e`.

Equations

- MvPolynomial.mapEquiv σ e = { toFun := ⇑(MvPolynomial.map ↑e), invFun := ⇑(MvPolynomial.map ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.mapEquiv_apply {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) (a : MvPolynomial σ S₁) :
(mapEquiv σ e) a = (map ↑e) a
source
@[simp]
theorem MvPolynomial.mapEquiv_refl {R : Type u} (σ : Type u_1) [CommSemiring R] :
mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl (MvPolynomial σ R)
source
@[simp]
theorem MvPolynomial.mapEquiv_symm {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :
(mapEquiv σ e).symm = mapEquiv σ e.symm
source
@[simp]
theorem MvPolynomial.mapEquiv_trans {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] [CommSemiring S₃] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :
(mapEquiv σ e).trans (mapEquiv σ f) = mapEquiv σ (e.trans f)
source
def MvPolynomial.mapAlgEquiv {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
MvPolynomial σ A₁ ≃ₐ[R] MvPolynomial σ A₂

If `e : A ≃ₐ[R] B` is an isomorphism of `R`-algebras, then so is `map e`.

Equations

- MvPolynomial.mapAlgEquiv σ e = { toFun := ⇑(MvPolynomial.map ↑e), invFun := (MvPolynomial.mapEquiv σ ↑e).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.mapAlgEquiv_apply {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : MvPolynomial σ A₁) :
(mapAlgEquiv σ e) a = (map ↑e) a
source
@[simp]
theorem MvPolynomial.mapAlgEquiv_refl {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} [CommSemiring A₁] [Algebra R A₁] :
mapAlgEquiv σ AlgEquiv.refl = AlgEquiv.refl
source
@[simp]
theorem MvPolynomial.mapAlgEquiv_symm {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
(mapAlgEquiv σ e).symm = mapAlgEquiv σ e.symm
source
@[simp]
theorem MvPolynomial.mapAlgEquiv_trans {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [CommSemiring A₁] [CommSemiring A₂] [CommSemiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :
(mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f)
source
theorem MvPolynomial.eval₂_pUnitAlgEquiv_symm {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : Polynomial R} {φ : R →+* S} {a : Unit → S} :
eval₂ φ a ((pUnitAlgEquiv R).symm f) = Polynomial.eval₂ φ (a ()) f
source
theorem MvPolynomial.eval₂_const_pUnitAlgEquiv_symm {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : Polynomial R} {φ : R →+* S} {a : S} :
eval₂ φ (fun (x : PUnit.{1}) => a) ((pUnitAlgEquiv R).symm f) = Polynomial.eval₂ φ a f
source
theorem MvPolynomial.eval₂_pUnitAlgEquiv {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : MvPolynomial PUnit.{u_4 + 1} R} {φ : R →+* S} {a : PUnit.{u_4 + 1} → S} :
Polynomial.eval₂ φ (a default) ((pUnitAlgEquiv R) f) = eval₂ φ a f
source
theorem MvPolynomial.eval₂_const_pUnitAlgEquiv {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : MvPolynomial PUnit.{u_4 + 1} R} {φ : R →+* S} {a : S} :
Polynomial.eval₂ φ a ((pUnitAlgEquiv R) f) = eval₂ φ (fun (x : PUnit.{u_4 + 1}) => a) f
source
def MvPolynomial.sumToIter (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
MvPolynomial (S₁ ⊕ S₂) R →+* MvPolynomial S₁ (MvPolynomial S₂ R)

The function from multivariable polynomials in a sum of two types, to multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.

See `sumRingEquiv` for the ring isomorphism.

Equations

- MvPolynomial.sumToIter R S₁ S₂ = MvPolynomial.eval₂Hom (MvPolynomial.C.comp MvPolynomial.C) fun (bc : S₁ ⊕ S₂) => Sum.recOn bc MvPolynomial.X (⇑MvPolynomial.C ∘ MvPolynomial.X)

Instances For

source
@[simp]
theorem MvPolynomial.sumToIter_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (a : R) :
(sumToIter R S₁ S₂) (C a) = C (C a)
source
@[simp]
theorem MvPolynomial.sumToIter_Xl (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (b : S₁) :
(sumToIter R S₁ S₂) (X (Sum.inl b)) = X b
source
@[simp]
theorem MvPolynomial.sumToIter_Xr (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (c : S₂) :
(sumToIter R S₁ S₂) (X (Sum.inr c)) = C (X c)
source
def MvPolynomial.iterToSum (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
MvPolynomial S₁ (MvPolynomial S₂ R) →+* MvPolynomial (S₁ ⊕ S₂) R

The function from multivariable polynomials in one type, with coefficients in multivariable polynomials in another type, to multivariable polynomials in the sum of the two types.

See `sumRingEquiv` for the ring isomorphism.

Equations

- MvPolynomial.iterToSum R S₁ S₂ = MvPolynomial.eval₂Hom (MvPolynomial.eval₂Hom MvPolynomial.C (MvPolynomial.X ∘ Sum.inr)) (MvPolynomial.X ∘ Sum.inl)

Instances For

source
@[simp]
theorem MvPolynomial.iterToSum_C_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (a : R) :
(iterToSum R S₁ S₂) (C (C a)) = C a
source
@[simp]
theorem MvPolynomial.iterToSum_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (b : S₁) :
(iterToSum R S₁ S₂) (X b) = X (Sum.inl b)
source
@[simp]
theorem MvPolynomial.iterToSum_C_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (c : S₂) :
(iterToSum R S₁ S₂) (C (X c)) = X (Sum.inr c)
source
def MvPolynomial.isEmptyAlgEquiv (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] :
MvPolynomial σ R ≃ₐ[R] R

The algebra isomorphism between multivariable polynomials in no variables and the ground ring.

Equations

- MvPolynomial.isEmptyAlgEquiv R σ = AlgEquiv.ofAlgHom (MvPolynomial.aeval fun (a : σ) => isEmptyElim a) (Algebra.ofId R (MvPolynomial σ R)) ⋯ ⋯

Instances For

source
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_apply (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] (a : MvPolynomial σ R) :
(isEmptyAlgEquiv R σ) a = (eval fun (a : σ) => isEmptyElim a) a
source
@[simp]
theorem MvPolynomial.aeval_injective_iff_of_isEmpty {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [IsEmpty σ] [CommSemiring S₁] [Algebra R S₁] {f : σ → S₁} :
Function.Injective ⇑(aeval f) ↔ Function.Injective ⇑(algebraMap R S₁)
source
def MvPolynomial.isEmptyRingEquiv (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] :
MvPolynomial σ R ≃+* R

The ring isomorphism between multivariable polynomials in no variables and the ground ring.

Equations

- MvPolynomial.isEmptyRingEquiv R σ = (MvPolynomial.isEmptyAlgEquiv R σ).toRingEquiv

Instances For

source
@[simp]
theorem MvPolynomial.isEmptyRingEquiv_apply (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] (a : MvPolynomial σ R) :
(isEmptyRingEquiv R σ) a = (eval fun (a : σ) => isEmptyElim a) a
source
theorem MvPolynomial.isEmptyRingEquiv_symm_toRingHom (R : Type u) {σ : Type u_1} [CommSemiring R] [IsEmpty σ] :
(isEmptyRingEquiv R σ).symm.toRingHom = C
source
@[simp]
theorem MvPolynomial.isEmptyRingEquiv_symm_apply (R : Type u) {σ : Type u_1} [CommSemiring R] [IsEmpty σ] (r : R) :
(isEmptyRingEquiv R σ).symm r = C r
source
theorem MvPolynomial.isEmptyRingEquiv_eq_coeff_zero {σ : Type u_2} {R : Type u_3} [CommSemiring R] [IsEmpty σ] {x : MvPolynomial σ R} :
(isEmptyRingEquiv R σ) x = coeff 0 x
source
def MvPolynomial.mvPolynomialEquivMvPolynomial (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [CommSemiring R] [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp C = C) (hfgX : ∀ (n : S₂), f (g (X n)) = X n) (hgfC : (g.comp f).comp C = C) (hgfX : ∀ (n : S₁), g (f (X n)) = X n) :
MvPolynomial S₁ R ≃+* MvPolynomial S₂ S₃

A helper function for `sumRingEquiv`.

Equations

- MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [CommSemiring R] [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp C = C) (hfgX : ∀ (n : S₂), f (g (X n)) = X n) (hgfC : (g.comp f).comp C = C) (hgfX : ∀ (n : S₁), g (f (X n)) = X n) (a : MvPolynomial S₂ S₃) :
(mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX).symm a = g a
source
@[simp]
theorem MvPolynomial.mvPolynomialEquivMvPolynomial_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [CommSemiring R] [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp C = C) (hfgX : ∀ (n : S₂), f (g (X n)) = X n) (hgfC : (g.comp f).comp C = C) (hgfX : ∀ (n : S₁), g (f (X n)) = X n) (a : MvPolynomial S₁ R) :
(mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) a = f a
source
def MvPolynomial.sumRingEquiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)

The ring isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.

Equations

- MvPolynomial.sumRingEquiv R S₁ S₂ = MvPolynomial.mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) S₁ (MvPolynomial S₂ R) (MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.iterToSum R S₁ S₂) ⋯ ⋯ ⋯ ⋯

Instances For

source
def MvPolynomial.sumAlgEquiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
MvPolynomial (S₁ ⊕ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R)

The algebra isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.

Equations

- MvPolynomial.sumAlgEquiv R S₁ S₂ = { toEquiv := (MvPolynomial.sumRingEquiv R S₁ S₂).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.sumAlgEquiv_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (a : MvPolynomial S₁ (MvPolynomial S₂ R)) :
(sumAlgEquiv R S₁ S₂).symm a = (iterToSum R S₁ S₂) a
source
@[simp]
theorem MvPolynomial.sumAlgEquiv_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (a : MvPolynomial (S₁ ⊕ S₂) R) :
(sumAlgEquiv R S₁ S₂) a = (sumToIter R S₁ S₂) a
source
theorem MvPolynomial.sumAlgEquiv_comp_rename_inr (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
(↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr) = IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))
source
theorem MvPolynomial.sumAlgEquiv_comp_rename_inl (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
(↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl) = mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))
source
noncomputable def MvPolynomial.commAlgEquiv (R : Type u_2) (S₁ : Type u_3) (S₂ : Type u_4) [CommSemiring R] :
MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R)

The algebra isomorphism between multivariable polynomials in variables `S₁` of multivariable polynomials in variables `S₂` and multivariable polynomials in variables `S₂` of multivariable polynomials in variables `S₁`.

Equations

- MvPolynomial.commAlgEquiv R S₁ S₂ = (MvPolynomial.sumAlgEquiv R S₁ S₂).symm.trans ((MvPolynomial.renameEquiv R (Equiv.sumComm S₁ S₂)).trans (MvPolynomial.sumAlgEquiv R S₂ S₁))

Instances For

source
@[simp]
theorem MvPolynomial.commAlgEquiv_C {R : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [CommSemiring R] (p : MvPolynomial S₂ R) :
(commAlgEquiv R S₁ S₂) (C p) = (map C) p
source
theorem MvPolynomial.commAlgEquiv_C_X {R : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [CommSemiring R] (i : S₂) :
(commAlgEquiv R S₁ S₂) (C (X i)) = X i
source
@[simp]
theorem MvPolynomial.commAlgEquiv_X {R : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [CommSemiring R] (i : S₁) :
(commAlgEquiv R S₁ S₂) (X i) = C (X i)
source
def MvPolynomial.optionEquivLeft (R : Type u) (S₁ : Type v) [CommSemiring R] :
MvPolynomial (Option S₁) R ≃ₐ[R] Polynomial (MvPolynomial S₁ R)

The algebra isomorphism between multivariable polynomials in `Option S₁` and polynomials with coefficients in `MvPolynomial S₁ R`.

Equations

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

Instances For

source
theorem MvPolynomial.optionEquivLeft_symm_apply (R : Type u) (S₁ : Type v) [CommSemiring R] (a : Polynomial (MvPolynomial S₁ R)) :
(optionEquivLeft R S₁).symm a = (Polynomial.aevalTower (rename some) (X none)) a
source
theorem MvPolynomial.optionEquivLeft_apply (R : Type u) (S₁ : Type v) [CommSemiring R] (a : MvPolynomial (Option S₁) R) :
(optionEquivLeft R S₁) a = (aeval fun (o : Option S₁) => o.elim Polynomial.X fun (s : S₁) => Polynomial.C (X s)) a
source
theorem MvPolynomial.optionEquivLeft_X_some (R : Type u) (S₁ : Type v) [CommSemiring R] (x : S₁) :
(optionEquivLeft R S₁) (X (some x)) = Polynomial.C (X x)
source
theorem MvPolynomial.optionEquivLeft_X_none (R : Type u) (S₁ : Type v) [CommSemiring R] :
(optionEquivLeft R S₁) (X none) = Polynomial.X
source
theorem MvPolynomial.optionEquivLeft_C (R : Type u) (S₁ : Type v) [CommSemiring R] (r : R) :
(optionEquivLeft R S₁) (C r) = Polynomial.C (C r)
source
theorem MvPolynomial.optionEquivLeft_monomial (R : Type u) (S₁ : Type v) [CommSemiring R] (m : Option S₁ →₀ ℕ) (r : R) :
(optionEquivLeft R S₁) ((monomial m) r) = (Polynomial.monomial (m none)) ((monomial m.some) r)
source
theorem MvPolynomial.optionEquivLeft_coeff_coeff (R : Type u) (S₁ : Type v) [CommSemiring R] (n : Option S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R) :
coeff n.some (((optionEquivLeft R S₁) f).coeff (n none)) = coeff n f

The coefficient of `n.some` in the `n none`-th coefficient of `optionEquivLeft R S₁ f` equals the coefficient of `n` in `f`

source
theorem MvPolynomial.optionEquivLeft_elim_eval (R : Type u) (S₁ : Type v) [CommSemiring R] (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R) :
(eval fun (x : Option S₁) => x.elim y s) f = Polynomial.eval y (Polynomial.map (eval s) ((optionEquivLeft R S₁) f))
source
@[simp]
theorem MvPolynomial.natDegree_optionEquivLeft (R : Type u) (S₁ : Type v) [CommSemiring R] (p : MvPolynomial (Option S₁) R) :
((optionEquivLeft R S₁) p).natDegree = degreeOf none p
source
theorem MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le (R : Type u) (S₁ : Type v) [CommSemiring R] (p : MvPolynomial (Option S₁) R) (i : ℕ) (hi : i ≤ p.totalDegree) :
(((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree
source
theorem MvPolynomial.totalDegree_coeff_optionEquivLeft_le (R : Type u) (S₁ : Type v) [CommSemiring R] (p : MvPolynomial (Option S₁) R) (i : ℕ) :
(((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree
source
def MvPolynomial.optionEquivRight (R : Type u) (S₁ : Type v) [CommSemiring R] :
MvPolynomial (Option S₁) R ≃ₐ[R] MvPolynomial S₁ (Polynomial R)

The algebra isomorphism between multivariable polynomials in `Option S₁` and multivariable polynomials with coefficients in polynomials.

Equations

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

Instances For

source
@[simp]
theorem MvPolynomial.optionEquivRight_symm_apply (R : Type u) (S₁ : Type v) [CommSemiring R] (a : MvPolynomial S₁ (Polynomial R)) :
(optionEquivRight R S₁).symm a = (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) => X (some i)) a
source
@[simp]
theorem MvPolynomial.optionEquivRight_apply (R : Type u) (S₁ : Type v) [CommSemiring R] (a : MvPolynomial (Option S₁) R) :
(optionEquivRight R S₁) a = (aeval fun (o : Option S₁) => o.elim (C Polynomial.X) X) a
source
theorem MvPolynomial.optionEquivRight_X_some (R : Type u) (S₁ : Type v) [CommSemiring R] (x : S₁) :
(optionEquivRight R S₁) (X (some x)) = X x
source
theorem MvPolynomial.optionEquivRight_X_none (R : Type u) (S₁ : Type v) [CommSemiring R] :
(optionEquivRight R S₁) (X none) = C Polynomial.X
source
theorem MvPolynomial.optionEquivRight_C (R : Type u) (S₁ : Type v) [CommSemiring R] (r : R) :
(optionEquivRight R S₁) (C r) = C (Polynomial.C r)
source
def MvPolynomial.finSuccEquiv (R : Type u) [CommSemiring R] (n : ℕ) :
MvPolynomial (Fin (n + 1)) R ≃ₐ[R] Polynomial (MvPolynomial (Fin n) R)

The algebra isomorphism between multivariable polynomials in `Fin (n + 1)` and polynomials over multivariable polynomials in `Fin n`.

Equations

- MvPolynomial.finSuccEquiv R n = (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivLeft R (Fin n))

Instances For

source
theorem MvPolynomial.finSuccEquiv_eq (R : Type u) [CommSemiring R] (n : ℕ) :
↑(finSuccEquiv R n) = eval₂Hom (Polynomial.C.comp C) fun (i : Fin (n + 1)) => Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C (X k)) i
source
theorem MvPolynomial.finSuccEquiv_apply (R : Type u) [CommSemiring R] (n : ℕ) (p : MvPolynomial (Fin (n + 1)) R) :
(finSuccEquiv R n) p = (eval₂Hom (Polynomial.C.comp C) fun (i : Fin (n + 1)) => Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C (X k)) i) p
source
theorem MvPolynomial.finSuccEquiv_comp_C_eq_C {R : Type u} [CommSemiring R] (n : ℕ) :
(↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C) = C
source
theorem MvPolynomial.finSuccEquiv_X_zero {R : Type u} [CommSemiring R] {n : ℕ} :
(finSuccEquiv R n) (X 0) = Polynomial.X
source
theorem MvPolynomial.finSuccEquiv_X_succ {R : Type u} [CommSemiring R] {n : ℕ} {j : Fin n} :
(finSuccEquiv R n) (X j.succ) = Polynomial.C (X j)
source
theorem MvPolynomial.finSuccEquiv_coeff_coeff {R : Type u} [CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) :
coeff m (((finSuccEquiv R n) f).coeff i) = coeff (Finsupp.cons i m) f

The coefficient of `m` in the `i`-th coefficient of `finSuccEquiv R n f` equals the coefficient of `Finsupp.cons i m` in `f`.

source
theorem MvPolynomial.eval_eq_eval_mv_eval' {R : Type u} [CommSemiring R] {n : ℕ} (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) :
(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))
source
theorem MvPolynomial.coeff_eval_eq_eval_coeff {R : Type u} (S₁ : Type v) [CommSemiring R] (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R)) (i : ℕ) :
(Polynomial.map (eval s') f).coeff i = (eval s') (f.coeff i)
source
theorem MvPolynomial.support_coeff_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ} :
m ∈ (((finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i m ∈ f.support
source
theorem MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le {R : Type u} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) (hi : ((finSuccEquiv R n) f).coeff i ≠ 0) :
(((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

The `totalDegree` of a multivariable polynomial `p` is at least `i` more than the `totalDegree` of the `i`th coefficient of `finSuccEquiv` applied to `p`, if this is nonzero.

source
theorem MvPolynomial.support_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) :
((finSuccEquiv R n) f).support = Finset.image (fun (m : Fin (n + 1) →₀ ℕ) => m 0) f.support
source
theorem MvPolynomial.mem_support_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {x : ℕ} :
x ∈ ((finSuccEquiv R n) f).support ↔ x ∈ (fun (m : Fin (n + 1) →₀ ℕ) => m 0) '' ↑f.support
source
theorem MvPolynomial.image_support_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} :
Finset.image (Finsupp.cons i) (((finSuccEquiv R n) f).coeff i).support = {m ∈ f.support | m 0 = i}
source
theorem MvPolynomial.mem_image_support_coeff_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin (n + 1) →₀ ℕ} :
x ∈ Finsupp.cons i '' ↑(((finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i
source
theorem MvPolynomial.mem_support_coeff_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin n →₀ ℕ} :
x ∈ (((finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i x ∈ f.support
source
theorem MvPolynomial.support_finSuccEquiv_nonempty {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
((finSuccEquiv R n) f).support.Nonempty
source
theorem MvPolynomial.degree_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)
source
theorem MvPolynomial.natDegree_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) :
((finSuccEquiv R n) f).natDegree = degreeOf 0 f
source
theorem MvPolynomial.degreeOf_coeff_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) :
degreeOf j (((finSuccEquiv R n) p).coeff i) ≤ degreeOf j.succ p
source
theorem MvPolynomial.finSuccEquiv_rename_finSuccEquiv {R : Type u} {σ : Type u_1} [CommSemiring R] {n : ℕ} (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) :
(finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) = Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`, and suppose that `σ ≃ Fin n`. Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by

1. renaming the variables via `Option σ ≃ Fin (n+1)`, and then singling out the `0`-th variable via `MvPolynomial.finSuccEquiv`;
2. first viewing it as polynomial over `MvPolynomial σ R` via `MvPolynomial.optionEquivLeft`, and then renaming the variables.

This lemma shows that both constructions are the same.

source
@[simp]
theorem MvPolynomial.rename_polynomial_aeval_X (R : Type u) [CommSemiring R] {σ : Type u_2} {τ : Type u_3} (f : σ → τ) (i : σ) (p : Polynomial R) :
(rename f) ((Polynomial.aeval (X i)) p) = (Polynomial.aeval (X (f i))) p
source
noncomputable def Polynomial.toMvPolynomial {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) :
Polynomial R →ₐ[R] MvPolynomial σ R

The embedding of `R[X]` into `R[Xᵢ]` as an `R`-algebra homomorphism.

Equations

- Polynomial.toMvPolynomial i = Polynomial.aeval (MvPolynomial.X i)

Instances For

source
@[simp]
theorem Polynomial.toMvPolynomial_C {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) (r : R) :
(toMvPolynomial i) (C r) = MvPolynomial.C r
source
@[simp]
theorem Polynomial.toMvPolynomial_X {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) :
(toMvPolynomial i) X = MvPolynomial.X i
source
theorem Polynomial.toMvPolynomial_eq_rename_comp {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) :
toMvPolynomial i = (MvPolynomial.rename fun (x : Unit) => i).comp ↑(MvPolynomial.pUnitAlgEquiv R).symm
source
theorem Polynomial.toMvPolynomial_injective {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) :
Function.Injective ⇑(toMvPolynomial i)
source
@[simp]
theorem MvPolynomial.eval_comp_toMvPolynomial {R : Type u_1} {σ : Type u_3} [CommSemiring R] (f : σ → R) (i : σ) :
(eval f).comp ↑(Polynomial.toMvPolynomial i) = Polynomial.evalRingHom (f i)
source
@[simp]
theorem MvPolynomial.eval_toMvPolynomial {R : Type u_1} {σ : Type u_3} [CommSemiring R] (f : σ → R) (i : σ) (p : Polynomial R) :
(eval f) ((Polynomial.toMvPolynomial i) p) = Polynomial.eval (f i) p
source
@[simp]
theorem MvPolynomial.aeval_comp_toMvPolynomial {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] (f : σ → S) (i : σ) :
(aeval f).comp (Polynomial.toMvPolynomial i) = Polynomial.aeval (f i)
source
@[simp]
theorem MvPolynomial.aeval_toMvPolynomial {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] (f : σ → S) (i : σ) (p : Polynomial R) :
(aeval f) ((Polynomial.toMvPolynomial i) p) = (Polynomial.aeval (f i)) p
source
@[simp]
theorem MvPolynomial.rename_comp_toMvPolynomial {R : Type u_1} {σ : Type u_3} {τ : Type u_4} [CommSemiring R] (f : σ → τ) (a : σ) :
(rename f).comp (Polynomial.toMvPolynomial a) = Polynomial.toMvPolynomial (f a)
source
@[simp]
theorem MvPolynomial.rename_toMvPolynomial {R : Type u_1} {σ : Type u_3} {τ : Type u_4} [CommSemiring R] (f : σ → τ) (a : σ) (p : Polynomial R) :
(rename f) ((Polynomial.toMvPolynomial a) p) = (Polynomial.toMvPolynomial (f a)) p