endMonoidalStarFunctor

Mathlib.CategoryTheory.Bicategory.SingleObj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor

Lean4

/-- The monoidal functor from the endomorphisms of the single object
when we promote a monoidal category to a single object bicategory,
to the original monoidal category.

We subsequently show this is an equivalence.
-/
@[simps]
def endMonoidalStarFunctor : (EndMonoidal (MonoidalSingleObj.star C)) ⥤ C
    where
  obj X := X
  map f := f

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru