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 : ι)
:
(quasiIso C c).IsInvertedBy (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
@[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
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 : ι.
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.
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]
:
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)
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)
:
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)
:
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
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)
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]
:
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.
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.
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]
:
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)
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.
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)]
:
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.
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]
:
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]
:
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]
:
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]
:
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]
:
The localizer morphism which expresses that F.mapHomologicalComplex c preserves
quasi-isomorphisms.
Equations
- F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c = { functor := F.mapHomologicalComplex c, map := ⋯ }
@[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]
:
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]
:
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]
:
The functor HomologicalComplexUpToQuasiIso C c ⥤ HomologicalComplexUpToQuasiIso D c
induced by a functor F : C ⥤ D which preserves homology.
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]
:
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}
[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]
:
The functor F.mapHomologicalComplexUpToQuasiIso c is induced by
F.mapHomologicalComplex c.
Equations
- One or more equations did not get rendered due to their size.
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)]
:
The functor F.mapHomologicalComplexUpToQuasiIso c is induced by
F.mapHomotopyCategory c.
Equations
- One or more equations did not get rendered due to their size.
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)]
:
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))))
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)))