# Projective resolutions #

A projective resolution P : ProjectiveResolution Z of an object Z : C consists of an -indexed chain complex P.complex of projective objects, along with a quasi-isomorphism P.π from C to the chain complex consisting just of Z in degree zero.

structure CategoryTheory.ProjectiveResolution {C : Type u} (Z : C) :
Type (max u v)

A ProjectiveResolution Z consists of a bundled -indexed chain complex of projective objects, along with a quasi-isomorphism to the complex consisting of just Z supported in degree 0.

• complex :

the chain complex involved in the resolution

• projective : ∀ (n : ), CategoryTheory.Projective (self.complex.X n)

the chain complex must be degreewise projective

• hasHomology : ∀ (i : ), HomologicalComplex.HasHomology self.complex i

the chain complex must have homology

• π : self.complex .obj Z

the morphism to the single chain complex with Z in degree 0

• quasiIso : QuasiIso self

the morphism to the single chain complex with Z in degree 0 is a quasi-isomorphism

Instances For
theorem CategoryTheory.ProjectiveResolution.projective {C : Type u} {Z : C} (self : ) (n : ) :
CategoryTheory.Projective (self.complex.X n)

the chain complex must be degreewise projective

theorem CategoryTheory.ProjectiveResolution.hasHomology {C : Type u} {Z : C} (self : ) (i : ) :

the chain complex must have homology

theorem CategoryTheory.ProjectiveResolution.quasiIso {C : Type u} {Z : C} (self : ) :
QuasiIso self

the morphism to the single chain complex with Z in degree 0 is a quasi-isomorphism

An object admits a projective resolution.

Instances

You will rarely use this typeclass directly: it is implied by the combination [EnoughProjectives C] and [Abelian C]. By itself it's enough to set up the basic theory of derived functors.

• out : ∀ (Z : C),
Instances
theorem CategoryTheory.ProjectiveResolution.exact_succ {C : Type u} {Z : C} (n : ) :
(CategoryTheory.ShortComplex.mk (P.complex.d (n + 2) (n + 1)) (P.complex.d (n + 1) n) ).Exact
@[simp]
theorem CategoryTheory.ProjectiveResolution.π_f_succ {C : Type u} {Z : C} (n : ) :
P.f (n + 1) = 0
@[simp]
theorem CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc {C : Type u} {Z : C} {Z : C} (h : (.obj Z✝).X 0 Z) :
theorem CategoryTheory.ProjectiveResolution.complex_d_succ_comp {C : Type u} {Z : C} (n : ) :
CategoryTheory.CategoryStruct.comp (P.complex.d n (n + 1)) (P.complex.d (n + 1) (n + 2)) = 0

The (limit) cokernel cofork given by the composition P.complex.X 1 ⟶ P.complex.X 0 ⟶ Z when P : ProjectiveResolution Z.

Equations
Instances For

Z is the cokernel of P.complex.X 1 ⟶ P.complex.X 0 when P : ProjectiveResolution Z.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
@[simp]
theorem CategoryTheory.ProjectiveResolution.self_complex {C : Type u} (Z : C) :
.complex = .obj Z
@[simp]
noncomputable def CategoryTheory.ProjectiveResolution.self {C : Type u} (Z : C) :

A projective object admits a trivial projective resolution: itself in degree 0.

Equations
Instances For