English
Given suitable ring homomorphisms f and g between mv-polynomials on S1 and S2 S3 with appropriate inverses on C and X, there exists a RingEquiv between MvPolynomial S1 R and MvPolynomial S2 S3 implementing this duality.
Русский
При наличии подходящих кольцевых однородных отображений f и g между mv-многочленами на S1 и S2 S3 с соответствующими обратными на C и X существует кольцевой эквивалент между MvPolynomial S1 R и MvPolynomial S2 S3, реализующий эту двойственность.
LaTeX
$$$\exists\text{ RingEquiv } f,g:\ MvPolynomial S1\,R \to MvPolynomial S2\,S3\,R \text{ с условиями } (f\circ g)\circ C = C, \ f(g(X(n))) = X(n) \ldots$$$
Lean4
/-- A helper function for `sumRingEquiv`. -/
@[simps]
def mvPolynomialEquivMvPolynomial [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃)
(g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp C = C) (hfgX : ∀ n, f (g (X n)) = X n)
(hgfC : (g.comp f).comp C = C) (hgfX : ∀ n, g (f (X n)) = X n) : MvPolynomial S₁ R ≃+* MvPolynomial S₂ S₃
where
toFun := f
invFun := g
left_inv := is_id (RingHom.comp _ _) hgfC hgfX
right_inv := is_id (RingHom.comp _ _) hfgC hfgX
map_mul' := f.map_mul
map_add' := f.map_add
