# Documentation

Mathlib.Data.MvPolynomial.Equiv

# 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_apply (R : Type u) [] (p : ) :
= MvPolynomial.eval₂ Polynomial.C (fun x => Polynomial.X) p
@[simp]
theorem MvPolynomial.pUnitAlgEquiv_symm_apply (R : Type u) [] (p : ) :
= Polynomial.eval₂ MvPolynomial.C () p

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

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

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₂) :
@[simp]
theorem MvPolynomial.mapEquiv_trans {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} (σ : Type u_1) [] [] [] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :
@[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 = ↑() 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.

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₂) :
@[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₃) :
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.

Instances For
@[simp]
theorem MvPolynomial.sumToIter_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (a : R) :
↑() (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.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.

Instances For
theorem MvPolynomial.iterToSum_C_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (a : R) :
↑() (MvPolynomial.C (MvPolynomial.C a)) = MvPolynomial.C a
theorem MvPolynomial.iterToSum_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (b : S₁) :
↑() () =
theorem MvPolynomial.iterToSum_C_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [] (c : S₂) :
↑() (MvPolynomial.C ()) =
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_symm_apply_toFun (R : Type u) (σ : Type u_1) [] [he : ] (a : R) (j : σ →₀ ) :
↑(↑() a) j = Pi.single 0 a j
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_apply (R : Type u) (σ : Type u_1) [] [he : ] (a : ) :
↑() a = ↑(MvPolynomial.aeval fun a => IsEmpty.elim he a) a
@[simp]
theorem MvPolynomial.isEmptyAlgEquiv_symm_apply_support (R : Type u) (σ : Type u_1) [] [he : ] (a : R) :
(↑() a).support = if a = 0 then else {0}
def MvPolynomial.isEmptyAlgEquiv (R : Type u) (σ : Type u_1) [] [he : ] :

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

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

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

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 : RingHom.comp () MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g ()) = ) (hgfC : RingHom.comp () MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f ()) = ) (a : MvPolynomial S₂ S₃) :
↑(RingEquiv.symm (MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX)) 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 : RingHom.comp () MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g ()) = ) (hgfC : RingHom.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 : RingHom.comp () MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g ()) = ) (hgfC : RingHom.comp () MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f ()) = ) :

A helper function for sumRingEquiv.

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.

Instances For
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.

Instances For
@[simp]
theorem MvPolynomial.optionEquivLeft_apply (R : Type u) (S₁ : Type v) [] (a : MvPolynomial (Option S₁) R) :
↑() a = ↑(MvPolynomial.aeval fun o => match o, Polynomial.X, fun s => Polynomial.C () with | some x, x_1, f => f x | none, y, x => y) a
@[simp]
theorem MvPolynomial.optionEquivLeft_symm_apply (R : Type u) (S₁ : Type v) [] (a : Polynomial (MvPolynomial S₁ R)) :
↑() a = ↑(Polynomial.aevalTower () (MvPolynomial.X none)) a

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

Instances For
def MvPolynomial.optionEquivRight (R : Type u) (S₁ : Type v) [] :

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

Instances For

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

Instances For
theorem MvPolynomial.finSuccEquiv_eq (R : Type u) [] (n : ) :
↑() = MvPolynomial.eval₂Hom (RingHom.comp Polynomial.C MvPolynomial.C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C ()) i
@[simp]
theorem MvPolynomial.finSuccEquiv_apply (R : Type u) [] (n : ) (p : MvPolynomial (Fin (n + 1)) R) :
↑() p = ↑(MvPolynomial.eval₂Hom (RingHom.comp Polynomial.C MvPolynomial.C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C ()) i) p
theorem MvPolynomial.finSuccEquiv_comp_C_eq_C {R : Type u} [] (n : ) :
RingHom.comp (↑()) (RingHom.comp Polynomial.C 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} :
↑() () = Polynomial.C ()
theorem MvPolynomial.finSuccEquiv_coeff_coeff {R : Type u} [] {n : } (m : Fin n →₀ ) (f : MvPolynomial (Fin (n + 1)) R) (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) :
↑() f = Polynomial.eval y (Polynomial.map () (↑() f))
theorem MvPolynomial.coeff_eval_eq_eval_coeff {R : Type u} [] {n : } (s' : Fin nR) (f : Polynomial (MvPolynomial (Fin n) R)) (i : ) :
= ↑() ()
theorem MvPolynomial.support_coeff_finSuccEquiv {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} {i : } {m : Fin n →₀ } :
theorem MvPolynomial.finSuccEquiv_support {R : Type u} [] {n : } (f : MvPolynomial (Fin (n + 1)) R) :
Polynomial.support (↑() f) = Finset.image (fun m => m 0) ()
theorem MvPolynomial.finSuccEquiv_support' {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} {i : } :
Finset.image () (MvPolynomial.support (Polynomial.coeff (↑() f) i)) = Finset.filter (fun m => m 0 = i) ()
theorem MvPolynomial.support_finSuccEquiv_nonempty {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} (h : f 0) :
theorem MvPolynomial.degree_finSuccEquiv {R : Type u} [] {n : } {f : MvPolynomial (Fin (n + 1)) R} (h : f 0) :
Polynomial.degree (↑() f) = ↑()
theorem MvPolynomial.natDegree_finSuccEquiv {R : Type u} [] {n : } (f : MvPolynomial (Fin (n + 1)) R) :
theorem MvPolynomial.degreeOf_coeff_finSuccEquiv {R : Type u} [] {n : } (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ) :