English
If X and Y are commutative rings carrying R-bialgebra structures, and f is a BialgHom from X to Y, then there exists a morphism in CommBialgCat(R) from of R X to of R Y corresponding to f.
Русский
Пусть X и Y — кольца с структурами биалгебр над R, и f является гомоморфизмом биалгебры от X к Y; тогда существует морфизм в категории CommBialgCat(R) from of R X к of R Y, соответствующий f.
LaTeX
$$$\forall X,Y,\ f : X \to_{R}^{\mathrm{bialg}} Y \implies \mathrm{ofHom}(f) : \mathrm{of}\,R X \to \mathrm{of}\,R Y.$$$
Lean4
/-- Typecheck a `BialgHom` as a morphism in `CommBialgCat R`. -/
abbrev ofHom {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Bialgebra R X} {_ : Bialgebra R Y} (f : X →ₐc[R] Y) :
of R X ⟶ of R Y :=
ConcreteCategory.ofHom (C := CommBialgCat R) f
