coconeOfCoconeEvalIsColimit

Mathlib.CategoryTheory.Limits.Pi

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

Lean4

/-- Given a family of colimit cocones over the `F ⋙ Pi.eval C i`,
assembling them together as a `Cocone F` produces a colimit cocone.
-/
def coconeOfCoconeEvalIsColimit {c : ∀ i, Cocone (F ⋙ Pi.eval C i)} (P : ∀ i, IsColimit (c i)) :
    IsColimit (coconeOfCoconeCompEval c)
    where
  desc s i := (P i).desc (coconeCompEval s i)
  fac s
    j := by
    funext i
    exact (P i).fac (coconeCompEval s i) j
  uniq s m
    w := by
    funext i
    exact (P i).uniq (coconeCompEval s i) (m i) fun j => congr_fun (w j) i

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

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

Разделы

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

Аффилиация

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