Theorems · Theorem · category theory

HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj

∀ (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 : ι),
  (HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C c i).hom.app ((HomotopyCategory.quotient C c).obj K) =
    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)
        ((HomotopyCategory.homologyFunctorFactors C c i).inv.app K))

Defined in

Mathlib.Algebra.Homology.Localization

Cited by

2 results in Mathlib

Foundations

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

Assumes

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