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 algebra isomorphism between multivariable polynomials in no variables and the ground ring.

Equations

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.map_equiv_apply {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [comm_semiring S₁] [comm_semiring S₂] (e : S₁ ≃+* S₂) (ᾰ : mv_polynomial σ S₁) :
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₃) :
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_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₂) (x : mv_polynomial σ A₁) :
@[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₃) :
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_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) :

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.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
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
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

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

Equations