obj — Mathlib

English

If F: C ⥤ D is a zero functor and D has a zero object, then for every X, F.obj X is zero.

Русский

Если F: C ⥤ D требует нулевой функтор, и D имеет нулевой объект, то для каждого X объект F(X) нулевой.

LaTeX

$$$[HasZeroObject\: D] \\Rightarrow (\\forall X, IsZero(F.obj X))$$$

Lean4

theorem obj [HasZeroObject D] {F : C ⥤ D} (hF : IsZero F) (X : C) : IsZero (F.obj X) :=
  by
  let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
  have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
  let e : F ≅ G := hF.iso hG
  exact (isZero_zero _).of_iso (e.app X)

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