ι : Type u_3
V : Type u
inst✝¹⁴ : Category V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category A
inst✝⁶ : Abelian A
B : Type u_5
inst✝⁵ : Category B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso
    ((homologyFunctorIso F i).hom.app C ≫
      (homologyFunctor B c i).map ((mapHomologicalComplex F c).map f) ≫ (homologyFunctorIso F i).inv.app D)
ι : Type u_3
V : Type u
inst✝¹⁴ : Category V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category A
inst✝⁶ : Abelian A
B : Type u_5
inst✝⁵ : Category B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso (F.map ((homologyFunctor A c i).map f))
rw [← Functor.comp_map, ← NatIso.naturality_2 (F.homologyFunctorIso i) f, Functor.comp_map]
no goals
ι : Type u_3
V : Type u
inst✝¹⁴ : Category V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category A
inst✝⁶ : Abelian A
B : Type u_5
inst✝⁵ : Category B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso
    ((homologyFunctorIso F i).hom.app C ≫
      (homologyFunctor B c i).map ((mapHomologicalComplex F c).map f) ≫ (homologyFunctorIso F i).inv.app D)
infer_instance