isZero_iff — Mathlib

English

A functor F is zero iff each component F(X) is a zero object in the target.

Русский

Функтор F нулевой тогда и только тогда, когда каждый компонент F(X) является нулевым объектом в целевом категории.

LaTeX

$$$IsZero F \\iff \\forall X, IsZero(F(X))$$$

Lean4

theorem isZero_iff [HasZeroObject D] (F : C ⥤ D) : IsZero F ↔ ∀ X, IsZero (F.obj X) :=
  ⟨fun hF X => hF.obj X, Functor.isZero _⟩

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