The injective derivability structure

Let C be an abelian category with enough injectives. In this file, we define a localizer morphism CochainComplex.Plus.localizerMorphism (relative to quasi-isomorphisms) which is given by the (fully faithful) functor CochainComplex.Plus (InjectiveObject C) ⥤ CochainComplex.Plus C, and we show that it is a right derivability structure. (The proof proceeds by showing that up to equivalences of categories, this functor is the inclusion of the full subcategory of fibrant objects in the model category CochainComplex.Plus C.)

We also obtain a similar right derivability structure HomotopyCategory.Plus.localizerMorphism for the functor HomotopyCategory.Plus (InjectiveObject C) ⥤ HomotopyCategory.Plus C, where the target category is equipped with the class of quasi-isomorphisms while the source category HomotopyCategory.Plus (InjectiveObject C) is equipped with the class of isomorphisms (which is exactly the same as quasi-isomorphisms). The consequence is that any functor from the category HomotopyCategory.Plus C has a right derived functor, and we show that the unit natural transformation for such a derived functor is an isomorphism on objects coming from HomotopyCategory.Plus (InjectiveObject C).

instance CochainComplex.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjHomotopyCategoryPlusObjPlusInjectiveObjectMapHomotopyCategoryPlusι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : HomotopyCategory.Plus (CategoryTheory.InjectiveObject C)) (n : ℤ) : CategoryTheory.Injective (((CategoryTheory.InjectiveObject.ι C).mapHomotopyCategoryPlus.obj X).obj.as.X n)

