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)

• Provide an API for computing Ext-groups using an injective resolution

References

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

class CochainComplex.IsKInjective {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[irreducible]

noncomputable def CochainComplex.IsKInjective.homotopyZero {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (hK : HomologicalComplex.Acyclic K) [L.IsKInjective] : Homotopy f 0

A choice of homotopy to zero for a morphism from an acyclic cochain complex to a K-injective cochain complex.

Equations

• CochainComplex.IsKInjective.homotopyZero f hK = ⋯.some

theorem CochainComplex.IsKInjective.homotopyZero_def {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (hK : HomologicalComplex.Acyclic K) [L.IsKInjective] : homotopyZero f hK = ⋯.some

theorem HomotopyEquiv.isKInjective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {L₁ L₂ : CochainComplex C ℤ} (e : HomotopyEquiv L₁ L₂) [L₁.IsKInjective] : L₂.IsKInjective

theorem CochainComplex.isKInjective_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {L₁ L₂ : CochainComplex C ℤ} (e : L₁ ≅ L₂) [L₁.IsKInjective] : L₂.IsKInjective

theorem CochainComplex.isKInjective_iff_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {L₁ L₂ : CochainComplex C ℤ} (e : L₁ ≅ L₂) : L₁.IsKInjective ↔ L₂.IsKInjective

theorem CochainComplex.isKInjective_iff_rightOrthogonal {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) : L.IsKInjective ↔ (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)

theorem CochainComplex.IsKInjective.rightOrthogonal {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) [L.IsKInjective] : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)

instance CochainComplex.instIsKInjectiveObjIntShiftFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) [hL : L.IsKInjective] (n : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L).IsKInjective

theorem CochainComplex.isKInjective_shift_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L).IsKInjective ↔ L.IsKInjective

theorem CochainComplex.isKInjective_of_injective_aux {C : Type u_1} [CategoryTheory.Category.{v_1, 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.{v_1, u_1} C] [CategoryTheory.Abelian C] (L : CochainComplex C ℤ) (d : ℤ) [L.IsStrictlyGE d] [∀ (n : ℤ), CategoryTheory.Injective (L.X n)] : L.IsKInjective