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 ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.

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

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

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

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

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

@[simp]
theorem mv_polynomial.ring_equiv_congr_inv_fun (R : Type u) {S₁ : Type v} {S₂ : Type w} [comm_semiring R] [comm_semiring S₂] (e : R ≃+* S₂) (a : 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₂] :
R ≃+* S₂mv_polynomial S₁ R ≃+* mv_polynomial S₁ 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_to_fun (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 : mv_polynomial S₁ R) :
(mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) a = f a

@[simp]
theorem mv_polynomial.mv_polynomial_equiv_mv_polynomial_inv_fun (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 : mv_polynomial S₂ S₃) :
(mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX).inv_fun a = g a

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) :
(∀ (a : S₃), f (g (mv_polynomial.C a)) = mv_polynomial.C a)(∀ (n : S₂), f (g (mv_polynomial.X n)) = mv_polynomial.X n)(∀ (a : R), g (f (mv_polynomial.C a)) = mv_polynomial.C a)(∀ (n : S₁), g (f (mv_polynomial.X n)) = mv_polynomial.X n)mv_polynomial S₁ R ≃+* mv_polynomial S₂ S₃

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