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 inmv_polynomial σ Rwhich mathematicians might callX^sa : Ri : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : mv_polynomial σ R
Tags
equivalence, isomorphism, morphism, ring hom, hom
@[simp]
theorem
mv_polynomial.pempty_ring_equiv_apply
(R : Type u)
[comm_semiring R]
(p : mv_polynomial pempty 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' := _}
@[simp]
@[simp]
theorem
mv_polynomial.pempty_alg_equiv_symm_apply
(R : Type u)
[comm_semiring R]
(ᾰ : R) :
⇑((mv_polynomial.pempty_alg_equiv R).symm) ᾰ = ⇑mv_polynomial.C ᾰ
@[simp]
theorem
mv_polynomial.pempty_alg_equiv_apply
(R : Type u)
[comm_semiring R]
(p : mv_polynomial pempty R) :
The algebra isomorphism between multivariable polynomials in no variables and the ground ring.
Equations
- mv_polynomial.pempty_alg_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' := _, commutes' := _}
@[simp]
theorem
mv_polynomial.punit_ring_equiv_apply
(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
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' := _}
@[simp]
theorem
mv_polynomial.punit_ring_equiv_symm_apply
(R : Type u)
[comm_semiring R]
(p : polynomial R) :
@[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) :
⇑((mv_polynomial.ring_equiv_of_equiv R e).symm) ᾰ = ⇑(mv_polynomial.rename ⇑(e.symm)) ᾰ
@[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) :
⇑(mv_polynomial.ring_equiv_of_equiv R e) ᾰ = ⇑(mv_polynomial.rename ⇑e) ᾰ
def
mv_polynomial.ring_equiv_of_equiv
(R : Type u)
{S₁ : Type v}
{S₂ : Type w}
[comm_semiring R]
(e : S₁ ≃ S₂) :
mv_polynomial S₁ R ≃+* mv_polynomial S₂ R
The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.
@[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) :
⇑((mv_polynomial.alg_equiv_of_equiv R e).symm) ᾰ = ⇑(mv_polynomial.rename ⇑(e.symm)) ᾰ
def
mv_polynomial.alg_equiv_of_equiv
(R : Type u)
{S₁ : Type v}
{S₂ : Type w}
[comm_semiring R]
(e : S₁ ≃ S₂) :
mv_polynomial S₁ R ≃ₐ[R] mv_polynomial S₂ R
The algebra isomorphism between multivariable polynomials induced by an equivalence of the variables.
@[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) :
⇑(mv_polynomial.alg_equiv_of_equiv R e) ᾰ = ⇑(mv_polynomial.rename ⇑e) ᾰ
@[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) :
⇑(mv_polynomial.ring_equiv_congr R e) ᾰ = ⇑(mv_polynomial.map ↑e) ᾰ
@[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₂) :
⇑((mv_polynomial.ring_equiv_congr R e).symm) ᾰ = ⇑(mv_polynomial.map ↑(e.symm)) ᾰ
def
mv_polynomial.ring_equiv_congr
(R : Type u)
{S₁ : Type v}
{S₂ : Type w}
[comm_semiring R]
[comm_semiring S₂]
(e : 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.
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))
@[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₂)
@[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)
@[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
@[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)
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) :
⇑(mv_polynomial.iter_to_sum R S₁ S₂) (⇑mv_polynomial.C (⇑mv_polynomial.C a)) = ⇑mv_polynomial.C a
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)
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)
@[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) :
mv_polynomial S₁ R ≃+* mv_polynomial S₂ S₃
A helper function for sum_ring_equiv.
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₂) _ _ _ _
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)))
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
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
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)
@[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