[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} 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
[PROOFSTEP]
have := NatIso.naturality_1 i f
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} 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 : NatTrans.app i.inv X✝ ≫ (F ⋙ G).map f ≫ NatTrans.app i.hom Y✝ = (𝟭 C).map f
⊢ HasKernel f
[PROOFSTEP]
simp at this 
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} 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 : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasKernel f
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} 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 : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasKernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} 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✝ : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
this : HasKernel (G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
⊢ HasKernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
apply Limits.hasKernel_iso_comp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} 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
[PROOFSTEP]
have : PreservesColimits G := adj.leftAdjointPreservesColimits
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} 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
[PROOFSTEP]
have := NatIso.naturality_1 i f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} 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 : NatTrans.app i.inv X✝ ≫ (F ⋙ G).map f ≫ NatTrans.app i.hom Y✝ = (𝟭 C).map f
⊢ HasCokernel f
[PROOFSTEP]
simp at this 
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} 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 : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasCokernel f
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} 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 : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
⊢ HasCokernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v, u₂} 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✝ : NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝ = f
this : HasCokernel (G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
⊢ HasCokernel (NatTrans.app i.inv X✝ ≫ G.map (F.map f) ≫ NatTrans.app i.hom Y✝)
[PROOFSTEP]
apply Limits.hasCokernel_epi_comp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ G.obj (cokernel (F.map f)) ≅ cokernel f
[PROOFSTEP]
have : PreservesColimits G := adj.leftAdjointPreservesColimits
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ G.obj (cokernel (F.map f)) ≅ cokernel f
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ G.obj (cokernel (F.map f)) ≅ cokernel f
[PROOFSTEP]
calc
  G.obj (cokernel (F.map f)) ≅ cokernel (G.map (F.map f)) := (asIso (cokernelComparison _ G)).symm
  _ ≅ cokernel (i.hom.app X ≫ f ≫ i.inv.app Y) := (cokernelIsoOfEq (NatIso.naturality_2 i f).symm)
  _ ≅ cokernel (f ≫ i.inv.app Y) := (cokernelEpiComp (i.hom.app X) (f ≫ i.inv.app Y))
  _ ≅ cokernel f := cokernelCompIsIso f (i.inv.app Y)
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
⊢ kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π f)
[PROOFSTEP]
have : PreservesColimits G := adj.leftAdjointPreservesColimits
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π f)
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π f)
[PROOFSTEP]
calc
  kernel (G.map (cokernel.π (F.map f))) ≅ kernel (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G) :=
    kernelIsoOfEq (π_comp_cokernelComparison _ _).symm
  _ ≅ kernel (cokernel.π (G.map (F.map f))) := (kernelCompMono _ _)
  _ ≅ kernel (cokernel.π (_ ≫ f ≫ _) ≫ (cokernelIsoOfEq _).hom) :=
    (kernelIsoOfEq (π_comp_cokernelIsoOfEq_hom (NatIso.naturality_2 i f)).symm)
  _ ≅ kernel (cokernel.π (_ ≫ f ≫ _)) := (kernelCompMono _ _)
  _ ≅ kernel (cokernel.π (f ≫ i.inv.app Y) ≫ (cokernelEpiComp (i.hom.app X) _).inv) :=
    (kernelIsoOfEq (by simp only [cokernel.π_desc, cokernelEpiComp_inv]))
  _ ≅ kernel (cokernel.π (f ≫ _)) := (kernelCompMono _ _)
  _ ≅ kernel (inv (i.inv.app Y) ≫ cokernel.π f ≫ (cokernelCompIsIso f (i.inv.app Y)).inv) :=
    (kernelIsoOfEq
      (by simp only [cokernel.π_desc, cokernelCompIsIso_inv, Iso.hom_inv_id_app_assoc, NatIso.inv_inv_app]))
  _ ≅ kernel (cokernel.π f ≫ _) := (kernelIsIsoComp _ _)
  _ ≅ kernel (cokernel.π f) := kernelCompMono _ _
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
    cokernel.π (f ≫ NatTrans.app i.inv Y) ≫ (cokernelEpiComp (NatTrans.app i.hom X) (f ≫ NatTrans.app i.inv Y)).inv
[PROOFSTEP]
simp only [cokernel.π_desc, cokernelEpiComp_inv]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
D : Type u₂
inst✝⁵ : Category.{v, u₂} D
inst✝⁴ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝³ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝² : HasCokernels C
inst✝¹ : HasKernels C
inst✝ : PreservesFiniteLimits G
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ cokernel.π (f ≫ NatTrans.app i.inv Y) =
    inv (NatTrans.app i.inv Y) ≫ cokernel.π f ≫ (cokernelCompIsIso f (NatTrans.app i.inv Y)).inv
