English
There exists a ring isomorphism between polynomials with sum-type variables and polynomials where the sum splits into nested mv-polynomials: MvPolynomial (S1 ⊕ S2) R ≃+* MvPolynomial S1 (MvPolynomial S2 R).
Русский
Существует кольцевой изоморфизм между полиномами с переменными типа суммы и полиномами, где сумма распадается на вложенные mv-полиномы: MvPolynomial(S1 ⊕ S2) R ≃+* MvPolynomial S1 (MvPolynomial S2 R).
LaTeX
$$$\operatorname{sumRingEquiv} : MvPolynomial (S_1 \oplus S_2)\,R \simeq_{+*} MvPolynomial S_1 (MvPolynomial S_2 R)$$$
Lean4
/-- The ring 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.
-/
def sumRingEquiv : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) :=
by
apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
· refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)
case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
· simp [iterToSum_X, sumToIter_Xl]
· ext1; simp only [RingHom.comp_apply, sumToIter_C, iterToSum_C_C]
· rintro ⟨⟩ <;> simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]
