English
There is an algebra isomorphism between the symmetric algebra of a free R-module M and the multivariate polynomial algebra MvPolynomial κ R, given a basis b of M.
Русский
Существует алгебраическое изоморфизм между симметрической алгеброй свободного R-модуля M и многочленной алгеброй MvPolynomial κ R, заданный на базе b.
LaTeX
$$$\operatorname{equivMvPolynomial}\;b:\operatorname{Sym}_R(M) \cong_R \operatorname{MvPolynomial}_\kappa R$$$
Lean4
/-- `SymmetricAlgebra.equivMvPolynomial` gives an algebra isomorphism between the symmetric algebra
over a free module and multivariate polynomials over a basis. This is analogous to
`TensorAlgebra.equivFreeAlgebra`. -/
noncomputable def equivMvPolynomial (b : Basis κ R M) : SymmetricAlgebra R M ≃ₐ[R] MvPolynomial κ R :=
.ofAlgHom (SymmetricAlgebra.lift <| Basis.constr b R .X) (MvPolynomial.aeval fun i ↦ ι R M (b i))
(MvPolynomial.algHom_ext fun i ↦ by simp) (algHom_ext <| b.ext fun i ↦ by simp)
