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^s -
a : R -
i : σ, with corresponding monomialX i, often denotedX_iby mathematicians -
p : mv_polynomial σ R
Tags #
equivalence, isomorphism, morphism, ring hom, hom
noncomputable
def
mv_polynomial.punit_alg_equiv
(R : Type u)
[comm_semiring R] :
mv_polynomial punit R ≃ₐ[R] polynomial R
The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.
Equations
- mv_polynomial.punit_alg_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' := _, commutes' := _}
@[simp]
theorem
mv_polynomial.punit_alg_equiv_apply
(R : Type u)
[comm_semiring R]
(p : mv_polynomial punit R) :
⇑(mv_polynomial.punit_alg_equiv R) p = mv_polynomial.eval₂ polynomial.C (λ (u : punit), polynomial.X) p
@[simp]
theorem
mv_polynomial.punit_alg_equiv_symm_apply
(R : Type u)
[comm_semiring R]
(p : polynomial R) :
@[simp]
theorem
mv_polynomial.map_equiv_apply
{S₁ : Type v}
{S₂ : Type w}
(σ : Type u_1)
[comm_semiring S₁]
[comm_semiring S₂]
(e : S₁ ≃+* S₂)
(ᾰ : mv_polynomial σ S₁) :
⇑(mv_polynomial.map_equiv σ e) ᾰ = ⇑(mv_polynomial.map ↑e) ᾰ
noncomputable
def
mv_polynomial.map_equiv
{S₁ : Type v}
{S₂ : Type w}
(σ : Type u_1)
[comm_semiring S₁]
[comm_semiring S₂]
(e : S₁ ≃+* S₂) :
mv_polynomial σ S₁ ≃+* mv_polynomial σ S₂
If e : A ≃+* B is an isomorphism of rings, then so is map e.
@[simp]
@[simp]
theorem
mv_polynomial.map_equiv_symm
{S₁ : Type v}
{S₂ : Type w}
(σ : Type u_1)
[comm_semiring S₁]
[comm_semiring S₂]
(e : S₁ ≃+* S₂) :
(mv_polynomial.map_equiv σ e).symm = mv_polynomial.map_equiv σ e.symm
@[simp]
theorem
mv_polynomial.map_equiv_trans
{S₁ : Type v}
{S₂ : Type w}
{S₃ : Type x}
(σ : Type u_1)
[comm_semiring S₁]
[comm_semiring S₂]
[comm_semiring S₃]
(e : S₁ ≃+* S₂)
(f : S₂ ≃+* S₃) :
(mv_polynomial.map_equiv σ e).trans (mv_polynomial.map_equiv σ f) = mv_polynomial.map_equiv σ (e.trans f)
@[simp]
theorem
mv_polynomial.map_alg_equiv_apply
{R : Type u}
(σ : Type u_1)
[comm_semiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
[comm_semiring A₁]
[comm_semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂)
(ᾰ : mv_polynomial σ A₁) :
⇑(mv_polynomial.map_alg_equiv σ e) ᾰ = ⇑(mv_polynomial.map ↑e) ᾰ
noncomputable
def
mv_polynomial.map_alg_equiv
{R : Type u}
(σ : Type u_1)
[comm_semiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
[comm_semiring A₁]
[comm_semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
mv_polynomial σ A₁ ≃ₐ[R] mv_polynomial σ A₂
If e : A ≃ₐ[R] B is an isomorphism of R-algebras, then so is map e.
@[simp]
theorem
mv_polynomial.map_alg_equiv_refl
{R : Type u}
(σ : Type u_1)
[comm_semiring R]
{A₁ : Type u_2}
[comm_semiring A₁]
[algebra R A₁] :
@[simp]
theorem
mv_polynomial.map_alg_equiv_symm
{R : Type u}
(σ : Type u_1)
[comm_semiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
[comm_semiring A₁]
[comm_semiring A₂]
[algebra R A₁]
[algebra R A₂]
(e : A₁ ≃ₐ[R] A₂) :
@[simp]
theorem
mv_polynomial.map_alg_equiv_trans
{R : Type u}
(σ : Type u_1)
[comm_semiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
{A₃ : Type u_4}
[comm_semiring A₁]
[comm_semiring A₂]
[comm_semiring A₃]
[algebra R A₁]
[algebra R A₂]
[algebra R A₃]
(e : A₁ ≃ₐ[R] A₂)
(f : A₂ ≃ₐ[R] A₃) :
(mv_polynomial.map_alg_equiv σ e).trans (mv_polynomial.map_alg_equiv σ f) = mv_polynomial.map_alg_equiv σ (e.trans f)
noncomputable
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))
@[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)
noncomputable
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.is_empty_alg_equiv_symm_apply_to_fun
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ]
(ᾰ : R)
(a' : σ →₀ ℕ) :
@[simp]
theorem
mv_polynomial.is_empty_alg_equiv_apply
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ]
(ᾰ : mv_polynomial σ R) :
⇑(mv_polynomial.is_empty_alg_equiv R σ) ᾰ = ⇑(mv_polynomial.aeval he.elim) ᾰ
@[simp]
theorem
mv_polynomial.is_empty_alg_equiv_symm_apply_support
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ]
(ᾰ : R) :
noncomputable
def
mv_polynomial.is_empty_alg_equiv
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ] :
mv_polynomial σ R ≃ₐ[R] R
The algebra isomorphism between multivariable polynomials in no variables and the ground ring.
Equations
- mv_polynomial.is_empty_alg_equiv R σ = alg_equiv.of_alg_hom (mv_polynomial.aeval he.elim) (algebra.of_id R (mv_polynomial σ R)) _ _
@[simp]
theorem
mv_polynomial.is_empty_ring_equiv_symm_apply_support
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ]
(ᾰ : R) :
@[simp]
theorem
mv_polynomial.is_empty_ring_equiv_symm_apply_to_fun
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ]
(ᾰ : R)
(a' : σ →₀ ℕ) :
noncomputable
def
mv_polynomial.is_empty_ring_equiv
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ] :
mv_polynomial σ R ≃+* R
The ring isomorphism between multivariable polynomials in no variables and the ground ring.
Equations
@[simp]
theorem
mv_polynomial.is_empty_ring_equiv_apply
(R : Type u)
(σ : Type u_1)
[comm_semiring R]
[he : is_empty σ]
(ᾰ : mv_polynomial σ R) :
⇑(mv_polynomial.is_empty_ring_equiv R σ) ᾰ = ⇑(mv_polynomial.aeval he.elim) ᾰ
@[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 : (f.comp g).comp mv_polynomial.C = mv_polynomial.C)
(hfgX : ∀ (n : S₂), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n)
(hgfC : (g.comp f).comp mv_polynomial.C = mv_polynomial.C)
(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 : (f.comp g).comp mv_polynomial.C = mv_polynomial.C)
(hfgX : ∀ (n : S₂), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n)
(hgfC : (g.comp f).comp mv_polynomial.C = mv_polynomial.C)
(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 ᾰ
noncomputable
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 : (f.comp g).comp mv_polynomial.C = mv_polynomial.C)
(hfgX : ∀ (n : S₂), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n)
(hgfC : (g.comp f).comp mv_polynomial.C = mv_polynomial.C)
(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.
noncomputable
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₂) _ _ _ _
noncomputable
def
mv_polynomial.sum_alg_equiv
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
[comm_semiring R] :
mv_polynomial (S₁ ⊕ S₂) R ≃ₐ[R] mv_polynomial S₁ (mv_polynomial S₂ R)
The algebra 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_alg_equiv R S₁ S₂ = {to_fun := (mv_polynomial.sum_ring_equiv R S₁ S₂).to_fun, inv_fun := (mv_polynomial.sum_ring_equiv R S₁ S₂).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
mv_polynomial.option_equiv_left_apply
(R : Type u)
(S₁ : Type v)
[comm_semiring R]
(ᾰ : mv_polynomial (option S₁) R) :
⇑(mv_polynomial.option_equiv_left R S₁) ᾰ = ⇑(mv_polynomial.aeval (λ (o : option S₁), o.elim polynomial.X (λ (s : S₁), ⇑polynomial.C (mv_polynomial.X s)))) ᾰ
noncomputable
def
mv_polynomial.option_equiv_left
(R : Type u)
(S₁ : Type v)
[comm_semiring R] :
mv_polynomial (option S₁) R ≃ₐ[R] polynomial (mv_polynomial S₁ R)
The algebra isomorphism between multivariable polynomials in option S₁ and
polynomials with coefficients in mv_polynomial S₁ R.
Equations
- mv_polynomial.option_equiv_left R S₁ = alg_equiv.of_alg_hom (mv_polynomial.aeval (λ (o : option S₁), o.elim polynomial.X (λ (s : S₁), ⇑polynomial.C (mv_polynomial.X s)))) (polynomial.aeval_tower (mv_polynomial.rename some) (mv_polynomial.X none)) _ _
@[simp]
theorem
mv_polynomial.option_equiv_left_symm_apply
(R : Type u)
(S₁ : Type v)
[comm_semiring R]
(ᾰ : polynomial (mv_polynomial S₁ R)) :
⇑((mv_polynomial.option_equiv_left R S₁).symm) ᾰ = ⇑(polynomial.aeval_tower (mv_polynomial.rename some) (mv_polynomial.X none)) ᾰ
noncomputable
def
mv_polynomial.option_equiv_right
(R : Type u)
(S₁ : Type v)
[comm_semiring R] :
mv_polynomial (option S₁) R ≃ₐ[R] mv_polynomial S₁ (polynomial R)
The algebra isomorphism between multivariable polynomials in option S₁ and
multivariable polynomials with coefficients in polynomials.
Equations
- mv_polynomial.option_equiv_right R S₁ = alg_equiv.of_alg_hom (mv_polynomial.aeval (λ (o : option S₁), o.elim (⇑mv_polynomial.C polynomial.X) mv_polynomial.X)) (mv_polynomial.aeval_tower (polynomial.aeval (mv_polynomial.X none)) (λ (i : S₁), mv_polynomial.X (some i))) _ _
noncomputable
def
mv_polynomial.fin_succ_equiv
(R : Type u)
[comm_semiring R]
(n : ℕ) :
mv_polynomial (fin (n + 1)) R ≃ₐ[R] polynomial (mv_polynomial (fin n) R)
The algebra 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