coneOfConeEvalIsLimit

Mathlib.CategoryTheory.Limits.Pi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.pi.coneOfConeEvalIsLimit

Lean4

/-- Given a family of limit cones over the `F ⋙ Pi.eval C i`,
assembling them together as a `Cone F` produces a limit cone.
-/
def coneOfConeEvalIsLimit {c : ∀ i, Cone (F ⋙ Pi.eval C i)} (P : ∀ i, IsLimit (c i)) : IsLimit (coneOfConeCompEval c)
    where
  lift s i := (P i).lift (coneCompEval s i)
  fac s
    j := by
    funext i
    exact (P i).fac (coneCompEval s i) j
  uniq s m
    w := by
    funext i
    exact (P i).uniq (coneCompEval s i) (m i) fun j => congr_fun (w j) i

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

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

Разделы

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

Аффилиация

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