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

noncomputable 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.

@[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

@[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

theorem MvPolynomial.pUnitAlgEquiv_monomial (R : Type u) [CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R} : (pUnitAlgEquiv R) ((monomial d) r) = (Polynomial.monomial (d ())) r

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

noncomputable 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.

@[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

@[simp]

theorem MvPolynomial.mapEquiv_refl {R : Type u} (σ : Type u_1) [CommSemiring R] : mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl (MvPolynomial σ R)

@[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

@[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)

noncomputable 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.

@[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

@[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

@[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

@[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)

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

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

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

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

noncomputable 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.

@[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)

@[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

@[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)

noncomputable 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.

@[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

@[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)

@[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)

noncomputable 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.

@[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

@[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₁)

noncomputable 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.

@[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

theorem MvPolynomial.isEmptyRingEquiv_symm_toRingHom (R : Type u) {σ : Type u_1} [CommSemiring R] [IsEmpty σ] : (isEmptyRingEquiv R σ).symm.toRingHom = C

@[simp]

theorem MvPolynomial.isEmptyRingEquiv_symm_apply (R : Type u) {σ : Type u_1} [CommSemiring R] [IsEmpty σ] (r : R) : (isEmptyRingEquiv R σ).symm r = C r

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

noncomputable 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.

@[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

@[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

noncomputable 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.

@[simp]

theorem MvPolynomial.iterToSum_sumToIter (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (p : MvPolynomial (S₁ ⊕ S₂) R) : (iterToSum R S₁ S₂) ((sumToIter R S₁ S₂) p) = p

@[simp]

theorem MvPolynomial.sumToIter_iterToSum (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (p : MvPolynomial S₁ (MvPolynomial S₂ R)) : (sumToIter R S₁ S₂) ((iterToSum R S₁ S₂) p) = p

noncomputable 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.

@[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

@[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

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

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

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₁.

@[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

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

@[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)

noncomputable 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.

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

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

@[simp]

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)

@[simp]

theorem MvPolynomial.optionEquivLeft_X_none (R : Type u) (S₁ : Type v) [CommSemiring R] : (optionEquivLeft R S₁) (X none) = Polynomial.X

@[simp]

theorem MvPolynomial.optionEquivLeft_C (R : Type u) (S₁ : Type v) [CommSemiring R] (r : R) : (optionEquivLeft R S₁) (C r) = Polynomial.C (C r)

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)

@[simp]

theorem MvPolynomial.optionEquivLeft_symm_C_X (R : Type u) (S₁ : Type v) [CommSemiring R] (x : S₁) : (optionEquivLeft R S₁).symm (Polynomial.C (X x)) = X (some x)

@[simp]

theorem MvPolynomial.optionEquivLeft_symm_C_C (R : Type u) (S₁ : Type v) [CommSemiring R] (x : R) : (optionEquivLeft R S₁).symm (Polynomial.C (C x)) = C x

@[simp]

theorem MvPolynomial.optionEquivLeft_symm_X (R : Type u) (S₁ : Type v) [CommSemiring R] : (optionEquivLeft R S₁).symm Polynomial.X = X none

theorem MvPolynomial.optionEquivLeft_coeff_some_coeff_none (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

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

theorem MvPolynomial.mem_support_coeff_optionEquivLeft (R : Type u) {σ : Type u_1} [CommSemiring R] {f : MvPolynomial (Option σ) R} {i : ℕ} {m : σ →₀ ℕ} : m ∈ (((optionEquivLeft R σ) f).coeff i).support ↔ Finsupp.optionElim i m ∈ f.support

theorem MvPolynomial.support_optionEquivLeft (R : Type u) {σ : Type u_1} [CommSemiring R] (p : MvPolynomial (Option σ) R) : ((optionEquivLeft R σ) p).support = Finset.image (fun (m : Option σ →₀ ℕ) => m none) p.support

theorem MvPolynomial.nonempty_support_optionEquivLeft (R : Type u) {σ : Type u_1} [CommSemiring R] {f : MvPolynomial (Option σ) R} (h : f ≠ 0) : ((optionEquivLeft R σ) f).support.Nonempty

theorem MvPolynomial.degree_optionEquivLeft (R : Type u) {σ : Type u_1} [CommSemiring R] {f : MvPolynomial (Option σ) R} (h : f ≠ 0) : ((optionEquivLeft R σ) f).degree = ↑(degreeOf none f)

@[simp]

theorem MvPolynomial.natDegree_optionEquivLeft (R : Type u) {σ : Type u_1} [CommSemiring R] (p : MvPolynomial (Option σ) R) : ((optionEquivLeft R σ) p).natDegree = degreeOf none p

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

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

theorem MvPolynomial.optionEquivLeft_coeff_coeff (R : Type u) {σ : Type u_1} [CommSemiring R] (p : MvPolynomial (Option σ) R) (m : ℕ) (d : σ →₀ ℕ) : coeff d (((optionEquivLeft R σ) p).coeff m) = coeff (Finsupp.optionElim m d) p

noncomputable 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.

@[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

@[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

theorem MvPolynomial.optionEquivRight_X_some (R : Type u) (S₁ : Type v) [CommSemiring R] (x : S₁) : (optionEquivRight R S₁) (X (some x)) = X x

theorem MvPolynomial.optionEquivRight_X_none (R : Type u) (S₁ : Type v) [CommSemiring R] : (optionEquivRight R S₁) (X none) = C Polynomial.X

theorem MvPolynomial.optionEquivRight_C (R : Type u) (S₁ : Type v) [CommSemiring R] (r : R) : (optionEquivRight R S₁) (C r) = C (Polynomial.C r)

noncomputable 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.

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

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

theorem MvPolynomial.finSuccEquiv_comp_C_eq_C {R : Type u} [CommSemiring R] (n : ℕ) : (↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C) = C

theorem MvPolynomial.finSuccEquiv_X_zero {R : Type u} [CommSemiring R] {n : ℕ} : (finSuccEquiv R n) (X 0) = Polynomial.X

theorem MvPolynomial.finSuccEquiv_X_succ {R : Type u} [CommSemiring R] {n : ℕ} {j : Fin n} : (finSuccEquiv R n) (X j.succ) = Polynomial.C (X j)

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.

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

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)

theorem MvPolynomial.mem_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

@[deprecated MvPolynomial.mem_support_coeff_finSuccEquiv (since := "2025-11-28")]

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

Alias of MvPolynomial.mem_support_coeff_finSuccEquiv.

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 ith coefficient of finSuccEquiv applied to p, if this is nonzero.

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

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

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}

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

theorem MvPolynomial.nonempty_support_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : ((finSuccEquiv R n) f).support.Nonempty

@[deprecated MvPolynomial.nonempty_support_finSuccEquiv (since := "2025-11-28")]

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

Alias of MvPolynomial.nonempty_support_finSuccEquiv.

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)

theorem MvPolynomial.natDegree_finSuccEquiv {R : Type u} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) : ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

theorem MvPolynomial.degreeOf_eq_natDegree {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (a : σ) (p : MvPolynomial σ R) : degreeOf a p = ((optionEquivLeft R { b : σ // b ≠ a }) ((rename ⇑(Equiv.optionSubtypeNe a).symm) p)).natDegree

The MvPolynomial.degreeOf of a particular variable in a multivariate polynomial is equal to the Polynomial.natDegree of the single-variable polynomial obtained by treating the multivariable polynomial as a single variable polynomial over multivariable polynomials in the remaining variables

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

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.

@[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

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.

@[simp]

theorem Polynomial.toMvPolynomial_C {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) (r : R) : (toMvPolynomial i) (C r) = MvPolynomial.C r

@[simp]

theorem Polynomial.toMvPolynomial_X {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) : (toMvPolynomial i) X = MvPolynomial.X i

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

theorem Polynomial.toMvPolynomial_injective {R : Type u_1} {σ : Type u_3} [CommSemiring R] (i : σ) : Function.Injective ⇑(toMvPolynomial i)

@[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)

@[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

@[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)

@[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

@[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)

@[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