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.
@[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
- HomologicalComplexUpToQuasiIso.Q = (HomologicalComplex.quasiIso C c).Q'
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 : ι)
:
(HomologicalComplex.quasiIso C c).IsInvertedBy (HomologicalComplex.homologyFunctor C 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]
[(HomologicalComplex.quasiIso C c).HasLocalization]
(i : ι)
:
The homology functor HomologicalComplexUpToQuasiIso C c ⥤ C for each i : ι.
Equations
- HomologicalComplexUpToQuasiIso.homologyFunctor C c i = CategoryTheory.Localization.lift (HomologicalComplex.homologyFunctor C c i) ⋯ HomologicalComplexUpToQuasiIso.Q
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 : ι)
:
HomologicalComplexUpToQuasiIso.Q.comp (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
- HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i = CategoryTheory.Localization.fac (HomologicalComplex.homologyFunctor C c i) ⋯ HomologicalComplexUpToQuasiIso.Q
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 : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
:
CategoryTheory.IsIso (HomologicalComplexUpToQuasiIso.Q.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]
[(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 : HomotopyCategory C c}
{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 : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
:
HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).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]
:
(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}, Homotopy f g → CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g
Instances
theorem
ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization
{ι : Type u_3}
{c : ComplexShape ι}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.CategoryWithHomology C]
[self : c.QFactorsThroughHomotopy C]
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{f : K ⟶ L}
{g : K ⟶ L}
(h : Homotopy f g)
:
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 : HomologicalComplex C c}
{L : HomologicalComplex C c}
{f : K ⟶ L}
{g : K ⟶ L}
(h : Homotopy f g)
:
HomologicalComplexUpToQuasiIso.Q.map f = HomologicalComplexUpToQuasiIso.Q.map 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
- HomologicalComplexUpToQuasiIso.Qh = CategoryTheory.Quotient.lift (homotopic C c) HomologicalComplexUpToQuasiIso.Q ⋯
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]
:
(HomotopyCategory.quotient C c).comp HomologicalComplexUpToQuasiIso.Qh ≅ HomologicalComplexUpToQuasiIso.Q
The canonical isomorphism HomotopyCategory.quotient C c ⋙ Qh ≅ Q.
Equations
- HomologicalComplexUpToQuasiIso.quotientCompQhIso C c = CategoryTheory.Quotient.lift.isLift (homotopic C c) HomologicalComplexUpToQuasiIso.Q ⋯
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)
Equations
- ⋯ = ⋯
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 : ι)
:
HomologicalComplexUpToQuasiIso.Qh.comp (HomologicalComplexUpToQuasiIso.homologyFunctor C c i) ≅ HomotopyCategory.homologyFunctor C 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.
Equations
- ⋯ = ⋯
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 ι))
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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 ℤ))
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