V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ homology f g (_ : f ≫ g = 0) ≅ 0
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : Exact f g
⊢ homology f g (_ : f ≫ g = 0) ≅ 0
haveI := h.epi
no goals
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ homology f g (_ : f ≫ g = 0) ≅ 0
exact cokernel.ofEpi _
case intro.intro
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
i : homology f g w ≅ 0
⊢ Exact f g
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : ∃ w, Nonempty (homology f g w ≅ 0)
⊢ Exact f g
obtain ⟨w, ⟨i⟩⟩ := h
no goals
case intro.intro
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
i : homology f g w ≅ 0
⊢ Exact f g
exact ⟨w, Preadditive.epi_of_cokernel_zero ((cancel_mono i.hom).mp (by ext))⟩
no goals
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
i : homology f g w ≅ 0
⊢ cokernel.π (imageToKernel f g w) ≫ i.hom = 0 ≫ i.hom
ext