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 σ R
which mathematicians might callX^s
a : R
i : σ
, with corresponding monomialX i
, often denotedX_i
by mathematiciansp : mv_polynomial σ R
Tags
equivalence, isomorphism, morphism, ring hom, hom
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' := _}
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' := _}
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' := _}
The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.
The algebra isomorphism between multivariable polynomials induced by an equivalence of the variables.
The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring.
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))
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
A helper function for sum_ring_equiv
.
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₂) _ _ _ _
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)))
The ring isomorphism between multivariable polynomials in option S₁
and
multivariable polynomials with coefficients in polynomials.
Equations
The ring isomorphism between multivariable polynomials in fin (n + 1)
and
polynomials over multivariable polynomials in fin n
.