hasForgetToBialgebra — Mathlib

English

There exists a forgetful functor from HopfAlgCat R to BialgCat R, which sends a Hopf algebra to its underlying bialgebra and a Hopf-algebra morphism to the corresponding bialgebra homomorphism.

Русский

Существует функтор забывания из HopfAlgCat R в BialgCat R, который переводит Hopf-алгебру в соответствующую ей биалгебру и отображает морфизмы HopfAlgCat в соответствующие биалгеброгомоморфизмы.

LaTeX

$$$$ (forget_{ HopfAlgCat \\, R \\rightarrow BialgCat R}).obj(X) = \\mathrm{BialgCat.of}_{R}(X), \\quad (forget)_{\} (f) = f^{toBialgHom}. $$$$

Lean4

instance hasForgetToBialgebra : HasForget₂ (HopfAlgCat R) (BialgCat R) where
  forget₂ :=
    { obj := fun X => BialgCat.of R X
      map := fun {_ _} f => BialgCat.ofHom f.toBialgHom }

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