mvPolynomialOptionEquivPolynomialAdjoin

English

There is a natural isomorphism between the multivariate polynomial ring on Option ι and the polynomial ring over the algebra generated by an algebraically independent family.

Русский

Существует естественный изоморфизм между кольцом многочленов по Option ι и кольцом многочленов над порожденной алгеброй алгебраически независимой семьи.

LaTeX

$$$\MvPolynomial (Option \ ι) R \cong_*\ Polynomial (\operatorname{adjoin} R (\operatorname{range} x))$$$

Lean4

/-- The isomorphism between `MvPolynomial (Option ι) R` and the polynomial ring over
the algebra generated by an algebraically independent family. -/
def mvPolynomialOptionEquivPolynomialAdjoin (hx : AlgebraicIndependent R x) :
    MvPolynomial (Option ι) R ≃+* Polynomial (adjoin R (Set.range x)) :=
  (MvPolynomial.optionEquivLeft _ _).toRingEquiv.trans (Polynomial.mapEquiv hx.aevalEquiv.toRingEquiv)

Похожие утверждения