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.
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 : ι)
:
(HomologicalComplex.quasiIso C c).IsInvertedBy (HomologicalComplex.homologyFunctor C c i)
@[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
- HomologicalComplexUpToQuasiIso C c = (HomologicalComplex.quasiIso C c).Localization'
Instances For
@[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]
:
The localization functor HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c.
Equations
Instances For
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 : ι)
:
The homology functor HomologicalComplexUpToQuasiIso C c ⥤ C for each i : ι.
Equations
Instances For
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 : ι)
:
The homology functor on HomologicalComplexUpToQuasiIso C c is induced by
the homology functor on HomologicalComplex C c.
Equations
Instances For
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)
:
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 HomologicalComplexUpToQuasiIso.Q
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]
:
The class of quasi-isomorphisms in the homotopy category.
Equations
- HomotopyCategory.quasiIso C c f = ∀ (i : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c i).map f)
Instances For
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)
:
HomotopyCategory.quasiIso C c f ↔ ∀ (n : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c n).map f)
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)
:
HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
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]
:
(HomotopyCategory.quasiIso C c).RespectsIso
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 : ι)
:
(HomotopyCategory.quasiIso C c).IsInvertedBy (HomotopyCategory.homologyFunctor C c i)
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]
:
HomotopyCategory.quasiIso C c = (HomologicalComplex.quasiIso C c).map (HomotopyCategory.quotient C c)
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]
:
The condition on a complex shape c saying that homotopic maps become equal in
the localized category with respect to quasi-isomorphisms.
- areEqualizedByLocalization {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) : CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g
Instances
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)
:
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]
:
The functor HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c from the homotopy
category to the localized category with respect to quasi-isomorphisms.
Equations
Instances For
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]
:
The canonical isomorphism HomotopyCategory.quotient C c ⋙ Qh ≅ Q.
Equations
Instances For
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 HomologicalComplexUpToQuasiIso.Qh
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 HomologicalComplexUpToQuasiIso.Qh).IsLocalization
(HomologicalComplex.quasiIso C c)
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 : ι)
:
The homology functor on HomologicalComplexUpToQuasiIso C c is induced by
the homology functor on HomotopyCategory C c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)]
:
HomologicalComplexUpToQuasiIso.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.
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]
:
The homotopy category satisfies the universal property of the localized category with respect to homotopy equivalences.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
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
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 ι))
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
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 ℤ))
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
def
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[F.Additive]
[F.PreservesHomology]
:
The localizer morphism which expresses that F.mapHomologicalComplex c preserves
quasi-isomorphisms.
Equations
- F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c = { functor := F.mapHomologicalComplex c, map := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[F.Additive]
[F.PreservesHomology]
:
(F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).functor = F.mapHomologicalComplex c
theorem
CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[(HomologicalComplex.quasiIso D c).HasLocalization]
[F.Additive]
[F.PreservesHomology]
:
(HomologicalComplex.quasiIso C c).IsInvertedBy ((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q)
noncomputable def
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[(HomologicalComplex.quasiIso D c).HasLocalization]
[F.Additive]
[F.PreservesHomology]
[(HomologicalComplex.quasiIso C c).HasLocalization]
:
The functor HomologicalComplexUpToQuasiIso C c ⥤ HomologicalComplexUpToQuasiIso D c
induced by a functor F : C ⥤ D which preserves homology.
Equations
- F.mapHomologicalComplexUpToQuasiIso c = (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).localizedFunctor HomologicalComplexUpToQuasiIso.Q HomologicalComplexUpToQuasiIso.Q
Instances For
noncomputable instance
CategoryTheory.Functor.instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[(HomologicalComplex.quasiIso D c).HasLocalization]
[F.Additive]
[F.PreservesHomology]
[(HomologicalComplex.quasiIso C c).HasLocalization]
:
CategoryTheory.Localization.Lifting HomologicalComplexUpToQuasiIso.Q (HomologicalComplex.quasiIso C c)
((F.mapHomologicalComplex c).comp HomologicalComplexUpToQuasiIso.Q) (F.mapHomologicalComplexUpToQuasiIso c)
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactors
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.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
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.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
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
CategoryTheory.Functor.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.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)]
:
CategoryTheory.Localization.Lifting HomologicalComplexUpToQuasiIso.Qh (HomotopyCategory.quasiIso C c)
((F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh) (F.mapHomologicalComplexUpToQuasiIso c)
Equations
- F.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso c = { iso' := F.mapHomologicalComplexUpToQuasiIsoFactorsh c }
theorem
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
{c : ComplexShape ι}
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.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) = CategoryTheory.CategoryStruct.comp
((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
(CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K)
(CategoryTheory.CategoryStruct.comp
((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K))
(HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K))))
theorem
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(F : CategoryTheory.Functor C D)
{ι : Type u_3}
{c : ComplexShape ι}
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp
((F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K)) h = CategoryTheory.CategoryStruct.comp
((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
(CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K)
(CategoryTheory.CategoryStruct.comp
((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K))
(CategoryTheory.CategoryStruct.comp
(HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)) h)))