mathlib documentation

data.mv_polynomial.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:

Tags

equivalence, isomorphism, morphism, ring hom, hom

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

Equations

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

Equations

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

Equations
@[simp]
theorem mv_polynomial.ring_equiv_of_equiv_symm_apply (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] (e : S₁ S₂) (ᾰ : mv_polynomial S₂ R) :

@[simp]
theorem mv_polynomial.ring_equiv_of_equiv_apply (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] (e : S₁ S₂) (ᾰ : mv_polynomial S₁ R) :

def mv_polynomial.ring_equiv_of_equiv (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] (e : S₁ S₂) :

The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.

Equations
@[simp]
theorem mv_polynomial.alg_equiv_of_equiv_symm_apply (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] (e : S₁ S₂) (ᾰ : mv_polynomial S₂ R) :

def mv_polynomial.alg_equiv_of_equiv (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] (e : S₁ S₂) :

The algebra isomorphism between multivariable polynomials induced by an equivalence of the variables.

Equations
@[simp]
theorem mv_polynomial.alg_equiv_of_equiv_apply (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] (e : S₁ S₂) (ᾰ : mv_polynomial S₁ R) :

@[simp]
theorem mv_polynomial.ring_equiv_congr_apply (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] [comm_semiring S₂] (e : R ≃+* S₂) (ᾰ : mv_polynomial S₁ R) :

@[simp]
theorem mv_polynomial.ring_equiv_congr_symm_apply (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] [comm_semiring S₂] (e : R ≃+* S₂) (ᾰ : mv_polynomial S₁ S₂) :

def mv_polynomial.ring_equiv_congr (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] [comm_semiring S₂] (e : R ≃+* S₂) :

The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring.

Equations
def mv_polynomial.sum_to_iter (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :
mv_polynomial (S₁ S₂) R →+* mv_polynomial S₁ (mv_polynomial S₂ R)

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

See sum_ring_equiv for the ring isomorphism.

Equations
@[instance]
def mv_polynomial.is_semiring_hom_sum_to_iter (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :

@[simp]
theorem mv_polynomial.sum_to_iter_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (a : R) :

@[simp]
theorem mv_polynomial.sum_to_iter_Xl (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (b : S₁) :

@[simp]
theorem mv_polynomial.sum_to_iter_Xr (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (c : S₂) :

def mv_polynomial.iter_to_sum (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :
mv_polynomial S₁ (mv_polynomial S₂ R) →+* mv_polynomial (S₁ S₂) R

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

See sum_ring_equiv for the ring isomorphism.

Equations
theorem mv_polynomial.iter_to_sum_C_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (a : R) :

theorem mv_polynomial.iter_to_sum_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (b : S₁) :

theorem mv_polynomial.iter_to_sum_C_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (c : S₂) :

@[simp]
theorem mv_polynomial.mv_polynomial_equiv_mv_polynomial_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [comm_semiring R] [comm_semiring S₃] (f : mv_polynomial S₁ R →+* mv_polynomial S₂ S₃) (g : mv_polynomial S₂ S₃ →+* mv_polynomial S₁ R) (hfgC : ∀ (a : S₃), f (g (mv_polynomial.C a)) = mv_polynomial.C a) (hfgX : ∀ (n : S₂), f (g (mv_polynomial.X n)) = mv_polynomial.X n) (hgfC : ∀ (a : R), g (f (mv_polynomial.C a)) = mv_polynomial.C a) (hgfX : ∀ (n : S₁), g (f (mv_polynomial.X n)) = mv_polynomial.X n) (ᾰ : mv_polynomial S₁ R) :
(mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) = f ᾰ

@[simp]
theorem mv_polynomial.mv_polynomial_equiv_mv_polynomial_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [comm_semiring R] [comm_semiring S₃] (f : mv_polynomial S₁ R →+* mv_polynomial S₂ S₃) (g : mv_polynomial S₂ S₃ →+* mv_polynomial S₁ R) (hfgC : ∀ (a : S₃), f (g (mv_polynomial.C a)) = mv_polynomial.C a) (hfgX : ∀ (n : S₂), f (g (mv_polynomial.X n)) = mv_polynomial.X n) (hgfC : ∀ (a : R), g (f (mv_polynomial.C a)) = mv_polynomial.C a) (hgfX : ∀ (n : S₁), g (f (mv_polynomial.X n)) = mv_polynomial.X n) (ᾰ : mv_polynomial S₂ S₃) :
((mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX).symm) = g ᾰ

def mv_polynomial.mv_polynomial_equiv_mv_polynomial (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [comm_semiring R] [comm_semiring S₃] (f : mv_polynomial S₁ R →+* mv_polynomial S₂ S₃) (g : mv_polynomial S₂ S₃ →+* mv_polynomial S₁ R) (hfgC : ∀ (a : S₃), f (g (mv_polynomial.C a)) = mv_polynomial.C a) (hfgX : ∀ (n : S₂), f (g (mv_polynomial.X n)) = mv_polynomial.X n) (hgfC : ∀ (a : R), g (f (mv_polynomial.C a)) = mv_polynomial.C a) (hgfX : ∀ (n : S₁), g (f (mv_polynomial.X n)) = mv_polynomial.X n) :

A helper function for sum_ring_equiv.

Equations
def mv_polynomial.sum_ring_equiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :
mv_polynomial (S₁ S₂) R ≃+* mv_polynomial S₁ (mv_polynomial S₂ R)

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

Equations
def mv_polynomial.option_equiv_left (R : Type u) (S₁ : Type v) [comm_semiring R] :

The ring isomorphism between multivariable polynomials in option S₁ and polynomials with coefficients in mv_polynomial S₁ R.

Equations
def mv_polynomial.option_equiv_right (R : Type u) (S₁ : Type v) [comm_semiring R] :

The ring isomorphism between multivariable polynomials in option S₁ and multivariable polynomials with coefficients in polynomials.

Equations

The ring isomorphism between multivariable polynomials in fin (n + 1) and polynomials over multivariable polynomials in fin n.

Equations