supportedEquivMvPolynomial — Mathlib

English

There is an isomorphism of R-algebras between the subalgebra of polynomials supported by s and the polynomial ring in s, i.e. an equivalence supported R s ≃ₐ[R] MvPolynomial s R.

Русский

Существуют изоморфизм алгебр над R между подалгеброй полиномов, поддерживаемых s, и полиномиальной окружностью по переменным s: supported R s ≃ₐ[R] MvPolynomial s R.

LaTeX

$$$ \text{supported } R s \cong_{R} \mathrm{MvPolynomial}\ s\ R $$$

Lean4

/-- The isomorphism between the subalgebra of polynomials supported by `s` and
`MvPolynomial s R`. -/
noncomputable def supportedEquivMvPolynomial (s : Set σ) : supported R s ≃ₐ[R] MvPolynomial s R :=
  (Subalgebra.equivOfEq _ _ (supported_eq_range_rename s)).trans
    (AlgEquiv.ofInjective (rename ((↑) : s → σ)) (rename_injective _ Subtype.val_injective)).symm

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