mathlib3 documentation

data.mv_polynomial.equiv

Equivalences between polynomial rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Equations
@[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₁) :
noncomputable def mv_polynomial.map_equiv {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [comm_semiring S₁] [comm_semiring S₂] (e : S₁ ≃+* S₂) :

If e : A ≃+* B is an isomorphism of rings, then so is map e.

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

If e : A ≃ₐ[R] B is an isomorphism of R-algebras, then so is map e.

Equations
@[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₃) :
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
@[simp]
@[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₂) :
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_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (b : S₁) :
@[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) (i : σ →₀ ) :
@[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 σ] :

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

Equations
@[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) (i : σ →₀ ) :
noncomputable def mv_polynomial.is_empty_ring_equiv (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] :

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

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

A helper function for sum_ring_equiv.

Equations
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
noncomputable def mv_polynomial.sum_alg_equiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring 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
noncomputable def mv_polynomial.option_equiv_left (R : Type u) (S₁ : Type v) [comm_semiring R] :

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

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

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

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

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

Equations

The coefficient of m in the i-th coefficient of fin_succ_equiv R n f equals the coefficient of finsupp.cons i m in f.