map_isZero — Mathlib

English

If X is a zero object, then F.obj X is a zero object for any F that preserves zero morphisms.

Русский

Если X является нулевым объектом, то F(X) является нулевым объектом для любого F, сохраняющего нулевые морфизмы.

LaTeX

$$$X \text{ isZero } \Rightarrow F( X ) \text{ isZero }$$$

Lean4

theorem map_isZero (F : C ⥤ D) [PreservesZeroMorphisms F] {X : C} (hX : IsZero X) : IsZero (F.obj X) :=
  by
  simp only [IsZero.iff_id_eq_zero] at hX ⊢
  rw [← F.map_id, hX, F.map_zero]

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