Injective resolutions as cochain complexes indexed by the integers

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

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

If R : InjectiveResolution X, this is the cochain complex indexed by ℤ obtained by extending by zero the R.cocomplex.

Equations

• R.cochainComplex = HomologicalComplex.extend R.cocomplex ComplexShape.embeddingUpNat

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

If R : InjectiveResolution X, then R.cochainComplex.X n (with n : ℕ) is isomorphic to R.cocomplex.X k (with k : ℕ) when k = n.

Equations

• R.cochainComplexXIso n k h = HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat h

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

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

instance CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] {X : C} (R : InjectiveResolution X) : R.cochainComplex.IsStrictlyGE 0

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

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

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

Equations

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

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

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