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)
:
If R : ProjectiveResolution X, this is the cochain complex indexed by ℤ
obtained by extending by zero the chain complex R.complex indexed by ℕ.
Instances For
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)
:
If R : ProjectiveResolution X, then R.cochainComplex.X n (with n : ℕ)
is isomorphic to R.complex.X k (with k : ℕ) when k = n.
Equations
Instances For
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)
:
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)
:
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.
Instances For
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)
:
instance
CategoryTheory.ProjectiveResolution.instIsGECochainComplexOfNatInt
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
(R : ProjectiveResolution X)
:
R.cochainComplex.IsGE 0
noncomputable def
CategoryTheory.ProjectiveResolution.Hom.hom'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : ProjectiveResolution X}
{X' : C}
{R' : ProjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
:
The morphism on cochain complexes indexed by ℤ that is induced by
a (heterogeneous) morphism of projective resolutions.
Equations
Instances For
theorem
CategoryTheory.ProjectiveResolution.Hom.hom'_f
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : ProjectiveResolution X}
{X' : C}
{R' : ProjectiveResolution 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.ProjectiveResolution.Hom.hom'_f_assoc
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : ProjectiveResolution X}
{X' : C}
{R' : ProjectiveResolution 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.ProjectiveResolution.Hom.hom'_comp_π'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : ProjectiveResolution X}
{X' : C}
{R' : ProjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
:
CategoryStruct.comp φ.hom' R'.π' = CategoryStruct.comp R.π' ((CochainComplex.singleFunctor C 0).map f)
@[simp]
theorem
CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
{R : ProjectiveResolution X}
{X' : C}
{R' : ProjectiveResolution X'}
{f : X ⟶ X'}
(φ : R.Hom R' f)
{Z : CochainComplex C ℤ}
(h : (CochainComplex.singleFunctor C 0).obj X' ⟶ Z)
:
CategoryStruct.comp φ.hom' (CategoryStruct.comp R'.π' h) = CategoryStruct.comp R.π' (CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f) h)