isColimitEvalMapCoconeCofan

Mathlib.CategoryTheory.Limits.FormalCoproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.FormalCoproduct.isColimitEvalMapCoconeCofan

Lean4

/-- `eval(F)` preserves arbitrary coproducts. -/
def isColimitEvalMapCoconeCofan : IsColimit (((eval.{w} C A).obj F).mapCocone (cofan.{w} J f))
    where
  desc s := Sigma.desc fun i ↦ Sigma.ι (F.obj ∘ (f i.1).obj) i.2 ≫ s.ι.app ⟨i.1⟩
  fac s i := Sigma.hom_ext _ _ fun i ↦ by simp [cofan, Function.comp_def]
  uniq s m h := Sigma.hom_ext _ _ fun ⟨i₁, i₂⟩ ↦ by simp [← h, cofan, Function.comp_def]

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

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

Разделы

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

Аффилиация

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