no goals
ι : Type ?u.262154
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type ?u.262509
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
⊢ X ((Functor.mapHomologicalComplex G c).obj C) i ⟶ X ((Functor.mapHomologicalComplex G c).obj D) j
exact G.map (hom i j)
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i : ι
⊢ Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap hom)) i =
    Hom.f (nullHomotopicMap fun i j => G.map (hom i j)) i
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
⊢ (Functor.mapHomologicalComplex G c).map (nullHomotopicMap hom) = nullHomotopicMap fun i j => G.map (hom i j)
ext i
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i : ι
⊢ G.map
      (d C i (ComplexShape.next c i) ≫ hom (ComplexShape.next c i) i +
        hom i (ComplexShape.prev c i) ≫ d D (ComplexShape.prev c i) i) =
    G.map (d C i (ComplexShape.next c i)) ≫ G.map (hom (ComplexShape.next c i) i) +
      G.map (hom i (ComplexShape.prev c i)) ≫ G.map (d D (ComplexShape.prev c i) i)
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i : ι
⊢ Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap hom)) i =
    Hom.f (nullHomotopicMap fun i j => G.map (hom i j)) i
dsimp [nullHomotopicMap, dNext, prevD]
no goals
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i : ι
⊢ G.map
      (d C i (ComplexShape.next c i) ≫ hom (ComplexShape.next c i) i +
        hom i (ComplexShape.prev c i) ≫ d D (ComplexShape.prev c i) i) =
    G.map (d C i (ComplexShape.next c i)) ≫ G.map (hom (ComplexShape.next c i) i) +
      G.map (hom i (ComplexShape.prev c i)) ≫ G.map (d D (ComplexShape.prev c i) i)
simp only [G.map_comp, Functor.map_add]