[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} 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
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} 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
[PROOFSTEP]
exact cokernel.ofEpi _
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} 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
[PROOFSTEP]
obtain ⟨w, ⟨i⟩⟩ := h
[GOAL]
case intro.intro
V : Type u
inst✝⁵ : Category.{v, u} 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
[PROOFSTEP]
exact ⟨w, Preadditive.epi_of_cokernel_zero ((cancel_mono i.hom).mp (by ext))⟩
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} 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
[PROOFSTEP]
ext
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
⊢ Exact f₂ g₂
[PROOFSTEP]
rw [Preadditive.exact_iff_homology_zero] at h ⊢
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h✝ : Exact f₁ g₁
h : ∃ w, Nonempty (homology f₁ g₁ w ≅ 0)
⊢ ∃ w, Nonempty (homology f₂ g₂ w ≅ 0)
[PROOFSTEP]
rcases h with ⟨w₁, ⟨i⟩⟩
[GOAL]
case intro.intro
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ ∃ w, Nonempty (homology f₂ g₂ w ≅ 0)
[PROOFSTEP]
suffices w₂ : f₂ ≫ g₂ = 0
[GOAL]
case intro.intro
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
w₂ : f₂ ≫ g₂ = 0
⊢ ∃ w, Nonempty (homology f₂ g₂ w ≅ 0)
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ f₂ ≫ g₂ = 0
[PROOFSTEP]
exact ⟨w₂, ⟨(homology.mapIso w₁ w₂ α β p).symm.trans i⟩⟩
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ f₂ ≫ g₂ = 0
[PROOFSTEP]
rw [← cancel_epi α.hom.left, ← cancel_mono β.inv.right, comp_zero, zero_comp, ← w₁]
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
have eq₁ := β.inv.w
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
eq₁ : (𝟭 V).map β.inv.left ≫ (Arrow.mk g₁).hom = (Arrow.mk g₂).hom ≫ (𝟭 V).map β.inv.right
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
have eq₂ := α.hom.w
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
eq₁ : (𝟭 V).map β.inv.left ≫ (Arrow.mk g₁).hom = (Arrow.mk g₂).hom ≫ (𝟭 V).map β.inv.right
eq₂ : (𝟭 V).map α.hom.left ≫ (Arrow.mk f₂).hom = (Arrow.mk f₁).hom ≫ (𝟭 V).map α.hom.right
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
dsimp at eq₁ eq₂ 
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
eq₁ : β.inv.left ≫ g₁ = g₂ ≫ β.inv.right
eq₂ : α.hom.left ≫ f₂ = f₁ ≫ α.hom.right
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
simp only [Category.assoc, Category.assoc, ← eq₁, reassoc_of% eq₂, p, ← reassoc_of% (Arrow.comp_left β.hom β.inv),
  β.hom_inv_id, Arrow.id_left, Category.id_comp]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right = β.symm.hom.left
