isColimit

Mathlib.Topology.Category.CompHausLike.Limits

URI: https://scilib.ai/kg/mathlib#CompHausLike.finiteCoproduct.isColimit

Lean4

/-- The explicit finite coproduct cocone is a colimit cocone. -/
def isColimit : Limits.IsColimit (finiteCoproduct.cofan X) :=
  mkCofanColimit _ (fun s ↦ desc _ fun a ↦ s.inj a) (fun _ _ ↦ ι_desc _ _ _) fun _ _ hm ↦
    finiteCoproduct.hom_ext _ _ _ fun a ↦ (ConcreteCategory.hom_ext _ _ fun t ↦ congrFun (congrArg _ (hm a)) t)

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

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

Разделы

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

Аффилиация

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