# 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

@[simp]
theorem MvPolynomial.pUnitAlgEquiv_symm_apply (R : Type u) [] (p : ) :
.symm p = Polynomial.eval₂ MvPolynomial.C p
@[simp]
theorem MvPolynomial.pUnitAlgEquiv_apply (R : Type u) [] (p : ) :
= MvPolynomial.eval₂ Polynomial.C (fun (x : PUnit.{u_2 + 1} ) => Polynomial.X) p

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
@[simp]
theorem MvPolynomial.mapEquiv_apply {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [] [] (e : S₁ ≃+* S₂) (a : MvPolynomial σ S₁) :
a = (MvPolynomial.map e) a
def MvPolynomial.mapEquiv {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [] [] (e : S₁ ≃+* S₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MvPolynomial.mapEquiv_refl {R : Type u} (σ : Type u_1) [] :
@[simp]
theorem MvPolynomial.mapEquiv_symm {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [] [] (e : S₁ ≃+* S₂) :
.symm = MvPolynomial.mapEquiv σ e.symm
@[simp]
theorem MvPolynomial.mapEquiv_trans {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} (σ : Type u_1) [] [] [] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :
.trans = MvPolynomial.mapEquiv σ (e.trans f)
@[simp]
theorem MvPolynomial.mapAlgEquiv_apply {R : Type u} (σ : Type u_1) [] {A₁ : Type u_2} {A₂ : Type u_3} [] [] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : MvPolynomial σ A₁) :
a = (MvPolynomial.map e) a
def MvPolynomial.mapAlgEquiv {R : Type u} (σ : Type u_1) [] {A₁ : Type u_2} {A₂ : Type u_3} [] [] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MvPolynomial.mapAlgEquiv_refl {R : Type u} (σ : Type u_1) [] {A₁ : Type u_2} [] [Algebra R A₁] :
MvPolynomial.mapAlgEquiv σ AlgEquiv.refl = AlgEquiv.refl
@[simp]
theorem MvPolynomial.mapAlgEquiv_symm {R : Type u} (σ : Type u_1) [] {A₁ : Type u_2} {A₂ : Type u_3} [] [] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
.symm = MvPolynomial.mapAlgEquiv σ e.symm
@[simp]
theorem MvPolynomial.mapAlgEquiv_trans {R : Type u} (σ : Type u_1) [] {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [] [] [] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :
.trans = MvPolynomial.mapAlgEquiv σ (e.trans f)
def MvPolynomial.sumToIter (R : Type u) (S₁ : Type v) (S₂ : Type w) [] :
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
Instances For
@[simp]
theorem MvPolynomial.sumToIter_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (a : R) :
(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.C a) = MvPolynomial.C (MvPolynomial.C a)
@[simp]
theorem MvPolynomial.sumToIter_Xl (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (b : S₁) :
@[simp]
theorem MvPolynomial.sumToIter_Xr (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (c : S₂) :
(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.X (Sum.inr c)) = MvPolynomial.C
def MvPolynomial.iterToSum (R : Type u) (S₁ : Type v) (S₂ : Type w) [] :
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
Instances For
@[simp]
theorem MvPolynomial.iterToSum_C_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (a : R) :
(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.C a)) = MvPolynomial.C a
@[simp]
theorem MvPolynomial.iterToSum_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (b : S₁) :
(MvPolynomial.iterToSum R S₁ S₂) =
@[simp]
theorem MvPolynomial.iterToSum_C_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (c : S₂) :
(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C ) =
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_symm_apply_support (R : Type u) (σ : Type u_1) [] [he : ] (a : R) :
(.symm a).support = if a = 0 then else {0}
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_apply (R : Type u) (σ : Type u_1) [] [he : ] (a : ) :
a = (MvPolynomial.aeval fun (a : σ) => he.elim a) a
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_symm_apply_toFun (R : Type u) (σ : Type u_1) [] [he : ] (a : R) (j : σ →₀ ) :
(.symm a) j = Pi.single 0 a j
def MvPolynomial.isEmptyAlgEquiv (R : Type u) (σ : Type u_1) [] [he : ] :

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

Equations
Instances For
@[simp]
theorem MvPolynomial.isEmptyRingEquiv_symm_apply_toFun (R : Type u) (σ : Type u_1) [] [] (a : R) (j : σ →₀ ) :
(.symm a) j = Pi.single 0 a j
@[simp]
theorem MvPolynomial.isEmptyRingEquiv_symm_apply_support (R : Type u) (σ : Type u_1) [] [] (a : R) :
(.symm a).support = if a = 0 then else {0}
@[simp]
theorem MvPolynomial.isEmptyRingEquiv_apply (R : Type u) (σ : Type u_1) [] [] (a : ) :
= (MvPolynomial.aeval fun (a : σ) => inst✝.elim a) a
def MvPolynomial.isEmptyRingEquiv (R : Type u) (σ : Type u_1) [] [] :

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

Equations
• = .toRingEquiv
Instances For
@[simp]
theorem MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [] [] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g ) = ) (hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f ) = ) (a : MvPolynomial S₂ S₃) :
(MvPolynomial.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) [] [] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g ) = ) (hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f ) = ) (a : MvPolynomial S₁ R) :
(MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) a = f a
def MvPolynomial.mvPolynomialEquivMvPolynomial (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [] [] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g ) = ) (hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f ) = ) :

A helper function for sumRingEquiv.

