The bounded below derived category

Let C be an abelian category. In this file, we show that the bounded below derived category DerivedCategory.Plus C (defined as a full subcategory of DerivedCategory C) is the localization of the bounded below homotopy category HomotopyCategory.Plus C with respect to quasi-isomorphisms.

@[reducible, inline]

abbrev HomotopyCategory.Plus.subcategoryAcyclic (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.ObjectProperty (Plus C)

The property of objects in HomotopyCategory.Plus C that is satisfied by acyclic complexes.

Equations

• HomotopyCategory.Plus.subcategoryAcyclic C = (HomotopyCategory.subcategoryAcyclic C).inverseImage (HomotopyCategory.Plus.ι C)

theorem HomotopyCategory.Plus.quasiIso_eq_subcategoryAcyclic_trW (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : quasiIso C = (subcategoryAcyclic C).trW

noncomputable def DerivedCategory.Plus.Qh {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (HomotopyCategory.Plus C) (Plus C)

The localization functor HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C.

Equations

• DerivedCategory.Plus.Qh = DerivedCategory.TStructure.t.plus.lift ((HomotopyCategory.Plus.ι C).comp DerivedCategory.Qh) ⋯

@[implicit_reducible]

noncomputable instance DerivedCategory.Plus.instCommShiftPlusQhInt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.CommShift ℤ

Equations

• DerivedCategory.Plus.instCommShiftPlusQhInt = id inferInstance

instance DerivedCategory.Plus.instIsTriangulatedPlusQh {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.IsTriangulated

theorem DerivedCategory.Plus.Qh_map_bijective_of_isKInjective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K L : HomotopyCategory.Plus C) : CochainComplex.IsKInjective L.obj.as → Function.Bijective Qh.map

instance DerivedCategory.Plus.instIsVerdierRightLocalizingHomotopyCategoryIntUpPlusSubcategoryAcyclic {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (HomotopyCategory.plus C).IsVerdierRightLocalizing (HomotopyCategory.subcategoryAcyclic C)

noncomputable def DerivedCategory.Plus.QhCompιIsoιCompQh (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.comp ι ≅ (HomotopyCategory.Plus.ι C).comp DerivedCategory.Qh

The functor DerivedCategory.Plus.Qh : HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C is induced by DerivedCategory.Qh : HomotopyCategory C (.up ℤ) ⥤ DerivedCategory C.

Equations

• DerivedCategory.Plus.QhCompιIsoιCompQh C = CategoryTheory.Iso.refl (DerivedCategory.Plus.Qh.comp DerivedCategory.Plus.ι)

instance DerivedCategory.Plus.instEssSurjPlusQh (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.EssSurj

instance DerivedCategory.Plus.instIsLocalizationPlusQhTrWSubcategoryAcyclic (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.IsLocalization (HomotopyCategory.Plus.subcategoryAcyclic C).trW

instance DerivedCategory.Plus.instIsLocalizationPlusQhQuasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.IsLocalization (HomotopyCategory.Plus.quasiIso C)

noncomputable def DerivedCategory.Plus.singleFunctors (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.SingleFunctors C (Plus C) ℤ

The single functors C ⥤ DerivedCategory.Plus C for all n : ℤ along with their compatibilities with shifts.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev DerivedCategory.Plus.singleFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : CategoryTheory.Functor C (Plus C)

The single functor C ⥤ DerivedCategory.Plus C which sends X : C to the single cochain complex with X sitting in degree n : ℤ.

Equations

• DerivedCategory.Plus.singleFunctor C n = (DerivedCategory.Plus.singleFunctors C).functor n

noncomputable def DerivedCategory.Plus.singleFunctorιIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctor C n).comp ι ≅ DerivedCategory.singleFunctor C n

The single functors on DerivedCategory.Plus C are induced by the single functors on DerivedCategory C.

Equations

• DerivedCategory.Plus.singleFunctorιIso C n = CategoryTheory.Iso.refl ((DerivedCategory.Plus.singleFunctor C n).comp DerivedCategory.Plus.ι)

instance DerivedCategory.Plus.instAdditiveSingleFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctor C n).Additive

noncomputable def DerivedCategory.Plus.homologyFunctor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : CategoryTheory.Functor (Plus C) C

The homology functor DerivedCategory.Plus C ⥤ C in degree n : ℤ.

Equations

• DerivedCategory.Plus.homologyFunctor C n = DerivedCategory.Plus.ι.comp (DerivedCategory.homologyFunctor C n)

instance DerivedCategory.Plus.instIsHomologicalHomologyFunctor (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (homologyFunctor C n).IsHomological

instance DerivedCategory.Plus.instEssSurjArrowPlusMapArrowQh (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Qh.mapArrow.EssSurj

@[reducible, inline]

noncomputable abbrev DerivedCategory.Plus.TStructure.t {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Triangulated.TStructure (Plus C)

The canonical t-structure on DerivedCategory.Plus C.

Equations

• DerivedCategory.Plus.TStructure.t = DerivedCategory.TStructure.t.plus.tStructure DerivedCategory.TStructure.t

@[reducible, inline]

abbrev DerivedCategory.Plus.IsGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) : Prop

Given X : DerivedCategory.Plus C and n : ℤ, this property means that X is ≥ n for the canonical t-structure.

Equations

• X.IsGE n = DerivedCategory.Plus.TStructure.t.IsGE X n

@[reducible, inline]

abbrev DerivedCategory.Plus.IsLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) : Prop

Given X : DerivedCategory.Plus C and n : ℤ, this property means that X is ≤ n for the canonical t-structure.

Equations

• X.IsLE n = DerivedCategory.Plus.TStructure.t.IsLE X n

theorem DerivedCategory.Plus.isGE_ι_obj_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) : (ι.obj X).IsGE n ↔ X.IsGE n

theorem DerivedCategory.Plus.isLE_ι_obj_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) : (ι.obj X).IsLE n ↔ X.IsLE n

instance DerivedCategory.Plus.instIsGEObjιOfIsGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) [X.IsGE n] : (ι.obj X).IsGE n

instance DerivedCategory.Plus.instIsLEObjιOfIsLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) [X.IsLE n] : (ι.obj X).IsLE n

@[implicit_reducible]

noncomputable instance DerivedCategory.Plus.instShiftSequenceHomologyFunctorOfNatInt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (homologyFunctor C 0).ShiftSequence ℤ

Equations

• One or more equations did not get rendered due to their size.

instance DerivedCategory.Plus.instIsGEObjSingleFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsGE n

instance DerivedCategory.Plus.instIsLEObjSingleFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsLE n

theorem DerivedCategory.Plus.isZero_homology_of_isGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) [X.IsGE n] (i : ℤ) (hi : i < n) : CategoryTheory.Limits.IsZero ((homologyFunctor C i).obj X)

theorem DerivedCategory.Plus.isZero_homology_of_isLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : Plus C) (n : ℤ) [X.IsLE n] (i : ℤ) (hi : n < i) : CategoryTheory.Limits.IsZero ((homologyFunctor C i).obj X)

theorem DerivedCategory.Plus.isIso_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : Plus C} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((homologyFunctor C n).map f)

noncomputable def DerivedCategory.Plus.Q {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (CochainComplex.Plus C) (Plus C)

The localization functor CochainComplex.Plus C ⥤ DerivedCategory.Plus C.

Equations

• DerivedCategory.Plus.Q = (HomotopyCategory.Plus.quotient C).comp DerivedCategory.Plus.Qh