K-injective cochain complexes

We define the notion of K-injective cochain complex in an abelian category, and show that bounded below complexes of injective objects are K-injective.

TODO (@joelriou)

• Show that a cochain complex is K-injective iff its image in the homotopy category belongs to the right orthogonal of the triangulated subcategory of acyclic complexes
• Deduce that we can compute morphisms to a K-injective complex in the derived category as homotopy classes of morphisms
• Provide an API for computing Ext-groups using an injective resolution
• Dualize everything

References

• [N. Spaltenstein, Resolutions of unbounded complexes][spaltenstein1998]

class CochainComplex.IsKInjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) : Prop

A cochain complex L is K-injective if any morphism K ⟶ L with K acyclic is homotopic to zero.

• nonempty_homotopy_zero {K : CochainComplex C ℤ} (f : K ⟶ L) : HomologicalComplex.Acyclic K → Nonempty (Homotopy f 0)

theorem CochainComplex.isKInjective_of_injective_aux {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (α : HomComplex.Cochain K L (-1)) (n m : ℤ) (hnm : n + 1 = m) (hK : HomologicalComplex.ExactAt K m) [CategoryTheory.Injective (L.X m)] (hα : (HomComplex.δ (-1) 0 α).EqUpTo (HomComplex.Cochain.ofHom f) n) : ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), (HomComplex.δ (-1) 0 (α + HomComplex.Cochain.single h (-1))).EqUpTo (HomComplex.Cochain.ofHom f) m

theorem CochainComplex.isKInjective_of_injective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) (d : ℤ) [L.IsStrictlyGE d] [∀ (n : ℤ), CategoryTheory.Injective (L.X n)] : L.IsKInjective