English
Tensoring the polynomial algebra on the left by an R-algebra A yields an algebraic equivalence with the polynomial algebra over A: A ⊗_R MvPolynomial(σ, R) ≃_A MvPolynomial(σ, A).
Русский
Тензоризация слева полиномной алгебры по R на A даёт алгебраическое эквивалищество с полиномной алгеброй над A: A ⊗_R MvPolynomial(σ, R) ≃_A MvPolynomial(σ, A).
LaTeX
$$$ A \\otimes_R MvPolynomial(\\sigma, R) \\cong_A MvPolynomial(\\sigma, A) $$$
Lean4
/-- Tensoring `MvPolynomial σ R` on the left by an `R`-algebra `A` is algebraically
equivalent to `MvPolynomial σ A`. -/
noncomputable def algebraTensorAlgEquiv : A ⊗[R] MvPolynomial σ R ≃ₐ[A] MvPolynomial σ A :=
AlgEquiv.ofAlgHom
(Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (MvPolynomial.mapAlgHom <| Algebra.ofId R A)
(fun _ _ ↦ Commute.all _ _))
(aeval (fun s ↦ 1 ⊗ₜ X s)) (by ext s; simp) (by ext s; simp)
