[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
