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 (TODO).
@[inline, reducible]
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]
[CategoryTheory.MorphismProperty.HasLocalization (HomologicalComplex.quasiIso C c)]
:
Type (max (max u_1 u_2) u_3)
The category of homological complexes up to quasi-isomorphisms.
Equations
Instances For
@[inline, reducible]
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]
[CategoryTheory.MorphismProperty.HasLocalization (HomologicalComplex.quasiIso C c)]
:
The localization functor HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c.
Equations
- HomologicalComplexUpToQuasiIso.Q = CategoryTheory.MorphismProperty.Q' (HomologicalComplex.quasiIso C c)
Instances For
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 : ι)
:
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]
[CategoryTheory.MorphismProperty.HasLocalization (HomologicalComplex.quasiIso C c)]
(i : ι)
:
The homology functor HomologicalComplexUpToQuasiIso C c ⥤ C for each i : ι.
Equations
- One or more equations did not get rendered due to their size.
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]
[CategoryTheory.MorphismProperty.HasLocalization (HomologicalComplex.quasiIso C c)]
(i : ι)
:
CategoryTheory.Functor.comp HomologicalComplexUpToQuasiIso.Q (HomologicalComplexUpToQuasiIso.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
- One or more equations did not get rendered due to their size.
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]
[CategoryTheory.MorphismProperty.HasLocalization (HomologicalComplex.quasiIso C c)]
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
:
CategoryTheory.IsIso (HomologicalComplexUpToQuasiIso.Q.toPrefunctor.map f) ↔ HomologicalComplex.quasiIso C c f
theorem
HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences
(C : Type u_1)
[CategoryTheory.Category.{u_3, u_1} C]
{ι : Type u_2}
(c : ComplexShape ι)
[CategoryTheory.Preadditive C]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.MorphismProperty.HasLocalization (HomologicalComplex.quasiIso C c)]
:
CategoryTheory.MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c)
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).toPrefunctor.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 : HomotopyCategory C c}
{Y : HomotopyCategory C c}
(f : X ⟶ Y)
:
HomotopyCategory.quasiIso C c f ↔ ∀ (n : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c n).toPrefunctor.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 : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
:
HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).toPrefunctor.map f) ↔ HomologicalComplex.quasiIso C c f
theorem
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]
:
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 : ι)
:
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}, Homotopy f g → CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g