functorEnrichedOrdinaryCategory

Mathlib.CategoryTheory.Enriched.FunctorCategory

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

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 functorEnrichedOrdinaryCategory [∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom V F₁ F₂]
    [∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom V F₁ F₂] : EnrichedOrdinaryCategory (J ⥤ V) (J ⥤ C)
    where
  homEquiv := functorHomEquiv V
  homEquiv_id F := functorHomEquiv_id V F
  homEquiv_comp f g := functorHomEquiv_comp V f g

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

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

Разделы

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

Аффилиация

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