Projective resolutions as cochain complexes indexed by the integers

Given a projective resolution R of an object X in an abelian category C, we define R.cochainComplex : CochainComplex C ℤ, which is the extension of R.complex : ChainComplex C ℕ, and the quasi-isomorphism R.π' : R.cochainComplex ⟶ (CochainComplex.singleFunctor C 0).obj X.

noncomputable def CategoryTheory.ProjectiveResolution.cochainComplex {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) : CochainComplex C ℤ

If R : ProjectiveResolution X, this is the cochain complex indexed by ℤ obtained by extending by zero the chain complex R.complex indexed by ℕ.

Equations

• R.cochainComplex = HomologicalComplex.extend R.complex ComplexShape.embeddingDownNat

noncomputable def CategoryTheory.ProjectiveResolution.cochainComplexXIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) (n : ℤ) (k : ℕ) (h : -↑k = n := by lia) : R.cochainComplex.X n ≅ R.complex.X k

If R : ProjectiveResolution X, then R.chainComplex.X n (with n : ℕ) is isomorphic to R.complex.X k (with k : ℕ) when k = n.

Equations

• R.cochainComplexXIso n k h = HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat h

theorem CategoryTheory.ProjectiveResolution.cochainComplex_d {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) (n₁ n₂ : ℤ) (k₁ k₂ : ℕ) (h₁ : -↑k₁ = n₁ := by lia) (h₂ : -↑k₂ = n₂ := by lia) : R.cochainComplex.d n₁ n₂ = CategoryStruct.comp (R.cochainComplexXIso n₁ k₁ ⋯).hom (CategoryStruct.comp (R.complex.d k₁ k₂) (R.cochainComplexXIso n₂ k₂ ⋯).inv)

theorem CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) (n₁ n₂ : ℤ) (k₁ k₂ : ℕ) (h₁ : -↑k₁ = n₁ := by lia) (h₂ : -↑k₂ = n₂ := by lia) {Z : C} (h : R.cochainComplex.X n₂ ⟶ Z) : CategoryStruct.comp (R.cochainComplex.d n₁ n₂) h = CategoryStruct.comp (R.cochainComplexXIso n₁ k₁ ⋯).hom (CategoryStruct.comp (R.complex.d k₁ k₂) (CategoryStruct.comp (R.cochainComplexXIso n₂ k₂ ⋯).inv h))

instance CategoryTheory.ProjectiveResolution.instIsStrictlyLECochainComplexOfNatInt {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) : R.cochainComplex.IsStrictlyLE 0

instance CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) (n : ℤ) : Projective (R.cochainComplex.X n)

noncomputable def CategoryTheory.ProjectiveResolution.π' {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) : R.cochainComplex ⟶ (CochainComplex.singleFunctor C 0).obj X

The quasi-isomorphism R.cochainComplex ⟶ (CochainComplex.singleFunctor C 0).obj X in CochainComplex C ℤ when R is a projective resolution of X.

Equations

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

theorem CategoryTheory.ProjectiveResolution.π'_f_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) : R.π'.f 0 = CategoryStruct.comp (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom (CategoryStruct.comp (R.π.f 0) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv)

theorem CategoryTheory.ProjectiveResolution.π'_f_zero_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : ProjectiveResolution X) {Z : C} (h : ((CochainComplex.singleFunctor C 0).obj X).X 0 ⟶ Z) : CategoryStruct.comp (R.π'.f 0) h = CategoryStruct.comp (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom (CategoryStruct.comp (R.π.f 0) (CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv h))

instance CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ' {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (R : ProjectiveResolution X) : QuasiIso R.π'