[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))
[PROOFSTEP]
let bc := BinaryBicone.ofLimitCone i
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))
[PROOFSTEP]
let presf : PreservesLimit (parallelPair bc.snd 0) F := by simpa
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
⊢ PreservesLimit (parallelPair bc.snd 0) F
[PROOFSTEP]
simpa
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
presf : PreservesLimit (parallelPair bc.snd 0) F := id inst✝
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))
[PROOFSTEP]
let hf : IsLimit bc.sndKernelFork := BinaryBicone.isLimitSndKernelFork i
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
presf : PreservesLimit (parallelPair bc.snd 0) F := id inst✝
hf : IsLimit (BinaryBicone.sndKernelFork bc) := BinaryBicone.isLimitSndKernelFork i
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))
[PROOFSTEP]
exact
  (isLimitMapConeBinaryFanEquiv F π₁ π₂).invFun
    (BinaryBicone.isBilimitOfKernelInl (F.mapBinaryBicone bc)
        (isLimitMapConeForkEquiv' F bc.inl_snd (isLimitOfPreserves F hf))).isLimit
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
⊢ PreservesLimit (parallelPair f g) F
[PROOFSTEP]
letI := preservesBinaryBiproductsOfPreservesBinaryProducts F
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
⊢ PreservesLimit (parallelPair f g) F
[PROOFSTEP]
haveI := additive_of_preservesBinaryBiproducts F
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
⊢ PreservesLimit (parallelPair f g) F
[PROOFSTEP]
constructor
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
⊢ {c : Cone (parallelPair f g)} → IsLimit c → IsLimit (F.mapCone c)
[PROOFSTEP]
intro c i
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
let c' := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (kernelForkOfFork (Fork.ofι (Fork.ι c) (_ : Fork.ι c ≫ f = Fork.ι c ≫ g))) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
dsimp only [kernelForkOfFork_ofι] at c' 
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ (f - g) = 0)) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
let iFc := isLimitForkMapOfIsLimit' F _ c'
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ (f - g) = 0)) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0)) :=
  isLimitForkMapOfIsLimit' F (_ : Fork.ι c ≫ (f - g) = 0) c'
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ ((Cones.functoriality _ F).mapIso (Fork.isoForkOfι c).symm)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ (f - g) = 0)) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0)) :=
  isLimitForkMapOfIsLimit' F (_ : Fork.ι c ≫ (f - g) = 0) c'
⊢ IsLimit ((Cones.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) (_ : Fork.ι c ≫ f = Fork.ι c ≫ g)))
[PROOFSTEP]
apply (isLimitMapConeForkEquiv F (Fork.condition c)).invFun
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ (f - g) = 0)) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0)) :=
  isLimitForkMapOfIsLimit' F (_ : Fork.ι c ≫ (f - g) = 0) c'
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map f = F.map (Fork.ι c) ≫ F.map g))
[PROOFSTEP]
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq F.map_sub rfl
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ (f - g) = 0)) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0)) :=
  isLimitForkMapOfIsLimit' F (_ : Fork.ι c ≫ (f - g) = 0) c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.eqOfHomEq (_ : F.map (f - g) = F.map f - F.map g) (_ : 0 = 0)
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map f = F.map (Fork.ι c) ≫ F.map g))
[PROOFSTEP]
exact
  IsLimit.ofIsoLimit (isLimitForkOfKernelFork ((IsLimit.postcomposeHomEquiv p _).symm iFc))
    (Fork.ext (Iso.refl _) (by simp))
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryProducts F
this : Additive F
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ (f - g) = 0)) :=
  isLimitKernelForkOfFork (IsLimit.ofIsoLimit i (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0)) :=
  isLimitForkMapOfIsLimit' F (_ : Fork.ι c ≫ (f - g) = 0) c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.eqOfHomEq (_ : F.map (f - g) = F.map f - F.map g) (_ : 0 = 0)
⊢ (Iso.refl
          (forkOfKernelFork
              ((Cones.postcompose p.hom).obj
                (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0)))).pt).hom ≫
      Fork.ι (Fork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map f = F.map (Fork.ι c) ≫ F.map g)) =
    Fork.ι
      (forkOfKernelFork
        ((Cones.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) (_ : F.map (Fork.ι c) ≫ F.map (f - g) = 0))))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesLimit K F
