instConcreteCategoryBialgHomCarrier

English

There is a canonical ConcreteCategory structure on CommBialgCat with Hom given by BialgHom R X Y and the carrier functor mapping to the base carrier.

Русский

Существует каноническая структура ConcreteCategory на CommBialgCat, где морфизмы заданы BialgHom R X Y, а базовая функторная карта соответствует носителю.

LaTeX

$$$ \text{ConcreteCategory}(\mathrm{CommBialgCat}\,R) \,\big(\mathrm{Hom}(X,Y) = \mathrm{BialgHom\ } R X Y\big), \; \text{with } \mathrm{Hom\,carrier}(\text{...}) = X. $$$

Lean4

instance : ConcreteCategory (CommBialgCat.{v} R) (· →ₐc[R] ·)
    where
  hom := Hom.hom'
  ofHom := Hom.mk

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