K-projective cochain complexes

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

TODO (@joelriou)

• Provide an API for computing Ext-groups using a projective resolution

References

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

class CochainComplex.IsKProjective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) : Prop

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

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

@[irreducible]

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

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

Equations

• CochainComplex.IsKProjective.homotopyZero f hL = ⋯.some

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

theorem HomotopyEquiv.isKProjective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K₁ K₂ : CochainComplex C ℤ} (e : HomotopyEquiv K₁ K₂) [K₁.IsKProjective] : K₂.IsKProjective

theorem CochainComplex.isKProjective_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K₁ K₂ : CochainComplex C ℤ} (e : K₁ ≅ K₂) [K₁.IsKProjective] : K₂.IsKProjective

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

theorem CochainComplex.isKProjective_iff_leftOrthogonal {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) : K.IsKProjective ↔ (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)

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

instance CochainComplex.instIsKProjectiveObjIntShiftFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) [hK : K.IsKProjective] (n : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).IsKProjective

theorem CochainComplex.isKProjective_shift_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).IsKProjective ↔ K.IsKProjective

theorem CochainComplex.isKProjective_of_op {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} (hK : ((opEquivalence C).functor.obj (Opposite.op K)).IsKInjective) : K.IsKProjective

theorem CochainComplex.isKProjective_of_projective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), CategoryTheory.Projective (K.X n)] : K.IsKProjective