limitCone

Mathlib.Algebra.Homology.ShortComplex.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.limitCone

Lean4

/-- Construction of a limit cone for a functor `J ⥤ ShortComplex C` using the limits
of the three components `J ⥤ C`. -/
noncomputable def limitCone : Cone F :=
  Cone.mk (ShortComplex.mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃)) (by cat_disch))
    { app := fun j => Hom.mk (limit.π _ _) (limit.π _ _) (limit.π _ _) (by simp) (by simp)
      naturality := fun _ _ f => by ext <;> simp [← limit.w _ f] }

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

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

Разделы

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

Аффилиация

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