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)
:
If R : InjectiveResolution X, this is the cochain complex indexed by ℤ
obtained by extending by zero the cochain complex R.cocomplex indexed by ℕ.
Instances For
instance
CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[Preadditive C]
{X : C}
(R : InjectiveResolution X)
:
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)
:
If R : InjectiveResolution X, then R.cochainComplex.X n (with n : ℕ)
is isomorphic to R.cocomplex.X k (with k : ℕ) when k = n.
Equations
Instances For
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_1
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[Preadditive C]
{X : C}
(R : InjectiveResolution X)
:
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)
:
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.
Instances For
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 ι'_f_zero._proof_1).inv)
theorem
CategoryTheory.InjectiveResolution.ι'_f_zero_assoc
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
[Preadditive C]
{X : C}
(R : InjectiveResolution X)
{Z : C}
(h : R.cochainComplex.X 0 ⟶ Z)
:
CategoryStruct.comp (R.ι'.f 0) h = CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom
(CategoryStruct.comp (R.ι.f 0) (CategoryStruct.comp (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv h))
instance
CategoryTheory.InjectiveResolution.instQuasiIsoIntι'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
(R : InjectiveResolution X)
:
instance
CategoryTheory.InjectiveResolution.instIsLECochainComplexOfNatInt
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
(R : InjectiveResolution X)
:
R.cochainComplex.IsLE 0
noncomputable def
CategoryTheory.InjectiveResolution.Hom.hom'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : InjectiveResolution X}
{X' : C}
{R' : InjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
:
The morphism on cochain complexes indexed by ℤ that is induced by
an (heterogeneous) morphism of injective resolutions.
Equations
Instances For
theorem
CategoryTheory.InjectiveResolution.Hom.hom'_f
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : InjectiveResolution X}
{X' : C}
{R' : InjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
(n : ℤ)
(m : ℕ)
(h : ↑m = n)
:
φ.hom'.f n = CategoryStruct.comp (R.cochainComplexXIso n m h).hom
(CategoryStruct.comp (φ.hom.f m) (R'.cochainComplexXIso n m h).inv)
theorem
CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : InjectiveResolution X}
{X' : C}
{R' : InjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
(n : ℤ)
(m : ℕ)
(h : ↑m = n)
{Z : C}
(h✝ : R'.cochainComplex.X n ⟶ Z)
:
CategoryStruct.comp (φ.hom'.f n) h✝ = CategoryStruct.comp (R.cochainComplexXIso n m h).hom
(CategoryStruct.comp (φ.hom.f m) (CategoryStruct.comp (R'.cochainComplexXIso n m h).inv h✝))
@[simp]
theorem
CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : InjectiveResolution X}
{X' : C}
{R' : InjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
:
CategoryStruct.comp R.ι' φ.hom' = CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f) R'.ι'
@[simp]
theorem
CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : InjectiveResolution X}
{X' : C}
{R' : InjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
{Z : CochainComplex C ℤ}
(h : R'.cochainComplex ⟶ Z)
:
CategoryStruct.comp R.ι' (CategoryStruct.comp φ.hom' h) = CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f) (CategoryStruct.comp R'.ι' h)