instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom

English

If f: A →𝖼[R] B is a bialgebra morphism between commutative algebras A and B, then the induced map on opposites CommAlgCat.ofHom (f) is a monoid hom in the opposite setting.

Русский

Пусть f: A →ᴄ[R] B — гомоморфизм биальгебр между коммутативными алгебрами A и B. Тогда индуцированный переход на противоположности CommAlgCat.ofHom(f) является моноидным гомом.

LaTeX

$$$\\text{IsMonHom}((\\mathrm{CommAlgCat.ofHom}(f)).\\mathrm{op})$$$

Lean4

instance {A B : Type u} [CommRing A] [Bialgebra R A] [CommRing B] [Bialgebra R B] (f : A →ₐc[R] B) :
    IsMonHom (CommAlgCat.ofHom (f : A →ₐ[R] B)).op where

Похожие утверждения