ofIsZero

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsColimit.ofIsZero

Lean4

/-- If a functor `F` is zero, then any cocone for `F` with a zero point is colimit. -/
def ofIsZero (c : Cocone F) (hF : IsZero F) (hc : IsZero c.pt) : IsColimit c
    where
  desc _ := 0
  fac _ j := (F.isZero_iff.1 hF j).eq_of_src _ _
  uniq _ _ _ := hc.eq_of_src _ _

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

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

Разделы

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

Аффилиация

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