C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : PreservesColimits G
⊢ HasCokernel f
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ HasCokernel f
have : PreservesColimits G := adj.leftAdjointPreservesColimits
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasCokernel f
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : PreservesColimits G
⊢ HasCokernel f
have := NatIso.naturality_1 i f
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel f
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasCokernel f
simp at this
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel (i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝)
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel f
rw [← this]
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝¹ : PreservesColimits G
this✝ : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
this : HasCokernel (G.map (F.map f) ≫ i.hom.app Y✝)
⊢ HasCokernel (i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝)
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel (i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝)
haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
no goals
C : Type u₁
inst✝⁴ : Category C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝¹ : PreservesColimits G
this✝ : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
this : HasCokernel (G.map (F.map f) ≫ i.hom.app Y✝)
⊢ HasCokernel (i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝)
apply Limits.hasCokernel_epi_comp