functorCategoryMonoidalClosed

Mathlib.CategoryTheory.Closed.FunctorCategory.Complete

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.functorCategoryMonoidalClosed

Lean4

/-- Assuming the existence of certain limits, functors into a monoidal closed category form a
monoidal closed category.

Note: this is defined completely abstractly, and does not have any good definitional properties.
See the TODO in the module docstring.
-/
def functorCategoryMonoidalClosed : MonoidalClosed (I ⥤ C) where closed F := functorCategoryClosed I C F

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

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

Разделы

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

Аффилиация

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