isLimitRaiseCone

Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CostructuredArrow.CreatesConnected.isLimitRaiseCone

Lean4

/-- (Implementation) Show that the raised cone is a limit. -/
def isLimitRaiseCone [IsConnected J] {B : D} {F : J ⥤ CostructuredArrow K B} {c : Cone (F ⋙ CostructuredArrow.proj K B)}
    (t : IsLimit c) : IsLimit (raiseCone c)
    where
  lift
    s := CostructuredArrow.homMk (t.lift ((CostructuredArrow.proj K B).mapCone s)) <| by simp [← Functor.map_comp_assoc]
  uniq s m
    K := by
    ext1
    apply t.hom_ext
    intro j
    simp [← K j]

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

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

Разделы

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

Аффилиация

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