English
There is a canonical algebra isomorphism between the mv-polynomial algebra in S1 ⊕ S2 and the mv-polynomial algebra in S2 with coefficients in mv-polynomials over S1.
Русский
Существует канонический изоморфизм алгебр между mv-многочленами над разбиением S1 ⊕ S2 и mv-многочленами S2 с коэффициентами в mv-многочленах над S1.
LaTeX
$$$\text{commAlgEquiv} : MvPolynomial S_1 (MvPolynomial S_2 R) \simeq_{R} MvPolynomial S_2 (MvPolynomial S_1 R)$$$
Lean4
/-- The algebra isomorphism between multivariable polynomials in variables `S₁` of multivariable
polynomials in variables `S₂` and multivariable polynomials in variables `S₂` of multivariable
polynomials in variables `S₁`. -/
noncomputable def commAlgEquiv : MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R) :=
(sumAlgEquiv R S₁ S₂).symm.trans <| (renameEquiv _ (.sumComm S₁ S₂)).trans (sumAlgEquiv R S₂ S₁)