[PROOFSTEP]
letI := preservesEqualizerOfPreservesKernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesLimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesEqualizerOfPreservesKernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesLimit K F
[PROOFSTEP]
apply preservesLimitOfIsoDiagram F (diagramIsoParallelPair K).symm
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
⊢ PreservesFiniteLimits F
[PROOFSTEP]
letI := preservesEqualizersOfPreservesKernels F
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
this : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizersOfPreservesKernels F
⊢ PreservesFiniteLimits F
[PROOFSTEP]
letI := preservesTerminalObjectOfPreservesZeroMorphisms F
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
this✝ : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizersOfPreservesKernels F
this : PreservesLimit (empty C) F := preservesTerminalObjectOfPreservesZeroMorphisms F
⊢ PreservesFiniteLimits F
[PROOFSTEP]
letI := preservesLimitsOfShapePemptyOfPreservesTerminal F
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
this✝¹ : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizersOfPreservesKernels F
this✝ : PreservesLimit (empty C) F := preservesTerminalObjectOfPreservesZeroMorphisms F
this : PreservesLimitsOfShape (Discrete PEmpty) F := preservesLimitsOfShapePemptyOfPreservesTerminal F
⊢ PreservesFiniteLimits F
[PROOFSTEP]
letI : PreservesFiniteProducts F := ⟨preservesFiniteProductsOfPreservesBinaryAndTerminal F⟩
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesLimit (parallelPair f 0) F
this✝² : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizersOfPreservesKernels F
this✝¹ : PreservesLimit (empty C) F := preservesTerminalObjectOfPreservesZeroMorphisms F
this✝ : PreservesLimitsOfShape (Discrete PEmpty) F := preservesLimitsOfShapePemptyOfPreservesTerminal F
this : PreservesFiniteProducts F := { preserves := preservesFiniteProductsOfPreservesBinaryAndTerminal F }
⊢ PreservesFiniteLimits F
[PROOFSTEP]
exact preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))
[PROOFSTEP]
let bc := BinaryBicone.ofColimitCocone i
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))
[PROOFSTEP]
let presf : PreservesColimit (parallelPair bc.inr 0) F := by simpa
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
⊢ PreservesColimit (parallelPair bc.inr 0) F
[PROOFSTEP]
simpa
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
presf : PreservesColimit (parallelPair bc.inr 0) F := id inst✝
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))
[PROOFSTEP]
let hf : IsColimit bc.inrCokernelCofork := BinaryBicone.isColimitInrCokernelCofork i
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
presf : PreservesColimit (parallelPair bc.inr 0) F := id inst✝
hf : IsColimit (BinaryBicone.inrCokernelCofork bc) := BinaryBicone.isColimitInrCokernelCofork i
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))
[PROOFSTEP]
exact
  (isColimitMapCoconeBinaryCofanEquiv F ι₁ ι₂).invFun
    (BinaryBicone.isBilimitOfCokernelFst (F.mapBinaryBicone bc)
        (isColimitMapCoconeCoforkEquiv' F bc.inr_fst (isColimitOfPreserves F hf))).isColimit
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
⊢ PreservesColimit (parallelPair f g) F
[PROOFSTEP]
letI := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
⊢ PreservesColimit (parallelPair f g) F
[PROOFSTEP]
haveI := additive_of_preservesBinaryBiproducts F
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
⊢ PreservesColimit (parallelPair f g) F
[PROOFSTEP]
constructor
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
⊢ {c : Cocone (parallelPair f g)} → IsColimit c → IsColimit (F.mapCocone c)
[PROOFSTEP]
intro c i
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
let c' := isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (cokernelCoforkOfCofork (Cofork.ofπ (Cofork.π c) (_ : f ≫ Cofork.π c = g ≫ Cofork.π c))) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
dsimp only [cokernelCoforkOfCofork_ofπ] at c' 
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
let iFc := isColimitCoforkMapOfIsColimit' F _ c'
[GOAL]
case preserves
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ ((Cocones.functoriality _ F).mapIso (Cofork.isoCoforkOfπ c).symm)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
⊢ IsColimit
    ((Cocones.functoriality (parallelPair f g) F).obj (Cofork.ofπ (Cofork.π c) (_ : f ≫ Cofork.π c = g ≫ Cofork.π c)))
[PROOFSTEP]
apply (isColimitMapCoconeCoforkEquiv F (Cofork.condition c)).invFun
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
⊢ IsColimit (Cofork.ofπ (F.map (Cofork.π c)) (_ : F.map f ≫ F.map (Cofork.π c) = F.map g ≫ F.map (Cofork.π c)))
[PROOFSTEP]
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl _) (Iso.refl _) (by simp) (by simp)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.left
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one))
    (_ : F.map (f - g) ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ (F.map f - F.map g)) (_ : 0 ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ 0)
