V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (imageToKernel f 0 (_ : f ≫ 0 = 0))
⊢ Epi f
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
⊢ Epi f
have e₁ := h.epi
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
⊢ Epi f
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (imageToKernel f 0 (_ : f ≫ 0 = 0))
⊢ Epi f
rw [imageToKernel_zero_right] at e₁
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ :
  Epi
    ((Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0))
⊢ Epi f
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
⊢ Epi f
have e₂ : Epi (((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow) ≫
      (kernelSubobject 0).arrow) := @epi_comp _ _ _ _ _ _ e₁ _ _
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi (Subobject.arrow (imageSubobject f))
⊢ Epi f
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ :
  Epi
    ((Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0))
⊢ Epi f
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id] at e₂
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi ((imageSubobjectIso f).hom ≫ image.ι f)
⊢ Epi f
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi (Subobject.arrow (imageSubobject f))
⊢ Epi f
rw [← imageSubobject_arrow] at e₂
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi ((imageSubobjectIso f).hom ≫ image.ι f)
this : Epi (image.ι f)
⊢ Epi f
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi ((imageSubobjectIso f).hom ≫ image.ι f)
⊢ Epi f
haveI : Epi (image.ι f) := epi_of_epi (imageSubobjectIso f).hom (image.ι f)
no goals
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi ((imageSubobjectIso f).hom ≫ image.ι f)
this : Epi (image.ι f)
⊢ Epi f
apply epi_of_epi_image