concreteCategory — Mathlib

English

There is a canonical concrete category structure on HopfAlgCat R, with hom-sets given by the underlying BialgHom' between carriers.

Русский

Существует каноническая структура конкретной категории на HopfAlgCat R, где множества морфизмов совпадают с соответствующими BialgHom' между носителями.

LaTeX

$$$\text{HopfAlgCat concreteCategory } \Longrightarrow \text{ hom } f = f^{\mathrm{toBialgHom}'}$$$

Lean4

instance concreteCategory : ConcreteCategory (HopfAlgCat.{v} R) (· →ₐc[R] ·)
    where
  hom f := f.toBialgHom'
  ofHom f := ⟨f⟩

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