[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ imageSubobject f = kernelSubobject g
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g → imageSubobject f = kernelSubobject g
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ imageSubobject f = kernelSubobject g
[PROOFSTEP]
have : IsIso (imageToKernel f g h.w) :=
  have := h.epi;
  isIso_of_mono_of_epi _
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageSubobject f = kernelSubobject g
[PROOFSTEP]
refine Subobject.eq_of_comm (asIso (imageToKernel _ _ h.w)) ?_
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ (asIso (imageToKernel f g (_ : f ≫ g = 0))).hom ≫ Subobject.arrow (kernelSubobject g) =
    Subobject.arrow (imageSubobject f)
[PROOFSTEP]
simp
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ imageSubobject f = kernelSubobject g → Exact f g
[PROOFSTEP]
apply exact_of_image_eq_kernel
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g → f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
exact fun h ↦ ⟨h.1, kernel_comp_cokernel f g h⟩
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0 → Exact f g
[PROOFSTEP]
refine fun h ↦ ⟨h.1, ?_⟩
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
suffices hl : IsLimit (KernelFork.ofι (imageSubobject f).arrow (imageSubobject_arrow_comp_eq_zero h.1))
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
have : imageToKernel f g h.1 = (hl.conePointUniqueUpToIso (limit.isLimit _)).hom ≫ (kernelSubobjectIso _).inv := by ext;
  simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    ((IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv) ≫
      Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
this :
  imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
rw [this]
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
this :
  imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
⊢ Epi ((IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv)
[PROOFSTEP]
infer_instance
[GOAL]
case hl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
[PROOFSTEP]
refine KernelFork.IsLimit.ofι _ _ (fun u hu ↦ ?_) ?_ (fun _ _ _ h ↦ ?_)
[GOAL]
case hl.refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
[PROOFSTEP]
refine kernel.lift (cokernel.π f) u ?_ ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso _).inv
[GOAL]
case hl.refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ u ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← kernel.lift_ι g u hu, Category.assoc, h.2, comp_zero]
[GOAL]
case hl.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ ∀ {W' : C} (g' : W' ⟶ Y) (eq' : g' ≫ g = 0),
    (fun {W'} u hu =>
            kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
          g' eq' ≫
        Subobject.arrow (imageSubobject f) =
      g'
[PROOFSTEP]
aesop_cat
[GOAL]
case hl.refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝ =
    (fun {W'} u hu =>
        kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
      x✝² x✝¹
[PROOFSTEP]
intros
[GOAL]
case hl.refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝ =
    (fun {W'} u hu =>
        kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
      x✝² x✝¹
[PROOFSTEP]
rw [← cancel_mono (imageSubobject f).arrow, h]
[GOAL]
case hl.refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝² =
    (fun {W'} u hu =>
          kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
        x✝² x✝¹ ≫
      Subobject.arrow (imageSubobject f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ Exact f g ↔ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ Exact f g → f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : Exact f g
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
[PROOFSTEP]
exact ⟨h.1, fork_ι_comp_cofork_π f g h cg cf⟩
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0 → Exact f g
[PROOFSTEP]
rw [exact_iff]
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0 → f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
refine fun h => ⟨h.1, ?_⟩
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
apply zero_of_epi_comp (IsLimit.conePointUniqueUpToIso hg (limit.isLimit _)).hom
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ (IsLimit.conePointUniqueUpToIso hg (limit.isLimit (parallelPair g 0))).hom ≫ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
apply zero_of_comp_mono (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) hf).hom
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ ((IsLimit.conePointUniqueUpToIso hg (limit.isLimit (parallelPair g 0))).hom ≫ kernel.ι g ≫ cokernel.π f) ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)) hf).hom =
    0
[PROOFSTEP]
simp [h.2]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
[PROOFSTEP]
tfae_have 1 ↔ 2
[GOAL]
case tfae_1_iff_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
apply exact_iff
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
[PROOFSTEP]
tfae_have 1 ↔ 3
[GOAL]
case tfae_1_iff_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ Exact f g ↔ imageSubobject f = kernelSubobject g
[PROOFSTEP]
apply exact_iff_image_eq_kernel
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
tfae_1_iff_3 : Exact f g ↔ imageSubobject f = kernelSubobject g
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
[PROOFSTEP]
tfae_finish
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : IsEquivalence F
⊢ Exact (F.map f) (F.map g) ↔ Exact f g
[PROOFSTEP]
simp only [exact_iff, ← F.map_eq_zero_iff, F.map_comp, Category.assoc, ← kernelComparison_comp_ι g F, ←
  π_comp_cokernelComparison f F]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : IsEquivalence F
⊢ F.map f ≫ F.map g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0 ↔
    F.map f ≫ F.map g = 0 ∧
      kernelComparison g F ≫ kernel.ι (F.map g) ≫ cokernel.π (F.map f) ≫ cokernelComparison f F = 0
[PROOFSTEP]
rw [IsIso.comp_left_eq_zero (kernelComparison g F), ← Category.assoc,
  IsIso.comp_right_eq_zero _ (cokernelComparison f F)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
⊢ Exact (h ≫ f) g ↔ Exact f g
[PROOFSTEP]
refine' ⟨fun hfg => _, fun h => exact_epi_comp h⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
⊢ Exact f g
[PROOFSTEP]
let hc :=
  isCokernelOfComp _ _ (colimit.isColimit (parallelPair (h ≫ f) 0))
    (by rw [← cancel_epi h, ← Category.assoc, CokernelCofork.condition, comp_zero]) rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
⊢ f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0
[PROOFSTEP]
rw [← cancel_epi h, ← Category.assoc, CokernelCofork.condition, comp_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ Exact f g
[PROOFSTEP]
refine' (exact_iff' _ _ (limit.isLimit _) hc).2 ⟨_, ((exact_iff _ _).1 hfg).2⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ f ≫ g = 0
[PROOFSTEP]
exact zero_of_epi_comp h (by rw [← hfg.1, Category.assoc])
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ h ≫ f ≫ g = 0
[PROOFSTEP]
rw [← hfg.1, Category.assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ IsLimit (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0))
[PROOFSTEP]
rw [exact_iff] at h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ IsLimit (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0))
[PROOFSTEP]
exact
  KernelFork.IsLimit.ofι _ _
    (fun u hu ↦ kernel.lift (cokernel.π f) u (by rw [← kernel.lift_ι g u hu, Category.assoc, h.2, comp_zero]))
    (by aesop_cat) (fun _ _ _ hm => by rw [← cancel_mono (image.ι f), hm, kernel.lift_ι])
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ u ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← kernel.lift_ι g u hu, Category.assoc, h.2, comp_zero]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ ∀ {W' : C} (g' : W' ⟶ Y) (eq' : g' ≫ g = 0),
    (fun {W'} u hu => kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0)) g' eq' ≫ image.ι f = g'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Abelian.image f
hm : x✝ ≫ image.ι f = x✝²
⊢ x✝ = (fun {W'} u hu => kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0)) x✝² x✝¹
[PROOFSTEP]
rw [← cancel_mono (image.ι f), hm, kernel.lift_ι]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ IsColimit (CokernelCofork.ofπ (coimage.π g) (_ : f ≫ coimage.π g = 0))
[PROOFSTEP]
rw [exact_iff] at h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ (coimage.π g) (_ : f ≫ coimage.π g = 0))
[PROOFSTEP]
refine'
  CokernelCofork.IsColimit.ofπ _ _
    (fun u hu => cokernel.desc (kernel.ι g) u (by rw [← cokernel.π_desc f u hu, ← Category.assoc, h.2, zero_comp]))
    (by aesop_cat) _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
Z'✝ : C
u : Y ⟶ Z'✝
hu : f ≫ u = 0
⊢ kernel.ι g ≫ u = 0
[PROOFSTEP]
rw [← cokernel.π_desc f u hu, ← Category.assoc, h.2, zero_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : f ≫ g' = 0),
    coimage.π g ≫ (fun {Z'} u hu => cokernel.desc (kernel.ι g) u (_ : kernel.ι g ≫ u = 0)) g' eq' = g'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : f ≫ g' = 0) (m : Abelian.coimage g ⟶ Z'),
    coimage.π g ≫ m = g' → m = (fun {Z'} u hu => cokernel.desc (kernel.ι g) u (_ : kernel.ι g ≫ u = 0)) g' eq'
[PROOFSTEP]
intros _ _ _ _ hm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
Z'✝ : C
g'✝ : Y ⟶ Z'✝
eq'✝ : f ≫ g'✝ = 0
m✝ : Abelian.coimage g ⟶ Z'✝
hm : coimage.π g ≫ m✝ = g'✝
⊢ m✝ = (fun {Z'} u hu => cokernel.desc (kernel.ι g) u (_ : kernel.ι g ≫ u = 0)) g'✝ eq'✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Exact f g
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
Z'✝ : C
g'✝ : Y ⟶ Z'✝
eq'✝ : f ≫ g'✝ = 0
m✝ : Abelian.coimage g ⟶ Z'✝
hm : coimage.π g ≫ m✝ = g'✝
⊢ coequalizer.π (kernel.ι g) 0 ≫ m✝ =
    coequalizer.π (kernel.ι g) 0 ≫ (fun {Z'} u hu => cokernel.desc (kernel.ι g) u (_ : kernel.ι g ≫ u = 0)) g'✝ eq'✝
[PROOFSTEP]
rw [hm, cokernel.π_desc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ (Cofork.π (CokernelCofork.ofπ (coimage.π g) (_ : f ≫ coimage.π g = 0)) ≫ (coimageIsoImage' g).hom) ≫
      Limits.image.ι g =
    factorThruImage g ≫ Limits.image.ι g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f (cokernel.π f)
[PROOFSTEP]
rw [exact_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ cokernel.π f = 0 ∧ kernel.ι (cokernel.π f) ≫ cokernel.π f = 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ cokernel.π f ≫ cokernel.desc f g (_ : f ≫ g = 0) =
    cokernel.π f ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)) (isColimitImage f g h)).hom ≫
        Limits.image.ι g
[PROOFSTEP]
simp
  -- porting note: this can no longer be an instance in Lean4
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
ex : Exact f g
⊢ let_fun this := (_ : IsIso (cokernel.desc f g (_ : f ≫ g = 0)));
  g ≫ CategoryTheory.inv (cokernel.desc f g (_ : f ≫ g = 0)) = cokernel.π f
[PROOFSTEP]
have := isIso_cokernel_desc_of_exact_of_epi _ _ ex
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
ex : Exact f g
this : IsIso (cokernel.desc f g (_ : f ≫ g = 0))
⊢ let_fun this := (_ : IsIso (cokernel.desc f g (_ : f ≫ g = 0)));
  g ≫ CategoryTheory.inv (cokernel.desc f g (_ : f ≫ g = 0)) = cokernel.π f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
ex : Exact f g
⊢ let_fun this := (_ : IsIso (kernel.lift g f (_ : f ≫ g = 0)));
  CategoryTheory.inv (kernel.lift g f (_ : f ≫ g = 0)) ≫ f = kernel.ι g
[PROOFSTEP]
have := isIso_kernel_lift_of_exact_of_mono _ _ ex
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
ex : Exact f g
this : IsIso (kernel.lift g f (_ : f ≫ g = 0))
⊢ let_fun this := (_ : IsIso (kernel.lift g f (_ : f ≫ g = 0)));
  CategoryTheory.inv (kernel.lift g f (_ : f ≫ g = 0)) ≫ f = kernel.ι g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
h : Exact f g
⊢ cokernel.π f ≫ cokernel.desc f g (_ : f ≫ g = 0) ≫ epiDesc g (cokernel.π f) (_ : kernel.ι g ≫ cokernel.π f = 0) =
    cokernel.π f ≫ 𝟙 (colimit.cocone (parallelPair f 0)).pt
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
h : Exact f g
⊢ g ≫ epiDesc g (cokernel.π f) (_ : kernel.ι g ≫ cokernel.π f = 0) ≫ cokernel.desc f g (_ : f ≫ g = 0) =
    g ≫ 𝟙 (CokernelCofork.ofπ g (_ : f ≫ g = 0)).pt
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
h : Exact f g
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (colimit.cocone (parallelPair f 0)).ι j ≫
        (Iso.mk (cokernel.desc f g (_ : f ≫ g = 0))
            (epiDesc g (cokernel.π f) (_ : kernel.ι g ≫ cokernel.π f = 0))).hom =
      NatTrans.app (CokernelCofork.ofπ g (_ : f ≫ g = 0)).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
h : Exact f g
⊢ NatTrans.app (colimit.cocone (parallelPair f 0)).ι WalkingParallelPair.zero ≫
      (Iso.mk (cokernel.desc f g (_ : f ≫ g = 0)) (epiDesc g (cokernel.π f) (_ : kernel.ι g ≫ cokernel.π f = 0))).hom =
    NatTrans.app (CokernelCofork.ofπ g (_ : f ≫ g = 0)).ι WalkingParallelPair.zero
[PROOFSTEP]
simp [h.w]
[GOAL]
case one
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
h : Exact f g
⊢ NatTrans.app (colimit.cocone (parallelPair f 0)).ι WalkingParallelPair.one ≫
      (Iso.mk (cokernel.desc f g (_ : f ≫ g = 0)) (epiDesc g (cokernel.π f) (_ : kernel.ι g ≫ cokernel.π f = 0))).hom =
    NatTrans.app (CokernelCofork.ofπ g (_ : f ≫ g = 0)).ι WalkingParallelPair.one
[PROOFSTEP]
simp [h.w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
h : Exact f g
⊢ (monoLift f (kernel.ι g) (_ : kernel.ι g ≫ cokernel.π f = 0) ≫ kernel.lift g f (_ : f ≫ g = 0)) ≫ kernel.ι g =
    𝟙 (limit.cone (parallelPair g 0)).pt ≫ kernel.ι g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
h : Exact f g
⊢ (kernel.lift g f (_ : f ≫ g = 0) ≫ monoLift f (kernel.ι g) (_ : kernel.ι g ≫ cokernel.π f = 0)) ≫ f =
    𝟙 (KernelFork.ofι f (_ : f ≫ g = 0)).pt ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
h : Exact f g
j : WalkingParallelPair
⊢ NatTrans.app (limit.cone (parallelPair g 0)).π j =
    (Iso.mk (monoLift f (kernel.ι g) (_ : kernel.ι g ≫ cokernel.π f = 0)) (kernel.lift g f (_ : f ≫ g = 0))).hom ≫
      NatTrans.app (KernelFork.ofι f (_ : f ≫ g = 0)).π j
[PROOFSTEP]
cases j
[GOAL]
case zero
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
h : Exact f g
⊢ NatTrans.app (limit.cone (parallelPair g 0)).π WalkingParallelPair.zero =
    (Iso.mk (monoLift f (kernel.ι g) (_ : kernel.ι g ≫ cokernel.π f = 0)) (kernel.lift g f (_ : f ≫ g = 0))).hom ≫
      NatTrans.app (KernelFork.ofι f (_ : f ≫ g = 0)).π WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
h : Exact f g
⊢ NatTrans.app (limit.cone (parallelPair g 0)).π WalkingParallelPair.one =
    (Iso.mk (monoLift f (kernel.ι g) (_ : kernel.ι g ≫ cokernel.π f = 0)) (kernel.lift g f (_ : f ≫ g = 0))).hom ≫
      NatTrans.app (KernelFork.ofι f (_ : f ≫ g = 0)).π WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
⊢ Exact f g
[PROOFSTEP]
refine' (exact_iff _ _).2 ⟨w, _⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
have := h.fac (CokernelCofork.ofπ _ (cokernel.condition f)) WalkingParallelPair.one
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
this :
  NatTrans.app (CokernelCofork.ofπ g w).ι WalkingParallelPair.one ≫
      IsColimit.desc h (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)) =
    NatTrans.app (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)).ι WalkingParallelPair.one
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
simp only [Cofork.ofπ_ι_app] at this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
this : g ≫ IsColimit.desc h (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)) = cokernel.π f
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← this, ← Category.assoc, kernel.condition, zero_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsLimit (KernelFork.ofι f w)
⊢ Exact f g
[PROOFSTEP]
refine' (exact_iff _ _).2 ⟨w, _⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsLimit (KernelFork.ofι f w)
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
have := h.fac (KernelFork.ofι _ (kernel.condition g)) WalkingParallelPair.zero
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsLimit (KernelFork.ofι f w)
this :
  IsLimit.lift h (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)) ≫
      NatTrans.app (KernelFork.ofι f w).π WalkingParallelPair.zero =
    NatTrans.app (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)).π WalkingParallelPair.zero
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
simp only [Fork.ofι_π_app] at this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsLimit (KernelFork.ofι f w)
this : IsLimit.lift h (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)) ≫ f = kernel.ι g
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← this, Category.assoc, cokernel.condition, comp_zero]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ Exact (image.ι f) g
[PROOFSTEP]
conv_lhs => rw [← Abelian.image.fac f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
| Exact f g
[PROOFSTEP]
rw [← Abelian.image.fac f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
| Exact f g
[PROOFSTEP]
rw [← Abelian.image.fac f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
| Exact f g
[PROOFSTEP]
rw [← Abelian.image.fac f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact (Abelian.factorThruImage f ≫ image.ι f) g ↔ Exact (image.ι f) g
[PROOFSTEP]
rw [exact_epi_comp_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ Exact f (coimage.π g)
[PROOFSTEP]
conv_lhs => rw [← Abelian.coimage.fac g]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
| Exact f g
[PROOFSTEP]
rw [← Abelian.coimage.fac g]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
| Exact f g
[PROOFSTEP]
rw [← Abelian.coimage.fac g]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
| Exact f g
[PROOFSTEP]
rw [← Abelian.coimage.fac g]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f (coimage.π g ≫ Abelian.factorThruCoimage g) ↔ Exact f (coimage.π g)
[PROOFSTEP]
rw [exact_comp_mono_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ TFAE [Mono f, kernel.ι f = 0, Exact 0 f]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact 0 f → kernel.ι f = 0
[PROOFSTEP]
exact kernel_ι_eq_zero_of_exact_zero_left Z
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact 0 f → kernel.ι f = 0
⊢ TFAE [Mono f, kernel.ι f = 0, Exact 0 f]
[PROOFSTEP]
tfae_have 1 → 3
[GOAL]
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact 0 f → kernel.ι f = 0
⊢ Mono f → Exact 0 f
[PROOFSTEP]
intros
[GOAL]
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact 0 f → kernel.ι f = 0
✝ : Mono f
⊢ Exact 0 f
[PROOFSTEP]
exact exact_zero_left_of_mono Z
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact 0 f → kernel.ι f = 0
tfae_1_to_3 : Mono f → Exact 0 f
⊢ TFAE [Mono f, kernel.ι f = 0, Exact 0 f]
[PROOFSTEP]
tfae_have 2 → 1
[GOAL]
case tfae_2_to_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact 0 f → kernel.ι f = 0
tfae_1_to_3 : Mono f → Exact 0 f
⊢ kernel.ι f = 0 → Mono f
[PROOFSTEP]
exact mono_of_kernel_ι_eq_zero _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact 0 f → kernel.ι f = 0
tfae_1_to_3 : Mono f → Exact 0 f
tfae_2_to_1 : kernel.ι f = 0 → Mono f
⊢ TFAE [Mono f, kernel.ι f = 0, Exact 0 f]
[PROOFSTEP]
tfae_finish
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f 0 → cokernel.π f = 0
[PROOFSTEP]
rw [exact_iff]
[GOAL]
case tfae_3_to_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0 → cokernel.π f = 0
[PROOFSTEP]
rintro ⟨-, h⟩
[GOAL]
case tfae_3_to_2.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : kernel.ι 0 ≫ cokernel.π f = 0
⊢ cokernel.π f = 0
[PROOFSTEP]
exact zero_of_epi_comp _ h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
[PROOFSTEP]
tfae_have 1 → 3
[GOAL]
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ Epi f → Exact f 0
[PROOFSTEP]
rw [exact_iff]
[GOAL]
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ Epi f → f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0
[PROOFSTEP]
intro
[GOAL]
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0
[PROOFSTEP]
exact ⟨by simp, by simp [cokernel.π_of_epi]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ f ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ kernel.ι 0 ≫ cokernel.π f = 0
[PROOFSTEP]
simp [cokernel.π_of_epi]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
[PROOFSTEP]
tfae_have 2 → 1
[GOAL]
case tfae_2_to_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
⊢ cokernel.π f = 0 → Epi f
[PROOFSTEP]
exact epi_of_cokernel_π_eq_zero _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
tfae_2_to_1 : cokernel.π f = 0 → Epi f
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
[PROOFSTEP]
tfae_finish
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ Exact g.op f.op
[PROOFSTEP]
rw [exact_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ g.op ≫ f.op = 0 ∧ kernel.ι f.op ≫ cokernel.π g.op = 0
[PROOFSTEP]
refine' ⟨by simp [← op_comp, h.w], Quiver.Hom.unop_inj _⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ g.op ≫ f.op = 0
[PROOFSTEP]
simp [← op_comp, h.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ (kernel.ι f.op ≫ cokernel.π g.op).unop = 0.unop
[PROOFSTEP]
simp only [unop_comp, cokernel.π_op, eqToHom_refl, kernel.ι_op, Category.id_comp, Category.assoc,
  kernel_comp_cokernel_assoc _ _ h, zero_comp, comp_zero, unop_zero]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e : Exact g.op f.op
⊢ Exact f g
[PROOFSTEP]
rw [← IsEquivalence.exact_iff _ _ (opOpEquivalence C).inverse]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e : Exact g.op f.op
⊢ Exact ((opOpEquivalence C).inverse.map f) ((opOpEquivalence C).inverse.map g)
[PROOFSTEP]
exact Exact.op _ _ e
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Cᵒᵖ
g : X ⟶ Y
f : Y ⟶ Z
h : Exact g f
⊢ Exact f.unop g.unop
[PROOFSTEP]
rw [← f.op_unop, ← g.op_unop] at h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Cᵒᵖ
g : X ⟶ Y
f : Y ⟶ Z
h : Exact g.unop.op f.unop.op
⊢ Exact f.unop g.unop
[PROOFSTEP]
rwa [← Exact.op_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Cᵒᵖ
g : X ⟶ Y
f : Y ⟶ Z
e : Exact f.unop g.unop
⊢ Exact g f
[PROOFSTEP]
rwa [← f.op_unop, ← g.op_unop, ← Exact.op_iff] at e
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Cᵒᵖ
g : X ⟶ Y
f : Y ⟶ Z
e : Exact g f
⊢ Exact f.unop g.unop
[PROOFSTEP]
rw [← Exact.op_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Cᵒᵖ
g : X ⟶ Y
f : Y ⟶ Z
e : Exact g f
⊢ Exact g.unop.op f.unop.op
[PROOFSTEP]
exact e
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : Exact (F.map f) (F.map g)
⊢ Exact f g
[PROOFSTEP]
rw [Abelian.exact_iff, ← F.map_comp, F.map_eq_zero_iff] at hfg
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : f ≫ g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0
⊢ Exact f g
[PROOFSTEP]
refine' (Abelian.exact_iff _ _).2 ⟨hfg.1, F.zero_of_map_zero _ _⟩
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : f ≫ g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0
⊢ F.map (kernel.ι g ≫ cokernel.π f) = 0
[PROOFSTEP]
obtain ⟨k, hk⟩ :=
  kernel.lift' (F.map g) (F.map (kernel.ι g))
    (by simp only [← F.map_comp, kernel.condition, CategoryTheory.Functor.map_zero])
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : f ≫ g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0
⊢ F.map (kernel.ι g) ≫ F.map g = 0
[PROOFSTEP]
simp only [← F.map_comp, kernel.condition, CategoryTheory.Functor.map_zero]
[GOAL]
case mk
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : f ≫ g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0
k : F.obj (kernel g) ⟶ kernel (F.map g)
hk : k ≫ kernel.ι (F.map g) = F.map (kernel.ι g)
⊢ F.map (kernel.ι g ≫ cokernel.π f) = 0
[PROOFSTEP]
obtain ⟨l, hl⟩ :=
  cokernel.desc' (F.map f) (F.map (cokernel.π f))
    (by simp only [← F.map_comp, cokernel.condition, CategoryTheory.Functor.map_zero])
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : f ≫ g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0
k : F.obj (kernel g) ⟶ kernel (F.map g)
hk : k ≫ kernel.ι (F.map g) = F.map (kernel.ι g)
⊢ F.map f ≫ F.map (cokernel.π f) = 0
[PROOFSTEP]
simp only [← F.map_comp, cokernel.condition, CategoryTheory.Functor.map_zero]
[GOAL]
case mk.mk
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hfg : f ≫ g = 0 ∧ kernel.ι (F.map g) ≫ cokernel.π (F.map f) = 0
k : F.obj (kernel g) ⟶ kernel (F.map g)
hk : k ≫ kernel.ι (F.map g) = F.map (kernel.ι g)
l : cokernel (F.map f) ⟶ F.obj (cokernel f)
hl : cokernel.π (F.map f) ≫ l = F.map (cokernel.π f)
⊢ F.map (kernel.ι g ≫ cokernel.π f) = 0
[PROOFSTEP]
rw [F.map_comp, ← hk, ← hl, Category.assoc, reassoc_of% hfg.2, zero_comp, comp_zero]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Abelian A
inst✝² : Abelian B
L : A ⥤ B
inst✝¹ : PreservesFiniteLimits L
inst✝ : PreservesFiniteColimits L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
e1 : Exact f g
⊢ Exact (L.map f) (L.map g)
[PROOFSTEP]
let hcoker := isColimitOfHasCokernelOfPreservesColimit L f
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Abelian A
inst✝² : Abelian B
L : A ⥤ B
inst✝¹ : PreservesFiniteLimits L
inst✝ : PreservesFiniteColimits L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
e1 : Exact f g
hcoker : IsColimit
  (Cofork.ofπ (L.map (cokernel.π f)) (_ : L.map f ≫ L.map (cokernel.π f) = 0 ≫ L.map (cokernel.π f))) :=
  isColimitOfHasCokernelOfPreservesColimit L f
⊢ Exact (L.map f) (L.map g)
[PROOFSTEP]
let hker := isLimitOfHasKernelOfPreservesLimit L g
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Abelian A
inst✝² : Abelian B
L : A ⥤ B
inst✝¹ : PreservesFiniteLimits L
inst✝ : PreservesFiniteColimits L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
e1 : Exact f g
hcoker : IsColimit
  (Cofork.ofπ (L.map (cokernel.π f)) (_ : L.map f ≫ L.map (cokernel.π f) = 0 ≫ L.map (cokernel.π f))) :=
  isColimitOfHasCokernelOfPreservesColimit L f
hker : IsLimit (Fork.ofι (L.map (kernel.ι g)) (_ : L.map (kernel.ι g) ≫ L.map g = L.map (kernel.ι g) ≫ 0)) :=
  isLimitOfHasKernelOfPreservesLimit L g
⊢ Exact (L.map f) (L.map g)
[PROOFSTEP]
refine' (exact_iff' _ _ hker hcoker).2 ⟨by simp [← L.map_comp, e1.1], _⟩
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Abelian A
inst✝² : Abelian B
L : A ⥤ B
inst✝¹ : PreservesFiniteLimits L
inst✝ : PreservesFiniteColimits L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
e1 : Exact f g
hcoker : IsColimit
  (Cofork.ofπ (L.map (cokernel.π f)) (_ : L.map f ≫ L.map (cokernel.π f) = 0 ≫ L.map (cokernel.π f))) :=
  isColimitOfHasCokernelOfPreservesColimit L f
hker : IsLimit (Fork.ofι (L.map (kernel.ι g)) (_ : L.map (kernel.ι g) ≫ L.map g = L.map (kernel.ι g) ≫ 0)) :=
  isLimitOfHasKernelOfPreservesLimit L g
⊢ L.map f ≫ L.map g = 0
[PROOFSTEP]
simp [← L.map_comp, e1.1]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Abelian A
inst✝² : Abelian B
L : A ⥤ B
inst✝¹ : PreservesFiniteLimits L
inst✝ : PreservesFiniteColimits L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
e1 : Exact f g
hcoker : IsColimit
  (Cofork.ofπ (L.map (cokernel.π f)) (_ : L.map f ≫ L.map (cokernel.π f) = 0 ≫ L.map (cokernel.π f))) :=
  isColimitOfHasCokernelOfPreservesColimit L f
hker : IsLimit (Fork.ofι (L.map (kernel.ι g)) (_ : L.map (kernel.ι g) ≫ L.map g = L.map (kernel.ι g) ≫ 0)) :=
  isLimitOfHasKernelOfPreservesLimit L g
⊢ Fork.ι (Fork.ofι (L.map (kernel.ι g)) (_ : L.map (kernel.ι g) ≫ L.map g = L.map (kernel.ι g) ≫ 0)) ≫
      Cofork.π (Cofork.ofπ (L.map (cokernel.π f)) (_ : L.map f ≫ L.map (cokernel.π f) = 0 ≫ L.map (cokernel.π f))) =
    0
[PROOFSTEP]
simp only [Fork.ι_ofι, Cofork.π_ofπ, ← L.map_comp, kernel_comp_cokernel _ _ e1, L.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
⊢ PreservesZeroMorphisms L
[PROOFSTEP]
replace h := (h (exact_of_zero (𝟙 0) (𝟙 0))).w
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : L.map (𝟙 0) ≫ L.map (𝟙 0) = 0
⊢ PreservesZeroMorphisms L
[PROOFSTEP]
rw [L.map_id, Category.comp_id] at h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : 𝟙 (L.obj 0) = 0
⊢ PreservesZeroMorphisms L
[PROOFSTEP]
exact preservesZeroMorphisms_of_map_zero_object (idZeroEquivIsoZero _ h)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono (L.map f)
[PROOFSTEP]
letI := preservesZeroMorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Mono (L.map f)
[PROOFSTEP]
apply ((tfae_mono (L.obj 0) (L.map f)).out 2 0).mp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact 0 (L.map f)
[PROOFSTEP]
rw [← L.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map 0) (L.map f)
[PROOFSTEP]
exact h (((tfae_mono 0 f).out 0 2).mp hf)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (L.map f)
[PROOFSTEP]
letI := preservesZeroMorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Epi (L.map f)
[PROOFSTEP]
apply ((tfae_epi (L.obj 0) (L.map f)).out 2 0).mp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map f) 0
[PROOFSTEP]
rw [← L.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map f) (L.map 0)
[PROOFSTEP]
exact h (((tfae_epi 0 f).out 0 2).mp hf)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cone (parallelPair f 0)
ic : IsLimit c
⊢ IsLimit (L.mapCone c)
[PROOFSTEP]
letI := preservesZeroMorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cone (parallelPair f 0)
ic : IsLimit c
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ IsLimit (L.mapCone c)
[PROOFSTEP]
letI := preservesMonomorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cone (parallelPair f 0)
ic : IsLimit c
this✝ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this : PreservesMonomorphisms L := preservesMonomorphisms_of_map_exact L h
⊢ IsLimit (L.mapCone c)
[PROOFSTEP]
letI := mono_of_isLimit_fork ic
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cone (parallelPair f 0)
ic : IsLimit c
this✝¹ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this✝ : PreservesMonomorphisms L := preservesMonomorphisms_of_map_exact L h
this : Mono (Fork.ι c) := mono_of_isLimit_fork ic
⊢ IsLimit (L.mapCone c)
[PROOFSTEP]
have hf :=
  (isLimitMapConeForkEquiv' L (KernelFork.condition c)).symm
    (isLimitOfExactOfMono (L.map (Fork.ι c)) (L.map f)
      (h (exact_of_is_kernel (Fork.ι c) f (KernelFork.condition c) (ic.ofIsoLimit (isoOfι _)))))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cone (parallelPair f 0)
ic : IsLimit c
this✝¹ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this✝ : PreservesMonomorphisms L := preservesMonomorphisms_of_map_exact L h
this : Mono (Fork.ι c) := mono_of_isLimit_fork ic
hf :
  (fun x => IsLimit (L.mapCone (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ f = 0))))
    (isLimitOfExactOfMono (L.map (Fork.ι c)) (L.map f) (_ : Exact (L.map (Fork.ι c)) (L.map f)))
⊢ IsLimit (L.mapCone c)
[PROOFSTEP]
exact hf.ofIsoLimit ((Cones.functoriality _ L).mapIso (isoOfι _).symm)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cocone (parallelPair f 0)
ic : IsColimit c
⊢ IsColimit (L.mapCocone c)
[PROOFSTEP]
letI := preservesZeroMorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cocone (parallelPair f 0)
ic : IsColimit c
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ IsColimit (L.mapCocone c)
[PROOFSTEP]
letI := preservesEpimorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cocone (parallelPair f 0)
ic : IsColimit c
this✝ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this : PreservesEpimorphisms L := preservesEpimorphisms_of_map_exact L h
⊢ IsColimit (L.mapCocone c)
[PROOFSTEP]
letI := epi_of_isColimit_cofork ic
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cocone (parallelPair f 0)
ic : IsColimit c
this✝¹ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this✝ : PreservesEpimorphisms L := preservesEpimorphisms_of_map_exact L h
this : Epi (Cofork.π c) := epi_of_isColimit_cofork ic
⊢ IsColimit (L.mapCocone c)
[PROOFSTEP]
have hf :=
  (isColimitMapCoconeCoforkEquiv' L (CokernelCofork.condition c)).symm
    (isColimitOfExactOfEpi (L.map f) (L.map (Cofork.π c))
      (h (exact_of_is_cokernel f (Cofork.π c) (CokernelCofork.condition c) (ic.ofIsoColimit (isoOfπ _)))))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X Y : A
f : X ⟶ Y
c : Cocone (parallelPair f 0)
ic : IsColimit c
this✝¹ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this✝ : PreservesEpimorphisms L := preservesEpimorphisms_of_map_exact L h
this : Epi (Cofork.π c) := epi_of_isColimit_cofork ic
hf :
  (fun x => IsColimit (L.mapCocone (CokernelCofork.ofπ (Cofork.π c) (_ : f ≫ Cofork.π c = 0))))
    (isColimitOfExactOfEpi (L.map f) (L.map (Cofork.π c)) (_ : Exact (L.map f) (L.map (Cofork.π c))))
⊢ IsColimit (L.mapCocone c)
[PROOFSTEP]
exact hf.ofIsoColimit ((Cocones.functoriality _ L).mapIso (isoOfπ _).symm)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
⊢ PreservesFiniteLimits L
[PROOFSTEP]
letI := preservesZeroMorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ PreservesFiniteLimits L
[PROOFSTEP]
letI := preservesKernelsOfMapExact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
this✝ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this : (X Y : A) → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) L := preservesKernelsOfMapExact L h
⊢ PreservesFiniteLimits L
[PROOFSTEP]
apply preservesFiniteLimitsOfPreservesKernels
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
⊢ PreservesFiniteColimits L
[PROOFSTEP]
letI := preservesZeroMorphisms_of_map_exact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ PreservesFiniteColimits L
[PROOFSTEP]
letI := preservesCokernelsOfMapExact L h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
this✝ : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
this : (X Y : A) → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) L := preservesCokernelsOfMapExact L h
⊢ PreservesFiniteColimits L
[PROOFSTEP]
apply preservesFiniteColimitsOfPreservesCokernels
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesMonomorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) L
⊢ PreservesFiniteLimits L
[PROOFSTEP]
apply preservesFiniteLimitsOfMapExact
[GOAL]
case h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesMonomorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) L
⊢ ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
[PROOFSTEP]
intro X Y Z f g h
[GOAL]
case h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesMonomorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ Exact (L.map f) (L.map g)
[PROOFSTEP]
rw [← Abelian.coimage.fac g, L.map_comp, exact_comp_mono_iff]
[GOAL]
case h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesMonomorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ Exact (L.map f) (L.map (coimage.π g))
[PROOFSTEP]
exact exact_of_is_cokernel _ _ _ (isColimitCoforkMapOfIsColimit' L _ (isColimitCoimage f g h))
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesEpimorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) L
⊢ PreservesFiniteColimits L
[PROOFSTEP]
apply preservesFiniteColimitsOfMapExact
[GOAL]
case h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesEpimorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) L
⊢ ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
[PROOFSTEP]
intro X Y Z f g h
[GOAL]
case h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesEpimorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ Exact (L.map f) (L.map g)
[PROOFSTEP]
rw [← Abelian.image.fac f, L.map_comp, exact_epi_comp_iff]
[GOAL]
case h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : Abelian C
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : PreservesZeroMorphisms L
inst✝¹ : PreservesEpimorphisms L
inst✝ : {X Y : A} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) L
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ Exact (L.map (Abelian.image.ι f)) (L.map g)
[PROOFSTEP]
exact exact_of_is_kernel _ _ _ (isLimitForkMapOfIsLimit' L _ (isLimitImage f g h))


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ Quiver.Hom.unmop (Quiver.Hom.mop f.hom ≫ Quiver.Hom.mop f.inv) = Quiver.Hom.unmop (𝟙 (MonoidalOpposite.mop X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ Quiver.Hom.unmop (Quiver.Hom.mop f.inv ≫ Quiver.Hom.mop f.hom) = Quiver.Hom.unmop (𝟙 (MonoidalOpposite.mop Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Cᵒᵖ
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
h : X₃✝ ⟶ Y₃✝
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) f g) h ≫
        ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) Y₁✝ Y₂✝ Y₃✝).hom).unop =
    (((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) X₁✝ X₂✝ X₃✝).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) f ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) g h)).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) (𝟙 (op (𝟙_ C))) f ≫
        ((fun X => Iso.op (λ_ X.unop).symm) Y✝).hom).unop =
    (((fun X => Iso.op (λ_ X.unop).symm) X✝).hom ≫ f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) f (𝟙 (op (𝟙_ C))) ≫
        ((fun X => Iso.op (ρ_ X.unop).symm) Y✝).hom).unop =
    (((fun X => Iso.op (ρ_ X.unop).symm) X✝).hom ≫ f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) W X Y).hom
          (𝟙 Z) ≫
        ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) W ((fun X Y => op (X.unop ⊗ Y.unop)) X Y) Z).hom ≫
          (fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) (𝟙 W)
            ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) X Y Z).hom).unop =
    (((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) ((fun X Y => op (X.unop ⊗ Y.unop)) W X) Y Z).hom ≫
        ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) W X ((fun X Y => op (X.unop ⊗ Y.unop)) Y Z)).hom).unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ ((𝟙 W.unop ⊗ (α_ X.unop Y.unop Z.unop).inv) ≫ (α_ W.unop (X.unop ⊗ Y.unop) Z.unop).inv) ≫
      ((α_ W.unop X.unop Y.unop).inv ⊗ 𝟙 Z.unop) =
    (α_ W.unop X.unop (Y.unop ⊗ Z.unop)).inv ≫ (α_ (W.unop ⊗ X.unop) Y.unop Z.unop).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ (((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) X (op (𝟙_ C)) Y).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) (𝟙 X) ((fun X => Iso.op (λ_ X.unop).symm) Y).hom).unop =
    ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) ((fun X => Iso.op (ρ_ X.unop).symm) X).hom (𝟙 Y)).unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ (𝟙 X.unop ⊗ (λ_ Y.unop).inv) ≫ (α_ X.unop (𝟙_ C) Y.unop).inv = (ρ_ X.unop).inv ⊗ 𝟙 Y.unop
