category

Mathlib.CategoryTheory.Functor.Category

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

Lean4

/-- `Functor.category C D` gives the category structure on functors and natural transformations
between categories `C` and `D`.

Notice that if `C` and `D` are both small categories at the same universe level,
this is another small category at that level.
However if `C` and `D` are both large categories at the same universe level,
this is a small category at the next higher level.
-/
instance category : Category.{max u₁ v₂} (C ⥤ D)
    where
  Hom F G := NatTrans F G
  id F := NatTrans.id F
  comp α β := vcomp α β

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

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

Разделы

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

Аффилиация

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