[PROOFSTEP]
simp only [cokernel.π_desc, cokernelCompIsIso_inv, Iso.hom_inv_id_app_assoc, NatIso.inv_inv_app]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
⊢ Abelian.coimage f ≅ Abelian.image f
[PROOFSTEP]
have : PreservesLimits F := adj.rightAdjointPreservesLimits
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this : PreservesLimits F
⊢ Abelian.coimage f ≅ Abelian.image f
[PROOFSTEP]
haveI : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝ : PreservesLimits F
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
⊢ Abelian.coimage f ≅ Abelian.image f
[PROOFSTEP]
calc
  Abelian.coimage f ≅ cokernel (kernel.ι f) := Iso.refl _
  _ ≅ G.obj (cokernel (F.map (kernel.ι f))) := (cokernelIso _ _ i adj _).symm
  _ ≅ G.obj (cokernel (kernelComparison f F ≫ kernel.ι (F.map f))) := (G.mapIso (cokernelIsoOfEq (by simp)))
  _ ≅ G.obj (cokernel (kernel.ι (F.map f))) := (G.mapIso (cokernelEpiComp _ _))
  _ ≅ G.obj (Abelian.coimage (F.map f)) := (Iso.refl _)
  _ ≅ G.obj (Abelian.image (F.map f)) := (G.mapIso (Abelian.coimageIsoImage _))
  _ ≅ G.obj (kernel (cokernel.π (F.map f))) := (Iso.refl _)
  _ ≅ kernel (G.map (cokernel.π (F.map f))) := (PreservesKernel.iso _ _)
  _ ≅ kernel (cokernel.π f) := (coimageIsoImageAux F G i adj f)
  _ ≅ Abelian.image f := Iso.refl _
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝ : PreservesLimits F
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
⊢ F.map (kernel.ι f) = kernelComparison f F ≫ kernel.ι (F.map f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝¹ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this✝ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
have : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasKernel f' := inferInstance
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝² : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this✝¹ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
this✝ : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasKernel f'
⊢ (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
[PROOFSTEP]
dsimp only [coimageIsoImage, Iso.instTransIso_trans, Iso.refl, Iso.trans, Iso.symm, Functor.mapIso, cokernelEpiComp,
  cokernelIso, cokernelCompIsIso_inv, asIso, coimageIsoImageAux, kernelCompMono]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v, u₁} C
inst✝⁷ : Preadditive C
D : Type u₂
inst✝⁶ : Category.{v, u₂} D
inst✝⁵ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝⁴ : Functor.PreservesZeroMorphisms G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
inst✝³ : HasCokernels C
inst✝² : HasKernels C
inst✝¹ : PreservesFiniteLimits G
inst✝ : Functor.PreservesZeroMorphisms F
X Y : C
f : X ⟶ Y
this✝² : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f'
this✝¹ : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasKernel f'
this✝ : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasCokernel f'
this : ∀ (X' Y' : D) (f' : X' ⟶ Y'), HasKernel f'
⊢ ((((((((𝟙 (Abelian.coimage f) ≫
                      cokernel.desc (kernel.ι f) (NatTrans.app i.inv X ≫ cokernel.π (kernel.ι f ≫ NatTrans.app i.inv X))
                          (_ : kernel.ι f ≫ NatTrans.app i.inv X ≫ cokernel.π (kernel.ι f ≫ NatTrans.app i.inv X) = 0) ≫
                        cokernel.desc (kernel.ι f ≫ NatTrans.app i.inv X)
                            (cokernel.π (NatTrans.app i.hom (kernel f) ≫ kernel.ι f ≫ NatTrans.app i.inv X))
                            (_ :
                              (kernel.ι f ≫ NatTrans.app i.inv X) ≫
                                  cokernel.π (NatTrans.app i.hom (kernel f) ≫ kernel.ι f ≫ NatTrans.app i.inv X) =
                                0) ≫
                          (cokernelIsoOfEq
                                (_ :
                                  (F ⋙ G).map (kernel.ι f) =
                                    NatTrans.app i.hom (kernel f) ≫
                                      (𝟭 C).map (kernel.ι f) ≫ NatTrans.app i.inv X)).inv ≫
                            cokernelComparison (F.map (kernel.ι f)) G) ≫
                    G.map (cokernelIsoOfEq (_ : F.map (kernel.ι f) = kernelComparison f F ≫ kernel.ι (F.map f))).hom) ≫
                  G.map
                    (cokernel.desc (kernelComparison f F ≫ kernel.ι (F.map f)) (cokernel.π (kernel.ι (F.map f)))
                      (_ : (kernelComparison f F ≫ kernel.ι (F.map f)) ≫ cokernel.π (kernel.ι (F.map f)) = 0))) ≫
                𝟙 (G.obj (cokernel (kernel.ι (F.map f))))) ≫
              G.map (Abelian.coimageIsoImage (F.map f)).hom) ≫
            𝟙 (G.obj (Abelian.image (F.map f)))) ≫
          (PreservesKernel.iso G (cokernel.π (F.map f))).hom) ≫
        ((((((((kernelIsoOfEq
                            (_ :
                              G.map (cokernel.π (F.map f)) =
                                cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G)).hom ≫
                        kernel.lift (cokernel.π (G.map (F.map f)))
                          (kernel.ι (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G))
                          (_ :
                            kernel.ι (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G) ≫
                                cokernel.π (G.map (F.map f)) =
                              0)) ≫
                      (kernelIsoOfEq
                          (_ :
                            cokernel.π ((F ⋙ G).map f) =
                              cokernel.π (NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y) ≫
                                (cokernelIsoOfEq
                                    (_ :
                                      NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y =
                                        (F ⋙ G).map f)).hom)).hom) ≫
                    kernel.lift (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                      (kernel.ι
                        (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) ≫
                          (cokernelIsoOfEq
                              (_ : NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y = (F ⋙ G).map f)).hom))
                      (_ :
                        kernel.ι
                              (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) ≫
                                (cokernelIsoOfEq
                                    (_ :
                                      NatTrans.app i.hom X ≫ (𝟭 C).map f ≫ NatTrans.app i.inv Y = (F ⋙ G).map f)).hom) ≫
                            cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                          0)) ≫
                  (kernelIsoOfEq
                      (_ :
                        cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                          cokernel.π (f ≫ NatTrans.app i.inv Y) ≫
                            cokernel.desc (f ≫ NatTrans.app i.inv Y)
                              (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                              (_ :
                                (f ≫ NatTrans.app i.inv Y) ≫
                                    cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                                  0))).hom) ≫
                kernel.lift (cokernel.π (f ≫ NatTrans.app i.inv Y))
                  (kernel.ι
                    (cokernel.π (f ≫ NatTrans.app i.inv Y) ≫
                      cokernel.desc (f ≫ NatTrans.app i.inv Y)
                        (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                        (_ :
                          (f ≫ NatTrans.app i.inv Y) ≫ cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                            0)))
                  (_ :
                    kernel.ι
                          (cokernel.π (f ≫ NatTrans.app i.inv Y) ≫
                            cokernel.desc (f ≫ NatTrans.app i.inv Y)
                              (cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y))
                              (_ :
                                (f ≫ NatTrans.app i.inv Y) ≫
                                    cokernel.π (NatTrans.app i.hom X ≫ f ≫ NatTrans.app i.inv Y) =
                                  0)) ≫
                        cokernel.π (f ≫ NatTrans.app i.inv Y) =
                      0)) ≫
              (kernelIsoOfEq
                  (_ :
                    cokernel.π (f ≫ NatTrans.app i.inv Y) =
                      inv (NatTrans.app i.inv Y) ≫
                        cokernel.π f ≫
                          cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                            (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0))).hom) ≫
            (kernelIsIsoComp (inv (NatTrans.app i.inv Y))
                (cokernel.π f ≫
                  cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                    (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0))).hom) ≫
          kernel.lift (cokernel.π f)
            (kernel.ι
              (cokernel.π f ≫
                cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                  (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0)))
            (_ :
              kernel.ι
                    (cokernel.π f ≫
                      cokernel.desc f (NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y))
                        (_ : f ≫ NatTrans.app i.inv Y ≫ cokernel.π (f ≫ NatTrans.app i.inv Y) = 0)) ≫
                  cokernel.π f =
                0)) ≫
      𝟙 (kernel (cokernel.π f)) =
    Abelian.coimageImageComparison f
[PROOFSTEP]
simpa only [← cancel_mono (Abelian.image.ι f), ← cancel_epi (Abelian.coimage.π f), Category.assoc, Category.id_comp,
  cokernel.π_desc_assoc, π_comp_cokernelIsoOfEq_inv_assoc, PreservesKernel.iso_hom, π_comp_cokernelComparison_assoc, ←
  G.map_comp_assoc, kernel.lift_ι, Abelian.coimage_image_factorisation, lift_comp_kernelIsoOfEq_hom_assoc,
  kernelIsIsoComp_hom, kernel.lift_ι_assoc, kernelIsoOfEq_hom_comp_ι_assoc, kernelComparison_comp_ι_assoc,
  π_comp_cokernelIsoOfEq_hom_assoc, asIso_hom, NatIso.inv_inv_app] using NatIso.naturality_1 i f
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
⊢ Abelian C
[PROOFSTEP]
haveI := hasKernels F G i
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this : HasKernels C
⊢ Abelian C
[PROOFSTEP]
haveI := hasCokernels F G i adj
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
⊢ Abelian C
[PROOFSTEP]
have : ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f) :=
  by
  intro X Y f
  rw [← coimageIsoImage_hom F G i adj f]
  infer_instance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
⊢ ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f)
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ IsIso (Abelian.coimageImageComparison f)
[PROOFSTEP]
rw [← coimageIsoImage_hom F G i adj f]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ IsIso (coimageIsoImage F G i adj f).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v, u₁} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasFiniteProducts C
D : Type u₂
inst✝⁴ : Category.{v, u₂} D
inst✝³ : Abelian D
F : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms F
G : D ⥤ C
inst✝¹ : Functor.PreservesZeroMorphisms G
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝¹ : HasKernels C
this✝ : HasCokernels C
this : ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f)
⊢ Abelian C
[PROOFSTEP]
apply Abelian.ofCoimageImageComparisonIsIso