[PROOFSTEP]
rw [← cancel_mono α.hom.right]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right ≫ α.hom.right = β.symm.hom.left ≫ α.hom.right
[PROOFSTEP]
simp only [Iso.symm_hom, ← Arrow.comp_right, α.inv_hom_id]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ (𝟙 (Arrow.mk f₂)).right = β.inv.left ≫ α.hom.right
[PROOFSTEP]
simp only [p, ← Arrow.comp_left, Arrow.id_right, Arrow.id_left, Iso.inv_hom_id]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ 𝟙 (Arrow.mk f₂).right = 𝟙 (Arrow.mk g₂).left
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ f ≫ g = 0
[PROOFSTEP]
suffices Subobject.arrow (imageSubobject f) ≫ g = 0 by
  rw [← imageSubobject_arrow_comp f, Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
this : Subobject.arrow (imageSubobject f) ≫ g = 0
⊢ f ≫ g = 0
[PROOFSTEP]
rw [← imageSubobject_arrow_comp f, Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Subobject.arrow (imageSubobject f) ≫ g = 0
[PROOFSTEP]
rw [p, kernelSubobject_arrow_comp]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ IsIso (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
refine' ⟨⟨Subobject.ofLE _ _ p.ge, _⟩⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        imageToKernel f g (_ : f ≫ g = 0) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
[PROOFSTEP]
dsimp [imageToKernel]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
[PROOFSTEP]
simp only [Subobject.ofLE_comp_ofLE, Subobject.ofLE_refl]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
haveI := imageToKernel_isIso_of_image_eq_kernel f g p
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ Exact (f ≫ i.hom) (i.inv ≫ g)
[PROOFSTEP]
refine' ⟨by simp [h.w], _⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ (f ≫ i.hom) ≫ i.inv ≫ g = 0
[PROOFSTEP]
simp [h.w]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ Epi (imageToKernel (f ≫ i.hom) (i.inv ≫ g) (_ : (f ≫ i.hom) ≫ i.inv ≫ g = 0))
[PROOFSTEP]
rw [imageToKernel_comp_hom_inv_comp]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ Epi ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv)
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact (f ≫ i.hom) (i.inv ≫ g)
⊢ Exact f g
[PROOFSTEP]
simpa using exact_comp_inv_hom_comp i h
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ Exact (f ≫ g) h
[PROOFSTEP]
refine' ⟨by simp [hgh.w], _⟩
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ (f ≫ g) ≫ h = 0
[PROOFSTEP]
simp [hgh.w]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ Epi (imageToKernel (f ≫ g) h (_ : (f ≫ g) ≫ h = 0))
[PROOFSTEP]
rw [imageToKernel_comp_left]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)
case w
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ g ≫ h = 0
[PROOFSTEP]
haveI := hgh.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
this : Epi (imageToKernel g h (_ : g ≫ h = 0))
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)
case w
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ g ≫ h = 0
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact g h
[PROOFSTEP]
rw [← IsIso.inv_hom_id_assoc f g]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact (inv f ≫ f ≫ g) h
[PROOFSTEP]
exact exact_epi_comp w
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ Exact f (g ≫ h)
[PROOFSTEP]
refine' ⟨by simp [hfg.w_assoc], _⟩
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ f ≫ g ≫ h = 0
[PROOFSTEP]
simp [hfg.w_assoc]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
[PROOFSTEP]
rw [imageToKernel_comp_right f g h hfg.w]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h)))
[PROOFSTEP]
haveI := hfg.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h)))
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
⊢ Exact f (g ≫ h) ↔ Exact f g
[PROOFSTEP]
refine' ⟨fun hfg => ⟨zero_of_comp_mono h (by rw [Category.assoc, hfg.1]), _⟩, fun h => exact_comp_mono h⟩
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ (f ≫ g) ≫ h = 0
[PROOFSTEP]
rw [Category.assoc, hfg.1]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
rw [← (Iso.eq_comp_inv _).1 (imageToKernel_comp_mono _ _ h hfg.1)]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
[PROOFSTEP]
haveI := hfg.2
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
this : Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (Subobject.arrow (kernelSubobject f)) f
[PROOFSTEP]
refine' ⟨by simp, _⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Subobject.arrow (kernelSubobject f) ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Epi (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
[PROOFSTEP]
refine' @IsIso.epi_of_iso _ _ _ _ _ ?_
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ IsIso (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
[PROOFSTEP]
exact ⟨⟨factorThruImageSubobject _, by aesop_cat, by aesop_cat⟩⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0) ≫
      factorThruImageSubobject (Subobject.arrow (kernelSubobject f)) =
    𝟙 (Subobject.underlying.obj (imageSubobject (Subobject.arrow (kernelSubobject f))))
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ factorThruImageSubobject (Subobject.arrow (kernelSubobject f)) ≫
      imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0) =
    𝟙 (Subobject.underlying.obj (kernelSubobject f))
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (kernel.ι f) f
[PROOFSTEP]
rw [← kernelSubobject_arrow', exact_iso_comp]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (Subobject.arrow (kernelSubobject f)) f
[PROOFSTEP]
exact exact_kernelSubobject_arrow
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0))
[PROOFSTEP]
rw [← factorThruImageSubobject_comp_imageToKernel]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (factorThruImageSubobject f ≫ imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi (factorThruImageSubobject f ≫ imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
apply epi_comp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (kernel.lift g f (_ : f ≫ g = 0))
[PROOFSTEP]
rw [← factorThruKernelSubobject_comp_kernelSubobjectIso]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0) ≫ (kernelSubobjectIso g).hom)
[PROOFSTEP]
haveI := h.epi_factorThruKernelSubobject
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
this : Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0))
⊢ Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0) ≫ (kernelSubobjectIso g).hom)
[PROOFSTEP]
apply epi_comp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
⊢ Subobject.arrow (kernelSubobject g) = 0
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) = 0
[PROOFSTEP]
rw [← cancel_epi (imageToKernel (0 : A ⟶ B) g h.w), ← cancel_epi (factorThruImageSubobject (0 : A ⟶ B))]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ 0
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
⊢ kernel.ι g = 0
[PROOFSTEP]
rw [← kernelSubobject_arrow']
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
⊢ (kernelSubobjectIso g).inv ≫ Subobject.arrow (kernelSubobject g) = 0
[PROOFSTEP]
simp [kernelSubobject_arrow_eq_zero_of_exact_zero_left A h]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝³ : HasZeroMorphisms V
inst✝² : HasEqualizers V
inst✝¹ : HasZeroObject V
inst✝ : Mono g
⊢ 0 ≫ g = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
suffices Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0 by
  rw [← kernelSubobject_arrow', Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← kernelSubobject_arrow', Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
[PROOFSTEP]
apply zero_of_epi_comp (imageToKernel f g h.w) _
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
[PROOFSTEP]
rw [imageToKernel_arrow_assoc, ← imageSubobject_arrow, Category.assoc, ← Iso.eq_inv_comp]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ image.ι f ≫ cokernel.π f = (imageSubobjectIso f).inv ≫ 0
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
X Y : V
ι : X ⟶ B
hι : ι ≫ g = 0
π : B ⟶ Y
hπ : f ≫ π = 0
⊢ ι ≫ π = 0
[PROOFSTEP]
rw [← kernel.lift_ι _ _ hι, ← cokernel.π_desc _ _ hπ, Category.assoc, kernel_comp_cokernel_assoc _ _ h, zero_comp,
  comp_zero]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f✝ : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
f : A ⟶ 0
g : 0 ⟶ C
⊢ Exact f g
[PROOFSTEP]
obtain rfl : f = 0 := by ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f✝ : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
f : A ⟶ 0
g : 0 ⟶ C
⊢ f = 0
[PROOFSTEP]
ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ Exact 0 g
[PROOFSTEP]
obtain rfl : g = 0 := by ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ g = 0
[PROOFSTEP]
ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Exact 0 0
[PROOFSTEP]
fconstructor
[GOAL]
case w
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ 0 ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case epi
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Epi (imageToKernel 0 0 (_ : 0 ≫ 0 = 0))
[PROOFSTEP]
exact imageToKernel_epi_of_zero_of_mono 0
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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✝ : HasKernels V
B C : V
f : B ⟶ C
h : Exact 0 f
⊢ Epi 0
[PROOFSTEP]
simpa using h.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
have e₁ := h.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
rw [imageToKernel_zero_right] at e₁ 
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
have e₂ : Epi (((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow) ≫ (kernelSubobject 0).arrow) :=
  @epi_comp _ _ _ _ _ _ e₁ _ _
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id] at e₂ 
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
rw [← imageSubobject_arrow] at e₂ 
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
haveI : Epi (image.ι f) := epi_of_epi (imageSubobjectIso f).hom (image.ι f)
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} 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
[PROOFSTEP]
apply epi_of_epi_image
