Theorems · Theorem · category theory

HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc

∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C]
  (K : HomologicalComplex C c) (i : ι) {Z : C}
  (h : (HomotopyCategory.homologyFunctor C c i).obj ((HomotopyCategory.quotient C c).obj K) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C c i).hom.app ((HomotopyCategory.quotient C c).obj K))
      h =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplexUpToQuasiIso.homologyFunctor C c i).map
        ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i).hom.app K)
        (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C c i).inv.app K) h))

Defined in

Mathlib.Algebra.Homology.Localization

Cited by

0 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryWithHomologyCategoryTheory.MorphismProperty.HasLocalizationComplexShape.QFactorsThroughHomotopy