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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasKernel (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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
this : HasKernel (G.map (F.map f) ≫ i.hom.app Y✝)
⊢ HasKernel (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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasKernel (i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝)
haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
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
inst✝ : PreservesFiniteLimits G
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
this : HasKernel (G.map (F.map f) ≫ i.hom.app Y✝)
⊢ HasKernel (i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝)
apply Limits.hasKernel_iso_comp