functorEnrichedCategory

Mathlib.CategoryTheory.Enriched.FunctorCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Enriched.FunctorCategory.functorEnrichedCategory

Lean4

/-- If `C` is a `V`-enriched ordinary category, and `C` has suitable limits,
then `J ⥤ C` is also a `J ⥤ V`-enriched ordinary category. -/
noncomputable def functorEnrichedCategory [∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom V F₁ F₂] :
    EnrichedCategory (J ⥤ V) (J ⥤ C) where
  Hom F₁ F₂ := functorEnrichedHom V F₁ F₂
  id F := functorEnrichedId V F
  comp F₁ F₂ F₃ := functorEnrichedComp V F₁ F₂ F₃
  assoc F₁ F₂ F₃ F₄ := functorEnriched_assoc V F₁ F₂ F₃ F₄

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

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

Разделы

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

Аффилиация

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