Theorems · Theorem · category theory

DerivedCategory.Plus.exists_injective_nonempty_iso

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (K : DerivedCategory.Plus C) (n : ℤ) [K.IsGE n],
  ∃ L,
    ∃ (_ : L.obj.IsStrictlyGE n),
      Nonempty (DerivedCategory.Plus.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.

Defined in

Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Cited by

0 results in Mathlib

Foundations

Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategoryCategoryTheory.EnoughInjectivesDerivedCategory.Plus.IsGE