Documentation

Mathlib.Algebra.Homology.Localization

The category of homological complexes up to quasi-isomorphisms

Given a category C with homology and any complex shape c, we define the category HomologicalComplexUpToQuasiIso C c which is the localized category of HomologicalComplex C c with respect to quasi-isomorphisms. When C is abelian, this will be the derived category of C in the particular case of the complex shape ComplexShape.up ℤ.

Under suitable assumptions on c (e.g. chain complexes, or cochain complexes indexed by ℤ), we shall show that HomologicalComplexUpToQuasiIso C c is also the localized category of HomotopyCategory C c with respect to the class of quasi-isomorphisms.

source
theorem HomologicalComplex.homologyFunctor_inverts_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] (i : ι) :
(quasiIso C c).IsInvertedBy (homologyFunctor C c i)
source
@[reducible, inline]
abbrev HomologicalComplexUpToQuasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] :
Type (max (max u_1 u_2) u_3)

The category of homological complexes up to quasi-isomorphisms.

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev HomologicalComplexUpToQuasiIso.Q {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] :
      CategoryTheory.Functor (HomologicalComplex C c) (HomologicalComplexUpToQuasiIso C c)

      The localization functor HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c.

      Equations
        Instances For
          source
          noncomputable def HomologicalComplexUpToQuasiIso.homologyFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] (i : ι) :
          CategoryTheory.Functor (HomologicalComplexUpToQuasiIso C c) C

          The homology functor HomologicalComplexUpToQuasiIso C c ⥤ C for each i : ι.

          Equations
            Instances For
              source
              noncomputable def HomologicalComplexUpToQuasiIso.homologyFunctorFactors (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] (i : ι) :
              Q.comp (homologyFunctor C c i) ≅ HomologicalComplex.homologyFunctor C c i

              The homology functor on HomologicalComplexUpToQuasiIso C c is induced by the homology functor on HomologicalComplex C c.

              Equations
                Instances For
                  source
                  theorem HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] {K L : HomologicalComplex C c} (f : K ⟶ L) :
                  CategoryTheory.IsIso (Q.map f) ↔ HomologicalComplex.quasiIso C c f
                  source
                  theorem HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] :
                  (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy Q
                  source
                  def HomotopyCategory.quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
                  CategoryTheory.MorphismProperty (HomotopyCategory C c)

                  The class of quasi-isomorphisms in the homotopy category.

                  Equations
                    Instances For
                      source
                      theorem HomotopyCategory.mem_quasiIso_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {X Y : HomotopyCategory C c} (f : X ⟶ Y) :
                      quasiIso C c f ↔ ∀ (n : ι), CategoryTheory.IsIso ((homologyFunctor C c n).map f)
                      source
                      theorem HomotopyCategory.quotient_map_mem_quasiIso_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : HomologicalComplex C c} (f : K ⟶ L) :
                      quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
                      source
                      instance HomotopyCategory.respectsIso_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
                      (quasiIso C c).RespectsIso
                      source
                      theorem HomotopyCategory.homologyFunctor_inverts_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (i : ι) :
                      (quasiIso C c).IsInvertedBy (homologyFunctor C c i)
                      source
                      theorem HomotopyCategory.quasiIso_eq_quasiIso_map_quotient (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
                      quasiIso C c = (HomologicalComplex.quasiIso C c).map (quotient C c)
                      source
                      class ComplexShape.QFactorsThroughHomotopy {ι : Type u_3} (c : ComplexShape ι) (C : Type u_4) [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
                      Prop

                      The condition on a complex shape c saying that homotopic maps become equal in the localized category with respect to quasi-isomorphisms.

                      Instances
                        source
                        theorem HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) :
                        Q.map f = Q.map g
                        source
                        def HomologicalComplexUpToQuasiIso.Qh {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] :
                        CategoryTheory.Functor (HomotopyCategory C c) (HomologicalComplexUpToQuasiIso C c)

                        The functor HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c from the homotopy category to the localized category with respect to quasi-isomorphisms.

                        Equations
                          Instances For
                            source
                            def HomologicalComplexUpToQuasiIso.quotientCompQhIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] :
                            (HomotopyCategory.quotient C c).comp Qh ≅ Q

                            The canonical isomorphism HomotopyCategory.quotient C c ⋙ Qh ≅ Q.

                            Equations
                              Instances For
                                source
                                theorem HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] :
                                (HomotopyCategory.quasiIso C c).IsInvertedBy Qh
                                source
                                instance HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] :
                                ((HomotopyCategory.quotient C c).comp Qh).IsLocalization (HomologicalComplex.quasiIso C c)
                                source
                                noncomputable def HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] (i : ι) :
                                Qh.comp (homologyFunctor C c i) ≅ HomotopyCategory.homologyFunctor C c i

                                The homology functor on HomologicalComplexUpToQuasiIso C c is induced by the homology functor on HomotopyCategory C c.

                                Equations
                                  Instances For
                                    source
                                    instance HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] :
                                    Qh.IsLocalization (HomotopyCategory.quasiIso C c)

                                    The category HomologicalComplexUpToQuasiIso C c which was defined as a localization of HomologicalComplex C c with respect to quasi-isomorphisms also identify to a localization of the homotopy category with respect ot quasi-isomorphisms.

                                    source
                                    def ComplexShape.strictUniversalPropertyFixedTargetQuotient {ι : Type u_1} (c : ComplexShape ι) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (C : Type u_2) [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] :
                                    CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) E

                                    The homotopy category satisfies the universal property of the localized category with respect to homotopy equivalences.

                                    Equations
                                      Instances For
                                        source
                                        theorem ComplexShape.quotient_isLocalization {ι : Type u_1} (c : ComplexShape ι) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] :
                                        (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
                                        source
                                        theorem ComplexShape.QFactorsThroughHomotopy_of_exists_prev {ι : Type u_1} (c : ComplexShape ι) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] :
                                        c.QFactorsThroughHomotopy C
                                        source
                                        instance instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} [CategoryTheory.Preadditive C] [AddRightCancelSemigroup ι] [One ι] [CategoryTheory.Limits.HasBinaryBiproducts C] :
                                        (HomotopyCategory.quotient C (ComplexShape.down ι)).IsLocalization (HomologicalComplex.homotopyEquivalences C (ComplexShape.down ι))
                                        source
                                        instance instQFactorsThroughHomotopyDown (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] {ι : Type u_2} [CategoryTheory.Preadditive C] [AddRightCancelSemigroup ι] [One ι] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] :
                                        (ComplexShape.down ι).QFactorsThroughHomotopy C
                                        source
                                        instance instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] :
                                        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).IsLocalization (HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ))
                                        source
                                        instance instQFactorsThroughHomotopyIntUp (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.CategoryWithHomology C] :
                                        (ComplexShape.up ℤ).QFactorsThroughHomotopy C
                                        source
                                        def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [F.Additive] [F.PreservesHomology] :
                                        LocalizerMorphism (HomologicalComplex.quasiIso C c) (HomologicalComplex.quasiIso D c)

                                        The localizer morphism which expresses that F.mapHomologicalComplex c preserves quasi-isomorphisms.

                                        Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [F.Additive] [F.PreservesHomology] :
                                            (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).functor = F.mapHomologicalComplex c
                                            source
                                            theorem CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] :
                                            (HomologicalComplex.quasiIso C c).IsInvertedBy ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q)
                                            source
                                            noncomputable def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] :
                                            Functor (HomologicalComplexUpToQuasiIso C c) (HomologicalComplexUpToQuasiIso D c)

                                            The functor HomologicalComplexUpToQuasiIso C c ⥤ HomologicalComplexUpToQuasiIso D c induced by a functor F : C ⥤ D which preserves homology.

                                            Equations
                                              Instances For
                                                source
                                                noncomputable instance CategoryTheory.Functor.instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] :
                                                Localization.Lifting HomologicalComplexUpToQuasiIso.Q (HomologicalComplex.quasiIso C c) ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q) (F.mapHomologicalComplexUpToQuasiIso c)
                                                Equations
                                                  source
                                                  noncomputable def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactors {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] :
                                                  HomologicalComplexUpToQuasiIso.Q.comp (F.mapHomologicalComplexUpToQuasiIso c) ≅ (F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q

                                                  The functor F.mapHomologicalComplexUpToQuasiIso c is induced by F.mapHomologicalComplex c.

                                                  Equations
                                                    Instances For
                                                      source
                                                      noncomputable def CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] :
                                                      HomologicalComplexUpToQuasiIso.Qh.comp (F.mapHomologicalComplexUpToQuasiIso c) ≅ (F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh

                                                      The functor F.mapHomologicalComplexUpToQuasiIso c is induced by F.mapHomotopyCategory c.

                                                      Equations
                                                        Instances For
                                                          source
                                                          noncomputable instance CategoryTheory.Functor.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C D) {ι : Type u_3} (c : ComplexShape ι) [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] :
                                                          Localization.Lifting HomologicalComplexUpToQuasiIso.Qh (HomotopyCategory.quasiIso C c) ((F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh) (F.mapHomologicalComplexUpToQuasiIso c)
                                                          Equations
                                                            source
                                                            theorem CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (F : Functor C D) {ι : Type u_3} {c : ComplexShape ι} [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] (K : HomologicalComplex C c) :
                                                            (F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K) = CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K)) (CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K) (CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K)) (HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K))))
                                                            source
                                                            theorem CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (F : Functor C D) {ι : Type u_3} {c : ComplexShape ι} [Preadditive C] [Preadditive D] [CategoryWithHomology C] [CategoryWithHomology D] [(HomologicalComplex.quasiIso D c).HasLocalization] [F.Additive] [F.PreservesHomology] [(HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C] [c.QFactorsThroughHomotopy D] [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)] (K : HomologicalComplex C c) {Z : HomologicalComplexUpToQuasiIso D c} (h : HomologicalComplexUpToQuasiIso.Qh.obj ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K)) ⟶ Z) :
                                                            CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K)) h = CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K)) (CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K) (CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K)) (CategoryStruct.comp (HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)) h)))