⊢ IsColimit (Cofork.ofπ (F.map (Cofork.π c)) (_ : F.map f ≫ F.map (Cofork.π c) = F.map g ≫ F.map (Cofork.π c)))
[PROOFSTEP]
exact
  IsColimit.ofIsoColimit (isColimitCoforkOfCokernelCofork ((IsColimit.precomposeHomEquiv p.symm _).symm iFc))
    (Cofork.ext (Iso.refl _) (by simp))
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproductsOfPreservesBinaryCoproducts F
this : Additive F
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) (_ : (f - g) ≫ Cofork.π c = 0)) :=
  isColimitCokernelCoforkOfCofork (IsColimit.ofIsoColimit i (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)) :=
  isColimitCoforkMapOfIsColimit' F (_ : (f - g) ≫ Cofork.π c = 0) c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one))
    (_ : F.map (f - g) ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ (F.map f - F.map g)) (_ : 0 ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ 0)
⊢ Cofork.π
        (coforkOfCokernelCofork
          ((Cocones.precompose p.symm.hom).obj
            (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)))) ≫
      (Iso.refl
          (coforkOfCokernelCofork
              ((Cocones.precompose p.symm.hom).obj
                (CokernelCofork.ofπ (F.map (Cofork.π c)) (_ : F.map (f - g) ≫ F.map (Cofork.π c) = 0)))).pt).hom =
    Cofork.π (Cofork.ofπ (F.map (Cofork.π c)) (_ : F.map f ≫ F.map (Cofork.π c) = F.map g ≫ F.map (Cofork.π c)))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesColimit K F
[PROOFSTEP]
letI :=
  preservesCoequalizerOfPreservesCokernels F (K.map Limits.WalkingParallelPairHom.left)
    (K.map Limits.WalkingParallelPairHom.right)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
inst✝¹ : HasBinaryBiproducts C
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesColimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesCoequalizerOfPreservesCokernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesColimit K F
[PROOFSTEP]
apply preservesColimitOfIsoDiagram F (diagramIsoParallelPair K).symm
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
⊢ PreservesFiniteColimits F
[PROOFSTEP]
letI := preservesCoequalizersOfPreservesCokernels F
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
this : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizersOfPreservesCokernels F
⊢ PreservesFiniteColimits F
[PROOFSTEP]
letI := preservesInitialObjectOfPreservesZeroMorphisms F
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
this✝ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizersOfPreservesCokernels F
this : PreservesColimit (empty C) F := preservesInitialObjectOfPreservesZeroMorphisms F
⊢ PreservesFiniteColimits F
[PROOFSTEP]
letI := preservesColimitsOfShapePemptyOfPreservesInitial F
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
this✝¹ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizersOfPreservesCokernels F
this✝ : PreservesColimit (empty C) F := preservesInitialObjectOfPreservesZeroMorphisms F
this : PreservesColimitsOfShape (Discrete PEmpty) F := preservesColimitsOfShapePemptyOfPreservesInitial F
⊢ PreservesFiniteColimits F
[PROOFSTEP]
letI : PreservesFiniteCoproducts F := ⟨preservesFiniteCoproductsOfPreservesBinaryAndInitial F⟩
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Preadditive C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : Preadditive D
F : C ⥤ D
inst✝⁶ : PreservesZeroMorphisms F
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : {X Y : C} → (f : X ⟶ Y) → PreservesColimit (parallelPair f 0) F
this✝² : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizersOfPreservesCokernels F
this✝¹ : PreservesColimit (empty C) F := preservesInitialObjectOfPreservesZeroMorphisms F
this✝ : PreservesColimitsOfShape (Discrete PEmpty) F := preservesColimitsOfShapePemptyOfPreservesInitial F
this : PreservesFiniteCoproducts F := { preserves := preservesFiniteCoproductsOfPreservesBinaryAndInitial F }
⊢ PreservesFiniteColimits F
[PROOFSTEP]
exact preservesFiniteColimitsOfPreservesCoequalizersAndFiniteCoproducts F
