[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.Hom.f P.π (n + 1) = 0
[PROOFSTEP]
apply zero_of_target_iso_zero
[GOAL]
case i
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) (n + 1) ≅ 0
[PROOFSTEP]
dsimp
[GOAL]
case i
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ 0 ≅ 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ Epi (HomologicalComplex.Hom.f P.π n)
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
⊢ Epi (HomologicalComplex.Hom.f P.π Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi (HomologicalComplex.Hom.f P.π (Nat.succ n✝))
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
⊢ Epi (HomologicalComplex.Hom.f P.π 0)
[PROOFSTEP]
infer_instance
[GOAL]
case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi (HomologicalComplex.Hom.f P.π (Nat.succ n✝))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
n : ℕ
⊢ Projective (HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) n)
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
⊢ Projective (HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
⊢ Projective Z
[PROOFSTEP]
infer_instance
[GOAL]
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
n✝ : ℕ
⊢ Projective (HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) (Nat.succ n✝))
[PROOFSTEP]
dsimp
[GOAL]
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
n✝ : ℕ
⊢ Projective 0
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
⊢ Exact (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0)
    (HomologicalComplex.Hom.f (𝟙 ((ChainComplex.single₀ C).obj Z)) 0)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
⊢ Exact 0 (𝟙 Z)
[PROOFSTEP]
exact exact_zero_mono _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
n : ℕ
⊢ Exact (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1))
    (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 1) n)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
