English
For X and Y objects in the category of R-bialgebras, every morphism f in the category is accompanied by an underlying BialgHom between the underlying carriers; this correspondence is given by forgetting the extraneous categorical structure.
Русский
Для объектов X и Y в категории биалгебр над R каждый морфизм f в этой категории сопровождается соответствием между базовыми носителями — подложными биалгебровыми гомоморфизмами; это соответствие достигается путем забывания дополнительной категориальной структуры.
LaTeX
$$$toBialgHom(f) : \mathrm{BialgHom}(R, X.c, Y.c)$$$
Lean4
/-- Turn a morphism in `BialgCat` back into a `BialgHom`. -/
abbrev toBialgHom {X Y : BialgCat R} (f : Hom X Y) :=
ConcreteCategory.hom (C := BialgCat R) f
