C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : L.map (𝟙 0) ≫ L.map (𝟙 0) = 0
⊢ PreservesZeroMorphisms L
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
⊢ PreservesZeroMorphisms L
replace h := (h (exact_of_zero (𝟙 0) (𝟙 0))).w
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : 𝟙 (L.obj 0) = 0
⊢ PreservesZeroMorphisms L
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : L.map (𝟙 0) ≫ L.map (𝟙 0) = 0
⊢ PreservesZeroMorphisms L
rw [L.map_id, Category.comp_id] at h
no goals
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : 𝟙 (L.obj 0) = 0
⊢ PreservesZeroMorphisms L
exact preservesZeroMorphisms_of_map_zero_object (idZeroEquivIsoZero _ h)