[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
f : X ⟶ Y
⊢ f = 0 → F.map f = 0
[PROOFSTEP]
rintro rfl
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
⊢ F.map 0 = 0
[PROOFSTEP]
exact F.map_zero _ _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
⊢ F.map 0 = 0
[PROOFSTEP]
let adj := Adjunction.ofLeftAdjoint F
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 = 0
[PROOFSTEP]
calc
  F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
  _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
  _ = 0 := ?_
[GOAL]
case calc_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ F.map (NatTrans.app adj.unit Y) ≫ NatTrans.app adj.counit (F.obj Y)
[PROOFSTEP]
rw [Adjunction.left_triangle_components]
[GOAL]
case calc_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ 𝟙 (F.obj Y)
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
case calc_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 ≫ F.map (NatTrans.app adj.unit Y) ≫ NatTrans.app adj.counit (F.obj Y) =
    F.map 0 ≫ F.map ((rightAdjoint F).map 0) ≫ NatTrans.app adj.counit (F.obj Y)
[PROOFSTEP]
simp only [← Category.assoc, ← F.map_comp, zero_comp]
[GOAL]
case calc_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 ≫ F.map ((rightAdjoint F).map 0) ≫ NatTrans.app adj.counit (F.obj Y) = 0
[PROOFSTEP]
simp only [Adjunction.counit_naturality, comp_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
⊢ G.map 0 = 0
[PROOFSTEP]
let adj := Adjunction.ofRightAdjoint G
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ G.map 0 = 0
[PROOFSTEP]
calc
  G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
  _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
  _ = 0 := ?_
[GOAL]
case calc_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ G.map 0 = NatTrans.app adj.unit (G.obj X) ≫ G.map (NatTrans.app adj.counit X) ≫ G.map 0
[PROOFSTEP]
rw [Adjunction.right_triangle_components_assoc]
[GOAL]
case calc_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ NatTrans.app adj.unit (G.obj X) ≫ G.map (NatTrans.app adj.counit X) ≫ G.map 0 =
    NatTrans.app adj.unit (G.obj X) ≫ G.map ((leftAdjoint G).map 0) ≫ G.map 0
[PROOFSTEP]
simp only [← G.map_comp, comp_zero]
[GOAL]
case calc_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ NatTrans.app adj.unit (G.obj X) ≫ G.map ((leftAdjoint G).map 0) ≫ G.map 0 = 0
[PROOFSTEP]
simp only [id_obj, comp_obj, Adjunction.unit_naturality_assoc, zero_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Full F
X Y : C
⊢ F.map 0 = F.map (0 ≫ F.preimage 0)
[PROOFSTEP]
rw [zero_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Full F
X Y : C
⊢ F.map (0 ≫ F.preimage 0) = 0
[PROOFSTEP]
rw [F.map_comp, F.image_preimage, comp_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
⊢ 0 ≫ 0 = 𝟙 (F.obj 0)
[PROOFSTEP]
rw [← F.map_id, id_zero, F.map_zero, zero_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
⊢ 0 ≫ 0 = 𝟙 0
[PROOFSTEP]
rw [id_zero, comp_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map 0 ≫ F.map 0
[PROOFSTEP]
rw [← Functor.map_comp, comp_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0
[PROOFSTEP]
rw [Iso.hom_inv_id, Category.id_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 = 0
[PROOFSTEP]
simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]