n : ℕ
⊢ Exact 0 0
[PROOFSTEP]
exact exact_of_zero _ _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
⊢ Epi (HomologicalComplex.Hom.f (𝟙 ((ChainComplex.single₀ C).obj Z)) 0)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Projective Z
⊢ Epi (𝟙 Z)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ (HomologicalComplex.d P.complex 1 0 ≫ liftZero f P Q) ≫ HomologicalComplex.Hom.f Q.π 0 = 0
[PROOFSTEP]
simp [liftZero, P.exact₀.w_assoc]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ liftOne f P Q ≫ HomologicalComplex.d Q.complex 1 0 = HomologicalComplex.d P.complex 1 0 ≫ liftZero f P Q
[PROOFSTEP]
dsimp [liftZero, liftOne]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ Exact.lift
        (HomologicalComplex.d P.complex 1 0 ≫
          factorThru (HomologicalComplex.Hom.f P.π 0 ≫ f) (HomologicalComplex.Hom.f Q.π 0))
        (HomologicalComplex.d Q.complex 1 0) (HomologicalComplex.Hom.f Q.π 0)
        (_ : Exact (HomologicalComplex.d Q.complex 1 0) (HomologicalComplex.Hom.f Q.π 0))
        (_ :
          (HomologicalComplex.d P.complex 1 0 ≫
                factorThru (HomologicalComplex.Hom.f P.π 0 ≫ f) (HomologicalComplex.Hom.f Q.π 0)) ≫
              HomologicalComplex.Hom.f Q.π 0 =
            0) ≫
      HomologicalComplex.d Q.complex 1 0 =
    HomologicalComplex.d P.complex 1 0 ≫
      factorThru (HomologicalComplex.Hom.f P.π 0 ≫ f) (HomologicalComplex.Hom.f Q.π 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
n : ℕ
g : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex n
g' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 1)
w : g' ≫ HomologicalComplex.d Q.complex (n + 1) n = HomologicalComplex.d P.complex (n + 1) n ≫ g
⊢ (HomologicalComplex.d P.complex (n + 2) (n + 1) ≫ g') ≫ HomologicalComplex.d Q.complex (n + 1) n = 0
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
n : ℕ
g : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex n
g' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 1)
w : g' ≫ HomologicalComplex.d Q.complex (n + 1) n = HomologicalComplex.d P.complex (n + 1) n ≫ g
⊢ Exact.lift (HomologicalComplex.d P.complex (n + 2) (n + 1) ≫ g') (HomologicalComplex.d Q.complex (n + 2) (n + 1))
        (HomologicalComplex.d Q.complex (n + 1) n)
        (_ : Exact (HomologicalComplex.d Q.complex (n + 2) (n + 1)) (HomologicalComplex.d Q.complex (n + 1) n))
        (_ : (HomologicalComplex.d P.complex (n + 2) (n + 1) ≫ g') ≫ HomologicalComplex.d Q.complex (n + 1) n = 0) ≫
      HomologicalComplex.d Q.complex (n + 2) (n + 1) =
    HomologicalComplex.d P.complex (n + 2) (n + 1) ≫ g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ HomologicalComplex.Hom.f (lift f P Q ≫ Q.π) 0 = HomologicalComplex.Hom.f (P.π ≫ (ChainComplex.single₀ C).map f) 0
[PROOFSTEP]
simp [lift, liftZero]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ (HomologicalComplex.Hom.f f 1 - HomologicalComplex.d P.complex 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      HomologicalComplex.d Q.complex 1 0 =
    0
[PROOFSTEP]
simp [liftHomotopyZeroZero]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
n : ℕ
g : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex (n + 1)
g' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 2)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    HomologicalComplex.d P.complex (n + 1) n ≫ g + g' ≫ HomologicalComplex.d Q.complex (n + 2) (n + 1)
⊢ (HomologicalComplex.Hom.f f (n + 2) - HomologicalComplex.d P.complex (n + 2) (n + 1) ≫ g') ≫
      HomologicalComplex.d Q.complex (n + 2) (n + 1) =
    0
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ HomologicalComplex.Hom.f f 0 = liftHomotopyZeroZero f comm ≫ HomologicalComplex.d Q.complex 1 0
[PROOFSTEP]
simp [liftHomotopyZeroZero]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ HomologicalComplex.Hom.f f 1 =
    HomologicalComplex.d P.complex 1 0 ≫ liftHomotopyZeroZero f comm +
      liftHomotopyZeroOne f comm ≫ HomologicalComplex.d Q.complex 2 1
[PROOFSTEP]
simp [liftHomotopyZeroOne]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
n : ℕ
x✝ :
  (f_1 : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex (n + 1)) ×'
    (f' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 2)) ×'
      HomologicalComplex.Hom.f f (n + 1) =
        HomologicalComplex.d P.complex (n + 1) n ≫ f_1 + f' ≫ HomologicalComplex.d Q.complex (n + 2) (n + 1)
g : HomologicalComplex.X P.complex n ⟶ HomologicalComplex.X Q.complex (n + 1)
g' : HomologicalComplex.X P.complex (n + 1) ⟶ HomologicalComplex.X Q.complex (n + 2)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    HomologicalComplex.d P.complex (n + 1) n ≫ g + g' ≫ HomologicalComplex.d Q.complex (n + 2) (n + 1)
⊢ HomologicalComplex.Hom.f f (n + 2) =
    HomologicalComplex.d P.complex (n + 2) (n + 1) ≫ { fst := g, snd := { fst := g', snd := w } }.snd.fst +
      liftHomotopyZeroSucc f n g g' w ≫ HomologicalComplex.d Q.complex (n + 3) (n + 2)
[PROOFSTEP]
simp [liftHomotopyZeroSucc, w]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
g h : P.complex ⟶ Q.complex
g_comm : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
h_comm : h ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (g - h) ≫ Q.π = 0
[PROOFSTEP]
simp [g_comm, h_comm]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X) P P) (𝟙 P.complex)
[PROOFSTEP]
apply liftHomotopy (𝟙 X)
[GOAL]
case g_comm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P : ProjectiveResolution X
⊢ lift (𝟙 X) P P ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
case h_comm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P : ProjectiveResolution X
⊢ 𝟙 P.complex ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)
[PROOFSTEP]
apply liftHomotopy (f ≫ g)
[GOAL]
case g_comm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ lift (f ≫ g) P R ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)
[PROOFSTEP]
simp
[GOAL]
case h_comm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X) P Q ≫ lift (𝟙 X) Q P) (𝟙 P.complex)
[PROOFSTEP]
refine' (liftCompHomotopy (𝟙 X) (𝟙 X) P Q P).symm.trans _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) P P) (𝟙 P.complex)
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X) P P) (𝟙 P.complex)
[PROOFSTEP]
apply liftIdHomotopy
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X) Q P ≫ lift (𝟙 X) P Q) (𝟙 Q.complex)
[PROOFSTEP]
refine' (liftCompHomotopy (𝟙 X) (𝟙 X) Q P Q).symm.trans _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) Q Q) (𝟙 Q.complex)
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X) Q Q) (𝟙 Q.complex)
[PROOFSTEP]
apply liftIdHomotopy
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ (homotopyEquiv P Q).hom ≫ Q.π = P.π
[PROOFSTEP]
simp [homotopyEquiv]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
X : C
P Q : ProjectiveResolution X
⊢ (homotopyEquiv P Q).inv ≫ P.π = Q.π
[PROOFSTEP]
simp [homotopyEquiv]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
inst✝ : HasProjectiveResolutions C
X : C
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
          map := fun {X Y} f =>
            (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
            map := fun {X Y} f =>
              (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.obj
        X)
[PROOFSTEP]
rw [← (HomotopyCategory.quotient _ _).map_id]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
inst✝ : HasProjectiveResolutions C
X : C
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
          map := fun {X Y} f =>
            (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.map
      (𝟙 X) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (𝟙 (projectiveResolution.complex X))
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
inst✝ : HasProjectiveResolutions C
X : C
⊢ Homotopy (projectiveResolution.lift (𝟙 X)) (𝟙 (projectiveResolution.complex X))
[PROOFSTEP]
apply ProjectiveResolution.liftIdHomotopy
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
inst✝ : HasProjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
          map := fun {X Y} f =>
            (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.map
      (f ≫ g) =
    { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
            map := fun {X Y} f =>
              (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.map
        f ≫
      { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
            map := fun {X Y} f =>
              (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.map
        g
[PROOFSTEP]
rw [← (HomotopyCategory.quotient _ _).map_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
inst✝ : HasProjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution.complex X),
          map := fun {X Y} f =>
            (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f) }.map
      (f ≫ g) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map (projectiveResolution.lift f ≫ projectiveResolution.lift g)
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
inst✝ : HasProjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Homotopy (projectiveResolution.lift (f ≫ g)) (projectiveResolution.lift f ≫ projectiveResolution.lift g)
[PROOFSTEP]
apply ProjectiveResolution.liftCompHomotopy


[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