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* [comm_semiring R] (the coefficients)
s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in mv_polynomial σ R which mathematicians might call X^s
a : R
i : σ, with corresponding monomial X i, often denoted X_i by mathematicians
p : mv_polynomial σ R

Tags

equivalence, isomorphism, morphism, ring hom, hom

source

@[simp]

theorem mv_polynomial.pempty_ring_equiv_inv_fun (R : Type u) [comm_semiring R] (a : R) :

(mv_polynomial.pempty_ring_equiv R).inv_fun a = ⇑mv_polynomial.C a

source

def mv_polynomial.pempty_ring_equiv (R : Type u) [comm_semiring R] :

mv_polynomial pempty R ≃+* R

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

Equations

mv_polynomial.pempty_ring_equiv R = {to_fun := mv_polynomial.eval₂ (ring_hom.id R) pempty.elim, inv_fun := ⇑mv_polynomial.C, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem mv_polynomial.pempty_ring_equiv_to_fun (R : Type u) [comm_semiring R] (p : mv_polynomial pempty R) :

⇑(mv_polynomial.pempty_ring_equiv R) p = mv_polynomial.eval₂ (ring_hom.id R) pempty.elim p

source

def mv_polynomial.punit_ring_equiv (R : Type u) [comm_semiring R] :

mv_polynomial punit R ≃+* polynomial R

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

Equations

mv_polynomial.punit_ring_equiv R = {to_fun := mv_polynomial.eval₂ polynomial.C (λ (u : punit), polynomial.X), inv_fun := polynomial.eval₂ mv_polynomial.C (mv_polynomial.X punit.star), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem mv_polynomial.punit_ring_equiv_to_fun (R : Type u) [comm_semiring R] (p : mv_polynomial punit R) :

⇑(mv_polynomial.punit_ring_equiv R) p = mv_polynomial.eval₂ polynomial.C (λ (u : punit), polynomial.X) p

source

@[simp]

theorem mv_polynomial.punit_ring_equiv_inv_fun (R : Type u) [comm_semiring R] (p : polynomial R) :

(mv_polynomial.punit_ring_equiv R).inv_fun p = polynomial.eval₂ mv_polynomial.C (mv_polynomial.X punit.star) p

source

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

(mv_polynomial.ring_equiv_of_equiv R e).inv_fun a = ⇑(mv_polynomial.rename ⇑(e.symm)) a

source

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

⇑(mv_polynomial.ring_equiv_of_equiv R e) a = ⇑(mv_polynomial.rename ⇑e) a

source

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

mv_polynomial.ring_equiv_of_equiv R e = {to_fun := ⇑(mv_polynomial.rename ⇑e), inv_fun := ⇑(mv_polynomial.rename ⇑(e.symm)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

⇑(mv_polynomial.ring_equiv_congr R e) a = ⇑(mv_polynomial.map ↑e) a

source

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

(mv_polynomial.ring_equiv_congr R e).inv_fun a = ⇑(mv_polynomial.map ↑(e.symm)) a

source

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

mv_polynomial.ring_equiv_congr R e = {to_fun := ⇑(mv_polynomial.map ↑e), inv_fun := ⇑(mv_polynomial.map ↑(e.symm)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

mv_polynomial.sum_to_iter R S₁ S₂ = mv_polynomial.eval₂_hom (mv_polynomial.C.comp mv_polynomial.C) (λ (bc : S₁ ⊕ S₂), bc.rec_on mv_polynomial.X (⇑mv_polynomial.C ∘ mv_polynomial.X))

source

@[instance]

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

is_semiring_hom ⇑(mv_polynomial.sum_to_iter R S₁ S₂)

source

@[simp]

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

⇑(mv_polynomial.sum_to_iter R S₁ S₂) (⇑mv_polynomial.C a) = ⇑mv_polynomial.C (⇑mv_polynomial.C a)

source

@[simp]

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

⇑(mv_polynomial.sum_to_iter R S₁ S₂) (mv_polynomial.X (sum.inl b)) = mv_polynomial.X b

source

@[simp]

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

⇑(mv_polynomial.sum_to_iter R S₁ S₂) (mv_polynomial.X (sum.inr c)) = ⇑mv_polynomial.C (mv_polynomial.X c)

source

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

mv_polynomial.iter_to_sum R S₁ S₂ = mv_polynomial.eval₂_hom (ring_hom.of (mv_polynomial.eval₂ mv_polynomial.C (mv_polynomial.X ∘ sum.inr))) (mv_polynomial.X ∘ sum.inl)

source

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

⇑(mv_polynomial.iter_to_sum R S₁ S₂) (⇑mv_polynomial.C (⇑mv_polynomial.C a)) = ⇑mv_polynomial.C a

source

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

⇑(mv_polynomial.iter_to_sum R S₁ S₂) (mv_polynomial.X b) = mv_polynomial.X (sum.inl b)

source

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

⇑(mv_polynomial.iter_to_sum R S₁ S₂) (⇑mv_polynomial.C (mv_polynomial.X c)) = mv_polynomial.X (sum.inr c)

source

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

source

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

source

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

mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX = {to_fun := ⇑f, inv_fun := ⇑g, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

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

mv_polynomial.sum_ring_equiv R S₁ S₂ = mv_polynomial.mv_polynomial_equiv_mv_polynomial R (S₁ ⊕ S₂) S₁ (mv_polynomial S₂ R) (mv_polynomial.sum_to_iter R S₁ S₂) (mv_polynomial.iter_to_sum R S₁ S₂) _ _ _ _

source

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

mv_polynomial (option S₁) R ≃+* polynomial (mv_polynomial S₁ R)

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

Equations

mv_polynomial.option_equiv_left R S₁ = (mv_polynomial.ring_equiv_of_equiv R ((equiv.option_equiv_sum_punit S₁).trans (equiv.sum_comm S₁ punit))).trans ((mv_polynomial.sum_ring_equiv R punit S₁).trans (mv_polynomial.punit_ring_equiv (mv_polynomial S₁ R)))

source

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

mv_polynomial (option S₁) R ≃+* mv_polynomial S₁ (polynomial R)

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

Equations

mv_polynomial.option_equiv_right R S₁ = (mv_polynomial.ring_equiv_of_equiv R (equiv.option_equiv_sum_punit S₁)).trans ((mv_polynomial.sum_ring_equiv R S₁ unit).trans (mv_polynomial.ring_equiv_congr (mv_polynomial unit R) (mv_polynomial.punit_ring_equiv R)))

source

def mv_polynomial.fin_succ_equiv (R : Type u) [comm_semiring R] (n : ℕ) :

mv_polynomial (fin (n + 1)) R ≃+* polynomial (mv_polynomial (fin n) R)

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

Equations

mv_polynomial.fin_succ_equiv R n = (mv_polynomial.ring_equiv_of_equiv R (fin_succ_equiv n)).trans (mv_polynomial.option_equiv_left R (fin n))

source

theorem mv_polynomial.fin_succ_equiv_eq (R : Type u) [comm_semiring R] (n : ℕ) :

↑(mv_polynomial.fin_succ_equiv R n) = mv_polynomial.eval₂_hom (polynomial.C.comp mv_polynomial.C) (λ (i : fin (n + 1)), fin.cases polynomial.X (λ (k : fin n), ⇑polynomial.C (mv_polynomial.X k)) i)

source

@[simp]

theorem mv_polynomial.fin_succ_equiv_apply (R : Type u) [comm_semiring R] (n : ℕ) (p : mv_polynomial (fin (n + 1)) R) :

⇑(mv_polynomial.fin_succ_equiv R n) p = ⇑(mv_polynomial.eval₂_hom (polynomial.C.comp mv_polynomial.C) (λ (i : fin (n + 1)), fin.cases polynomial.X (λ (k : fin n), ⇑polynomial.C (mv_polynomial.X k)) i)) p