isZero_pt — Mathlib

English

In a category with zero morphisms, if c is a cocone for F: D ⥤ C that is a colimit and F is the zero functor, then c.pt is a zero object of C.

Русский

В категории с нулевыми морфизмами, если c — коконус над F: D ⥤ C является ко-пределом и F — ноль-функтор, то с.pt — нулевой объект.

LaTeX

$$IsColimit c ∧ IsZero F ⇒ IsZero c.pt$$

Lean4

theorem isZero_pt {c : Cocone F} (hc : IsColimit c) (hF : IsZero F) : IsZero c.pt :=
  (isZero_zero C).of_iso (IsColimit.coconePointUniqueUpToIso hc (IsColimit.ofIsZero (Cocone.mk 0 0) hF (isZero_zero C)))

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