Equations
Instances For
def MvPolynomial.sumRingEquiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [] :
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
Instances For
@[simp]
theorem MvPolynomial.sumAlgEquiv_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (a : MvPolynomial (S₁ S₂) R) :
(MvPolynomial.sumAlgEquiv R S₁ S₂) a = (MvPolynomial.sumToIter R S₁ S₂) a
@[simp]
theorem MvPolynomial.sumAlgEquiv_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (a : MvPolynomial S₁ (MvPolynomial S₂ R)) :
(MvPolynomial.sumAlgEquiv R S₁ S₂).symm a = (MvPolynomial.iterToSum R S₁ S₂) a
def MvPolynomial.sumAlgEquiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [] :
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
• = let __src := ; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
@[simp]
theorem MvPolynomial.optionEquivLeft_apply (R : Type u) (S₁ : Type v) [] (a : MvPolynomial (Option S₁) R) :
a = (MvPolynomial.aeval fun (o : Option S₁) => o.elim Polynomial.X fun (s : S₁) => Polynomial.C ) a

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
theorem MvPolynomial.optionEquivLeft_X_some (R : Type u) (S₁ : Type v) [] (x : S₁) :
(MvPolynomial.X (some x)) = Polynomial.C
theorem MvPolynomial.optionEquivLeft_X_none (R : Type u) (S₁ : Type v) [] :
(MvPolynomial.X none) = Polynomial.X
theorem MvPolynomial.optionEquivLeft_C (R : Type u) (S₁ : Type v) [] (r : R) :
(MvPolynomial.C r) = Polynomial.C (MvPolynomial.C r)
@[simp]
theorem MvPolynomial.optionEquivRight_apply (R : Type u) (S₁ : Type v) [] (a : MvPolynomial (Option S₁) R) :
a = (MvPolynomial.aeval fun (o : Option S₁) => o.elim (MvPolynomial.C Polynomial.X) MvPolynomial.X) a
@[simp]
theorem MvPolynomial.optionEquivRight_symm_apply (R : Type u) (S₁ : Type v) [] (a : MvPolynomial S₁ (Polynomial R)) :
.symm a = (MvPolynomial.aevalTower (Polynomial.aeval (MvPolynomial.X none)) fun (i : S₁) => ) a

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
theorem MvPolynomial.optionEquivRight_X_some (R : Type u) (S₁ : Type v) [] (x : S₁) :
theorem MvPolynomial.optionEquivRight_X_none (R : Type u) (S₁ : Type v) [] :
(MvPolynomial.X none) = MvPolynomial.C Polynomial.X
theorem MvPolynomial.optionEquivRight_C (R : Type u) (S₁ : Type v) [] (r : R) :
(MvPolynomial.C r) = MvPolynomial.C (Polynomial.C r)

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

Equations
• = .trans
Instances For
theorem MvPolynomial.finSuccEquiv_eq (R : Type u) [] (n : ) :
= MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun (i : Fin (n + 1)) => Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C ) i
@[simp]
theorem MvPolynomial.finSuccEquiv_apply (R : Type u) [] (n : ) (p : MvPolynomial (Fin (n + 1)) R) :
p = (MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun (i : Fin (n + 1)) => Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C ) i) p
theorem MvPolynomial.finSuccEquiv_comp_C_eq_C {R : Type u} [] (n : ) :
(↑.symm).comp (Polynomial.C.comp MvPolynomial.C) = MvPolynomial.C
theorem MvPolynomial.finSuccEquiv_X_zero {R : Type u} [] {n : } :
= Polynomial.X
theorem MvPolynomial.finSuccEquiv_X_succ {R : Type u} [] {n : } {j : Fin n} :
(MvPolynomial.X j.succ) = Polynomial.C
theorem MvPolynomial.finSuccEquiv_coeff_coeff {R : Type u} [] {n : } (m : Fin n →₀ ) (f : MvPolynomial (Fin (n + 1)) R) (i : ) :
MvPolynomial.coeff m (( f).coeff i) =

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} [] {n : } (s : Fin nR) (y : R) (f : MvPolynomial (Fin (n + 1)) R) :
theorem MvPolynomial.coeff_eval_eq_eval_coeff {R : Type u} [] {n : } (s' : Fin nR) (f : Polynomial (MvPolynomial (Fin n) R)) (i : ) :
(Polynomial.map f).coeff i = (f.coeff i)
theorem MvPolynomial.support_coeff_finSuccEquiv {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} {i : } {m : Fin n →₀ } :
m (( f).coeff i).support f.support
theorem MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le {R : Type u} [] {n : } (f : MvPolynomial (Fin (n + 1)) R) (i : ) (hi : ( f).coeff i 0) :
(( 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.finSuccEquiv_support {R : Type u} [] {n : } (f : MvPolynomial (Fin (n + 1)) R) :
( f).support = Finset.image (fun (m : Fin (n + 1) →₀ ) => m 0) f.support
theorem MvPolynomial.finSuccEquiv_support' {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} {i : } :
Finset.image (Finsupp.cons i) (( f).coeff i).support = Finset.filter (fun (m : Fin (n + 1) →₀ ) => m 0 = i) f.support
theorem MvPolynomial.support_finSuccEquiv_nonempty {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} (h : f 0) :
( f).support.Nonempty
theorem MvPolynomial.degree_finSuccEquiv {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} (h : f 0) :
( f).degree =
theorem MvPolynomial.natDegree_finSuccEquiv {R : Type u} [] {n : } (f : MvPolynomial (Fin (n + 1)) R) :
( f).natDegree =
theorem MvPolynomial.degreeOf_coeff_finSuccEquiv {R : Type u} [] {n : } (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ) :
theorem MvPolynomial.finSuccEquiv_rename_finSuccEquiv {R : Type u} {σ : Type u_1} [] {n : } (e : σ Fin n) (φ : MvPolynomial (Option σ) R) :
((MvPolynomial.rename (e.optionCongr.trans (finSuccEquiv n).symm)) φ) = Polynomial.map .toRingHom ( φ)

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.