Limits of degreewise eventually constant systems

Let F : J ⥤ HomologicalComplex C c be a functor from a cofiltered category such that for any degree q, the functor F ⋙ eval C c q : J ⥤ C is eventually constant. Let cF be a limit cone for F. For a given degree q, we show that for suitable j : J, the map (cF.π.app j).f q is an isomorphism, and that cf.π.app j is a quasi-isomorphism in degree q.

theorem HomologicalComplex.isIso_π_f_of_isLimit_of_isEventuallyConstantTo {C : Type u_1} {J : Type u_2} {ι : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} J] {c : ComplexShape ι} [CategoryTheory.IsCofiltered J] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (j : ι), CategoryTheory.Limits.HasLimit (F.comp (eval C c j))] {cF : CategoryTheory.Limits.Cone F} (hcF : CategoryTheory.Limits.IsLimit cF) (q : ι) (j : J) (hq : (F.comp (eval C c q)).IsEventuallyConstantTo j) : CategoryTheory.IsIso ((cF.π.app j).f q)

theorem HomologicalComplex.quasiIsoAt_π_of_isLimit_of_isEventuallyConstantTo {C : Type u_1} {J : Type u_2} {ι : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} J] {c : ComplexShape ι} [CategoryTheory.IsCofiltered J] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (j : ι), CategoryTheory.Limits.HasLimit (F.comp (eval C c j))] {cF : CategoryTheory.Limits.Cone F} (hcF : CategoryTheory.Limits.IsLimit cF) [CategoryTheory.CategoryWithHomology C] (q₀ q₁ q₂ : ι) (h₀ : c.prev q₁ = q₀) (h₂ : c.next q₁ = q₂) (j : J) (hq₀ : (F.comp (eval C c q₀)).IsEventuallyConstantTo j) (hq₁ : (F.comp (eval C c q₁)).IsEventuallyConstantTo j) (hq₂ : (F.comp (eval C c q₂)).IsEventuallyConstantTo j) : QuasiIsoAt (cF.π.app j) q₁