forget₂_bialgebra_map — Mathlib

English

For objects X, Y in HopfAlgCat R and a morphism f: X ⟶ Y, the forgetful functor sends f to the corresponding bialgebra homomorphism f.toBialgHom.

Русский

Для объектов X, Y в HopfAlgCat R и морфизма f: X ⟶ Y, функтор забывания переводит f в соответствующий биалгеброгомоморфизм f.toBialgHom.

LaTeX

$$$$ (forget_{ HopfAlgCat \\; R})\\, .map\\, f = BialgCat.ofHom (f.toBialgHom). $$$$

Lean4

@[simp]
theorem forget₂_bialgebra_map (X Y : HopfAlgCat R) (f : X ⟶ Y) :
    (forget₂ (HopfAlgCat R) (BialgCat R)).map f = BialgCat.ofHom f.toBialgHom :=
  rfl

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