[PROOFSTEP]
coherence
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Cᴹᵒᵖ
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
h : X₃✝ ⟶ Y₃✝
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f))
          ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) f g) h ≫
        ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) Y₁✝ Y₂✝ Y₃✝).hom) =
    Quiver.Hom.unmop
      (((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) X₁✝ X₂✝ X₃✝).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) f
          ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) g h))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᴹᵒᵖ
f : X✝ ⟶ Y✝
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) (𝟙 (mop (𝟙_ C))) f ≫
        ((fun X => Iso.mop (ρ_ (unmop X))) Y✝).hom) =
    Quiver.Hom.unmop (((fun X => Iso.mop (ρ_ (unmop X))) X✝).hom ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᴹᵒᵖ
f : X✝ ⟶ Y✝
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) f (𝟙 (mop (𝟙_ C))) ≫
        ((fun X => Iso.mop (λ_ (unmop X))) Y✝).hom) =
    Quiver.Hom.unmop (((fun X => Iso.mop (λ_ (unmop X))) X✝).hom ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f))
          ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) W X Y).hom (𝟙 Z) ≫
        ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) W ((fun X Y => mop (unmop Y ⊗ unmop X)) X Y)
              Z).hom ≫
          (fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) (𝟙 W)
            ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) X Y Z).hom) =
    Quiver.Hom.unmop
      (((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) ((fun X Y => mop (unmop Y ⊗ unmop X)) W X) Y
            Z).hom ≫
        ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) W X
            ((fun X Y => mop (unmop Y ⊗ unmop X)) Y Z)).hom)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ (𝟙 (unmop Z) ⊗ (α_ (unmop Y) (unmop X) (unmop W)).inv) ≫
      (α_ (unmop Z) (unmop Y ⊗ unmop X) (unmop W)).inv ≫ ((α_ (unmop Z) (unmop Y) (unmop X)).inv ⊗ 𝟙 (unmop W)) =
    (α_ (unmop Z) (unmop Y) (unmop X ⊗ unmop W)).inv ≫ (α_ (unmop Z ⊗ unmop Y) (unmop X) (unmop W)).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ Quiver.Hom.unmop
      (((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) X (mop (𝟙_ C)) Y).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) (𝟙 X)
          ((fun X => Iso.mop (ρ_ (unmop X))) Y).hom) =
    Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f))
        ((fun X => Iso.mop (λ_ (unmop X))) X).hom (𝟙 Y))
[PROOFSTEP]
simp