preservesZeroMorphisms_of_iso — Mathlib

English

If F1 ≅ F2 as functors, then F2 preserves zero morphisms.

Русский

Если F1 и F2 изоморфны как функторы, то F2 сохраняет нулевые морфизмы.

LaTeX

$$$F_1 \cong F_2 \Rightarrow \PreservesZeroMorphisms F_2$$$

Lean4

theorem preservesZeroMorphisms_of_iso {F₁ F₂ : C ⥤ D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) :
    F₂.PreservesZeroMorphisms where
  map_zero X Y := by simp only [← cancel_epi (e.hom.app X), ← e.hom.naturality, F₁.map_zero, zero_comp, comp_zero]

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