limitConeIsLimit

Mathlib.CategoryTheory.Category.Cat.Limit

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

Lean4

/-- Auxiliary definition: the proposed cone is a limit cone. -/
def limitConeIsLimit (F : J ⥤ Cat.{v, v}) : IsLimit (limitCone F)
    where
  lift := limitConeLift F
  fac s
    j :=
    CategoryTheory.Functor.ext (by simp) fun X Y f =>
      by
      dsimp [limitConeLift]
      exact Types.Limit.π_mk.{v, v} _ _ _ _
  uniq s m
    w := by
    symm
    refine CategoryTheory.Functor.ext ?_ ?_
    · intro X
      apply Types.limit_ext.{v, v}
      intro j
      simp [← w j]
    · intro X Y f
      simp [fun j => Functor.congr_hom (w j).symm f]

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

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

Разделы

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

Аффилиация

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