English
There is an algebra isomorphism between MvPolynomial (S1 ⊕ S2) R and MvPolynomial S1 (MvPolynomial S2 R).
Русский
Существует изоморфизм алгебр между MvPolynomial(S1⊕S2) R и MvPolynomial S1 (MvPolynomial S2 R).
LaTeX
$$$\text{sumAlgEquiv} : MvPolynomial (S_1 \oplus S_2)\,R \simeq_{R} MvPolynomial S_1 (MvPolynomial S_2 R)$$$
Lean4
/-- The algebra isomorphism between multivariable polynomials in a sum of two types,
and multivariable polynomials in one of the types,
with coefficients in multivariable polynomials in the other type.
-/
@[simps!]
def sumAlgEquiv : MvPolynomial (S₁ ⊕ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R) :=
{ sumRingEquiv R S₁ S₂ with
commutes' := by
intro r
have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) :) := rfl
have B : algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) r = C r := rfl
simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe, Equiv.coe_fn_mk, B, sumToIter_C, A] }
