instCategoryLimitCompObjects

Mathlib.CategoryTheory.Category.Cat.Limit

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects

Lean4

@[simps]
instance (F : J ⥤ Cat.{v, v}) : Category (limit (F ⋙ Cat.objects))
    where
  Hom X Y := limit (homDiagram X Y)
  id X := Types.Limit.mk.{v, v} (homDiagram X X) (fun _ => 𝟙 _) fun j j' f => by simp
  comp {X Y Z} f
    g :=
    Types.Limit.mk.{v, v} (homDiagram X Z) (fun j => limit.π (homDiagram X Y) j f ≫ limit.π (homDiagram Y Z) j g)
      fun j j' h => by simp [← congr_fun (limit.w (homDiagram X Y) h) f, ← congr_fun (limit.w (homDiagram Y Z) h) g]
  id_comp
    _ := by
    apply Types.limit_ext.{v, v}
    simp
  comp_id
    _ := by
    apply Types.limit_ext.{v, v}
    simp

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

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

Разделы

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

Аффилиация

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