Projective resolutions #

A projective resolution P : ProjectiveResolution Z of an object Z : C consists of a ℕ-indexed chain complex P.complex of projective objects, along with a chain map P.π from C to the chain complex consisting just of Z in degree zero, so that the augmented chain complex is exact.

When C is abelian, this exactness condition is equivalent to π being a quasi-isomorphism. It turns out that this formulation allows us to set up the basic theory of derived functors without even assuming C is abelian.

(Typically, however, to show has_projective_resolutions C one will assume enough_projectives C and abelian C. This construction appears in category_theory.abelian.projectives.)

We show that given P : ProjectiveResolution X and Q : ProjectiveResolution Y, any morphism X ⟶ Y admits a lift to a chain map P.complex ⟶ Q.complex. (It is a lift in the sense that the projection maps P.π and Q.π intertwine the lift and the original morphism.)

Moreover, we show that any two such lifts are homotopic.

As a consequence, if every object admits a projective resolution, we can construct a functor projective_resolutions C : C ⥤ homotopy_category C.

@[nolint]
structure category_theory.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.

(We don't actually ask here that the chain map is a quasi-iso, just exactness everywhere: that π is a quasi-iso is a lemma when the category is abelian. Should we just ask for it here?)

Except in situations where you want to provide a particular projective resolution (for example to compute a derived functor), you will not typically need to use this bundled object, and will instead use

• projective_resolution Z: the ℕ-indexed chain complex (equipped with projective and exact instances)
• projective_resolution.π Z: the chain map from projective_resolution Z to (single C _ 0).obj Z (all the components are equipped with epi instances, and when the category is abelian we will show π is a quasi-iso).
Instances for category_theory.ProjectiveResolution
• category_theory.ProjectiveResolution.has_sizeof_inst
@[class]
• out :

An object admits a projective resolution.

Instances of this typeclass
@[class]
• out : ∀ (Z : C),

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

Instances of this typeclass
@[simp]
theorem category_theory.ProjectiveResolution.π_f_succ {C : Type u} {Z : C} (n : ) :
P.π.f (n + 1) = 0
@[simp]
theorem category_theory.ProjectiveResolution.complex_d_comp_π_f_zero {C : Type u} {Z : C}  :
P.complex.d 1 0 P.π.f 0 = 0
@[simp]
theorem category_theory.ProjectiveResolution.complex_d_succ_comp {C : Type u} {Z : C} (n : ) :
P.complex.d (n + 2) (n + 1) P.complex.d (n + 1) n = 0
@[protected, instance]

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

Equations
noncomputable def category_theory.ProjectiveResolution.lift_f_zero {C : Type u} {Y Z : C} (f : Y Z)  :

Auxiliary construction for lift.

Equations
noncomputable def category_theory.ProjectiveResolution.lift_f_one {C : Type u} {Y Z : C} (f : Y Z)  :

Auxiliary construction for lift.

Equations
@[simp]
theorem category_theory.ProjectiveResolution.lift_f_one_zero_comm {C : Type u} {Y Z : C} (f : Y Z)  :
=

Auxiliary lemma for lift.

noncomputable def category_theory.ProjectiveResolution.lift_f_succ {C : Type u} {Y Z : C} (n : ) (g : P.complex.X n Q.complex.X n) (g' : P.complex.X (n + 1) Q.complex.X (n + 1)) (w : g' Q.complex.d (n + 1) n = P.complex.d (n + 1) n g) :
Σ' (g'' : P.complex.X (n + 2) Q.complex.X (n + 2)), g'' Q.complex.d (n + 2) (n + 1) = P.complex.d (n + 2) (n + 1) g'

Auxiliary construction for lift.

Equations
@[irreducible]
noncomputable def category_theory.ProjectiveResolution.lift {C : Type u} {Y Z : C} (f : Y Z)  :

A morphism in C lifts to a chain map between projective resolutions.

Equations
@[simp]
theorem category_theory.ProjectiveResolution.lift_commutes {C : Type u} {Y Z : C} (f : Y Z)  :
= P.π f

The resolution maps intertwine the lift of a morphism and that morphism.

@[simp]
theorem category_theory.ProjectiveResolution.lift_commutes_assoc {C : Type u} {Y Z : C} (f : Y Z) {X' : } (f' : Z X') :
Q.π f' = P.π f f'
noncomputable def category_theory.ProjectiveResolution.lift_homotopy_zero_zero {C : Type u} {Y Z : C} (f : P.complex Q.complex) (comm : f Q.π = 0) :

An auxiliary definition for lift_homotopy_zero.

Equations
• = (Q.complex.d 1 0) (Q.π.f 0) category_theory.ProjectiveResolution.lift_homotopy_zero_zero._proof_2 _
noncomputable def category_theory.ProjectiveResolution.lift_homotopy_zero_one {C : Type u} {Y Z : C} (f : P.complex Q.complex) (comm : f Q.π = 0) :

An auxiliary definition for lift_homotopy_zero.

Equations
• = (Q.complex.d 2 1) (Q.complex.d 1 0) category_theory.ProjectiveResolution.lift_homotopy_zero_one._proof_2 _
noncomputable def category_theory.ProjectiveResolution.lift_homotopy_zero_succ {C : Type u} {Y Z : C} (f : P.complex Q.complex) (n : ) (g : P.complex.X n Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) Q.complex.X (n + 2)) (w : f.f (n + 1) = P.complex.d (n + 1) n g + g' Q.complex.d (n + 2) (n + 1)) :
P.complex.X (n + 2) Q.complex.X (n + 3)

An auxiliary definition for lift_homotopy_zero.

Equations
@[irreducible]
noncomputable def category_theory.ProjectiveResolution.lift_homotopy_zero {C : Type u} {Y Z : C} (f : P.complex Q.complex) (comm : f Q.π = 0) :
0

Any lift of the zero morphism is homotopic to zero.

Equations
@[irreducible]
noncomputable def category_theory.ProjectiveResolution.lift_homotopy {C : Type u} {Y Z : C} (f : Y Z) (g h : P.complex Q.complex) (g_comm : g Q.π = P.π f) (h_comm : h Q.π = P.π f) :
h

Two lifts of the same morphism are homotopic.

Equations
@[irreducible]
noncomputable def category_theory.ProjectiveResolution.lift_id_homotopy {C : Type u} (X : C)  :

The lift of the identity morphism is homotopic to the identity chain map.

Equations
@[irreducible]
noncomputable def category_theory.ProjectiveResolution.lift_comp_homotopy {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

The lift of a composition is homotopic to the composition of the lifts.

Equations
noncomputable def category_theory.ProjectiveResolution.homotopy_equiv {C : Type u} {X : C}  :

Any two projective resolutions are homotopy equivalent.

Equations
@[simp]
@[simp]
theorem category_theory.ProjectiveResolution.homotopy_equiv_hom_π_assoc {C : Type u} {X : C} {X' : } (f' : X X') :
(P.homotopy_equiv Q).hom Q.π f' = P.π f'
@[simp]
theorem category_theory.ProjectiveResolution.homotopy_equiv_inv_π_assoc {C : Type u} {X : C} {X' : } (f' : X X') :
(P.homotopy_equiv Q).inv P.π f' = Q.π f'
@[simp]
@[reducible]

An arbitrarily chosen projective resolution of an object.

@[reducible]

The chain map from the arbitrarily chosen projective resolution projective_resolution Z back to the chain complex consisting of Z supported in degree 0.

@[reducible]

The lift of a morphism to a chain map between the arbitrarily chosen projective resolutions.

Taking projective resolutions is functorial, if considered with target the homotopy category (ℕ-indexed chain complexes and chain maps up to homotopy).

Equations