C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) (0 + 1) 0 =
    F.map (HomologicalComplex.d P.complex 1 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ (HomologicalComplex.xPrevIso ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
            (_ : 0 + 1 = 0 + 1)).symm.hom ≫
      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    F.map (HomologicalComplex.d P.complex 1 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom
simp only [Iso.symm_hom, HomologicalComplex.xPrevIso_comp_dTo]
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ F.map (HomologicalComplex.d P.complex (0 + 1) 0) = F.map (HomologicalComplex.d P.complex 1 0)
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) (0 + 1) 0 =
    F.map (HomologicalComplex.d P.complex 1 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom
simp only [mapHomologicalComplex_obj_d, Iso.refl_hom, Category.comp_id]
no goals
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ F.map (HomologicalComplex.d P.complex (0 + 1) 0) = F.map (HomologicalComplex.d P.complex 1 0)
rfl
no goals
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom ≫ F.map (HomologicalComplex.Hom.f P.π 0) =
    F.map (HomologicalComplex.Hom.f P.π 0) ≫
      (Iso.refl (F.obj (HomologicalComplex.X ((ChainComplex.single₀ C).obj X) 0))).hom
simp