instance CochainComplex.Plus.instIsKInjectiveObjHomologicalComplexIntInjectiveObjectUpMapHomologicalComplexιObjPlus {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : Plus (CategoryTheory.InjectiveObject C)) : IsKInjective (((CategoryTheory.InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K.obj)

theorem CochainComplex.Plus.exists_quasiIso_injective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K : Plus C) (n : ℤ) [K.obj.IsStrictlyGE n] : ∃ (L : Plus (CategoryTheory.InjectiveObject C)) (_ : L.obj.IsStrictlyGE n) (i : K ⟶ (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.obj L), quasiIso C i

theorem DerivedCategory.Plus.exists_injective_nonempty_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (K : Plus C) (n : ℤ) [K.IsGE n] : ∃ (L : CochainComplex.Plus (CategoryTheory.InjectiveObject C)) (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)

Let K be an object in the bounded below derived category of an abelian category C with enough injectives. Assume that K is cohomologically ≥ n. Then, K admits an "injective resolution", in the sense that there exists a cochain complex L consisting of injective object and lying in degrees ≥ n, such that K is isomorphic to the image of L.

def CochainComplex.Plus.localizerMorphism (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.LocalizerMorphism ((quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus) (quasiIso C)

The localizer morphism (relative to quasi-isomorphisms) that is given by the "inclusion functor" CochainComplex.Plus (InjectiveObject C) ⥤ CochainComplex.Plus C.

Equations

• CochainComplex.Plus.localizerMorphism C = { functor := (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus, map := ⋯ }

@[simp]

theorem CochainComplex.Plus.localizerMorphism_functor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (localizerMorphism C).functor = (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus

instance CochainComplex.Plus.instIsInducedInjectiveObjectInverseImageQuasiIsoMapCochainComplexPlusιLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (localizerMorphism C).IsInduced

instance CochainComplex.Plus.instInjectiveObjIsInjectiveXIntInjectiveObjectPlus {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : Plus (CategoryTheory.InjectiveObject C)) (n : ℤ) : CategoryTheory.Injective (K.obj.X n).obj

instance CochainComplex.Plus.instInjectiveXIntObjPlusFibrantObjects {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : HomotopicalAlgebra.FibrantObject (Plus C)) (n : ℤ) : CategoryTheory.Injective (K.obj.obj.X n)

def CochainComplex.Plus.fibrantObjectEquivalence (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : Plus (CategoryTheory.InjectiveObject C) ≌ HomotopicalAlgebra.FibrantObject (Plus C)

The equivalence between CochainComplex.Plus (InjectiveObject C) and the category of fibrant object in CochainComplex.Plus C for the Quillen model category structure.

Equations

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

@[reducible, inline]

abbrev CochainComplex.Plus.fibrantObjectLocalizerMorphism (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.LocalizerMorphism ((quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus) (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject (Plus C)))

The localizer morphism (relative to quasi-isomorphisms) that is given by the equivalence of categories CochainComplex.Plus (InjectiveObject C) ≌ FibrantObject (CochainComplex.Plus C).

Equations

• CochainComplex.Plus.fibrantObjectLocalizerMorphism C = { functor := (CochainComplex.Plus.fibrantObjectEquivalence C).functor, map := ⋯ }

instance CochainComplex.Plus.instIsInducedInjectiveObjectFibrantObjectInverseImageQuasiIsoMapCochainComplexPlusιWeakEquivalencesFibrantObjectLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (fibrantObjectLocalizerMorphism C).IsInduced

instance CochainComplex.Plus.instIsRightDerivabilityStructureInjectiveObjectInverseImageQuasiIsoMapCochainComplexPlusιLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (localizerMorphism C).IsRightDerivabilityStructure

instance CochainComplex.Plus.instHasRightResolutionsArrowInjectiveObjectArrowInverseImageQuasiIsoMapCochainComplexPlusιArrowLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (localizerMorphism C).arrow.HasRightResolutions

@[reducible, inline]

abbrev HomotopyCategory.Plus.localizerMorphism (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.LocalizerMorphism (CategoryTheory.MorphismProperty.isomorphisms (Plus (CategoryTheory.InjectiveObject C))) (quasiIso C)

The localizer morphism that is given by the "inclusion functor" HomotopyCategory.Plus (InjectiveObject C) ⥤ HomotopyCategory.Plus C. The target category is equipped with the class of quasi-isomorphisms while the source category HomotopyCategory.Plus (InjectiveObject C) is equipped with the class of isomorphisms (which is exactly the same as quasi-isomorphisms).

Equations

• HomotopyCategory.Plus.localizerMorphism C = { functor := (CategoryTheory.InjectiveObject.ι C).mapHomotopyCategoryPlus, map := ⋯ }

theorem HomotopyCategory.Plus.isIso_quotient_map_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex.Plus (CategoryTheory.InjectiveObject C)} (f : K ⟶ L) : CategoryTheory.IsIso ((quotient (CategoryTheory.InjectiveObject C)).map f) ↔ CochainComplex.Plus.quasiIso C ((CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.map f)

theorem HomotopyCategory.Plus.inverseImage_quasiIso_mapCochainComplexPlus_injectiveObjectι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus = (HomologicalComplex.homotopyEquivalences (CategoryTheory.InjectiveObject C) (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι (CategoryTheory.InjectiveObject C))

instance HomotopyCategory.Plus.instIsLocalizationPlusInjectiveObjectQuotientInverseImageQuasiIsoMapCochainComplexPlusι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (quotient (CategoryTheory.InjectiveObject C)).IsLocalization ((CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus)

instance HomotopyCategory.Plus.instIsLocalizationPlusCompQuotientQuasiIsoOfQuasiIso {C : Type u_1} {H : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor (Plus C) H) [L.IsLocalization (quasiIso C)] : ((quotient C).comp L).IsLocalization (CochainComplex.Plus.quasiIso C)

The following private definitions are used to deduce that HomotopyCategory.Plus.localizerMorphism is a right derivability structure from the fact that CochainComplex.Plus.localizerMorphism is.

The strategy is to observe that the following commutative square of localizer morphisms gives a Guitart exact square:

                           CochainComplex.Plus.localizerMorphism C
CochainComplex.Plus (InjectiveObject C) ----------> CochainComplex.Plus C
     |                                                        |
 L C |                                                        | R C
     v                                                        v
HomotopyCategory.Plus (InjectiveObject C) --------> HomotopyCategory.Plus C
                           HomotopyCategory.Plus.localizerMorphism C

That the square is Guitart exact will follow from the lemma TwoSquare.GuitartExact.quotient_of_nonempty_rightHomotopy from the file Mathlib/CategoryTheory/GuitartExact/Quotient.lean.

instance HomotopyCategory.Plus.isRightDerivabilityStructure {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (localizerMorphism C).IsRightDerivabilityStructure

instance HomotopyCategory.Plus.instHasRightResolutionsArrowInjectiveObjectArrowIsomorphismsQuasiIsoArrowLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (localizerMorphism C).arrow.HasRightResolutions

instance HomotopyCategory.Plus.instEssSurjInjectiveObjectPlusCompMapHomotopyCategoryPlusιQh {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] [HasDerivedCategory C] : ((CategoryTheory.InjectiveObject.ι C).mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh).EssSurj

theorem HomotopyCategory.Plus.localizerMorphism_derives {C : Type u_1} {H : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{v_2, u_2} H] (F : CategoryTheory.Functor (Plus C) H) : (localizerMorphism C).Derives F

instance HomotopyCategory.Plus.instHasPointwiseRightDerivedFunctorQuasiIso {C : Type u_1} {H : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{v_2, u_2} H] [CategoryTheory.EnoughInjectives C] (F : CategoryTheory.Functor (Plus C) H) : F.HasPointwiseRightDerivedFunctor (quasiIso C)

Any functor from the bounded below homotopy category has a right derived functor with respect to quasi-isomorphisms.

instance HomotopyCategory.Plus.instIsIsoAppOfInjectiveXIntAsHomologicalComplexUpHomotopicObjPlus {C : Type u_1} {H : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{v_2, u_2} H] [CategoryTheory.EnoughInjectives C] (F : CategoryTheory.Functor (Plus C) H) [HasDerivedCategory C] (F' : CategoryTheory.Functor (DerivedCategory.Plus C) H) (α : F ⟶ DerivedCategory.Plus.Qh.comp F') [F'.IsRightDerivedFunctor α (quasiIso C)] (K : Plus C) [∀ (n : ℤ), CategoryTheory.Injective (K.obj.as.X n)] : CategoryTheory.IsIso (α.app K)

instance HomotopyCategory.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjPlusObjPlusQuotientOfCochainComplexPlus {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex.Plus C) (n : ℤ) [CategoryTheory.Injective (K.obj.X n)] : CategoryTheory.Injective (((quotient C).obj K).obj.as.X n)

instance HomotopyCategory.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjPlusObjPlusQuotientInjectiveObjectMapCochainComplexPlusι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex.Plus (CategoryTheory.InjectiveObject C)) (n : ℤ) : CategoryTheory.Injective (((quotient C).obj ((CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.obj K)).obj.as.X n)