Projective resolutions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
(Z : C) :
Type (max u v)
- complex : chain_complex C ℕ
- π : homological_complex.hom self.complex ((chain_complex.single₀ C).obj Z)
- projective : (∀ (n : ℕ), category_theory.projective (self.complex.X n)) . "apply_instance"
- exact₀ : category_theory.exact (self.complex.d 1 0) (self.π.f 0)
- exact : ∀ (n : ℕ), category_theory.exact (self.complex.d (n + 2) (n + 1)) (self.complex.d (n + 1) n)
- epi : category_theory.epi (self.π.f 0) . "apply_instance"
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 withprojectiveandexactinstances)projective_resolution.π Z: the chain map fromprojective_resolution Zto(single C _ 0).obj Z(all the components are equipped withepiinstances, and when the category isabelianwe will showπis a quasi-iso).
Instances for category_theory.ProjectiveResolution
- category_theory.ProjectiveResolution.has_sizeof_inst
@[class]
structure
category_theory.has_projective_resolution
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
(Z : C) :
Prop
- out : nonempty (category_theory.ProjectiveResolution Z)
An object admits a projective resolution.
@[class]
structure
category_theory.has_projective_resolutions
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C] :
Prop
- out : ∀ (Z : C), category_theory.has_projective_resolution Z
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}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Z : C}
(P : category_theory.ProjectiveResolution Z)
(n : ℕ) :
@[simp]
theorem
category_theory.ProjectiveResolution.complex_d_comp_π_f_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Z : C}
(P : category_theory.ProjectiveResolution Z) :
@[simp]
theorem
category_theory.ProjectiveResolution.complex_d_succ_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Z : C}
(P : category_theory.ProjectiveResolution Z)
(n : ℕ) :
@[protected, instance]
def
category_theory.ProjectiveResolution.f.category_theory.epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Z : C}
(P : category_theory.ProjectiveResolution Z)
(n : ℕ) :
category_theory.epi (P.π.f n)
noncomputable
def
category_theory.ProjectiveResolution.self
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
(Z : C)
[category_theory.projective Z] :
A projective object admits a trivial projective resolution: itself in degree 0.
Equations
- category_theory.ProjectiveResolution.self Z = {complex := (chain_complex.single₀ C).obj Z, π := 𝟙 ((chain_complex.single₀ C).obj Z), projective := _, exact₀ := _, exact := _, epi := _}
noncomputable
def
category_theory.ProjectiveResolution.lift_f_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z) :
Auxiliary construction for lift.
Equations
- category_theory.ProjectiveResolution.lift_f_zero f P Q = category_theory.projective.factor_thru (P.π.f 0 ≫ f) (Q.π.f 0)
noncomputable
def
category_theory.ProjectiveResolution.lift_f_one
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z) :
Auxiliary construction for lift.
Equations
- category_theory.ProjectiveResolution.lift_f_one f P Q = category_theory.exact.lift (P.complex.d 1 0 ≫ category_theory.ProjectiveResolution.lift_f_zero f P Q) (Q.complex.d 1 0) (Q.π.f 0) _ _
@[simp]
theorem
category_theory.ProjectiveResolution.lift_f_one_zero_comm
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z) :
category_theory.ProjectiveResolution.lift_f_one f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ category_theory.ProjectiveResolution.lift_f_zero f P Q
Auxiliary lemma for lift.
noncomputable
def
category_theory.ProjectiveResolution.lift_f_succ
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z)
(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) :
Auxiliary construction for lift.
@[irreducible]
noncomputable
def
category_theory.ProjectiveResolution.lift
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z) :
A morphism in C lifts to a chain map between projective resolutions.
Equations
- category_theory.ProjectiveResolution.lift f P Q = P.complex.mk_hom Q.complex (category_theory.ProjectiveResolution.lift_f_zero f P Q) (category_theory.ProjectiveResolution.lift_f_one f P Q) _ (λ (n : ℕ) (_x : Σ' (f : P.complex.X n ⟶ Q.complex.X n) (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)), f' ≫ Q.complex.d (n + 1) n = P.complex.d (n + 1) n ≫ f), category_theory.ProjectiveResolution.lift._match_1 P Q n _x)
- category_theory.ProjectiveResolution.lift._match_1 P Q n ⟨g, ⟨g', w⟩⟩ = P.lift_f_succ Q n g g' w
@[simp]
theorem
category_theory.ProjectiveResolution.lift_commutes
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z) :
category_theory.ProjectiveResolution.lift f P Q ≫ Q.π = P.π ≫ (chain_complex.single₀ C).map f
The resolution maps intertwine the lift of a morphism and that morphism.
@[simp]
theorem
category_theory.ProjectiveResolution.lift_commutes_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
(P : category_theory.ProjectiveResolution Y)
(Q : category_theory.ProjectiveResolution Z)
{X' : chain_complex C ℕ}
(f' : (chain_complex.single₀ C).obj Z ⟶ X') :
category_theory.ProjectiveResolution.lift f P Q ≫ Q.π ≫ f' = P.π ≫ (chain_complex.single₀ C).map f ≫ f'
noncomputable
def
category_theory.ProjectiveResolution.lift_homotopy_zero_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
{P : category_theory.ProjectiveResolution Y}
{Q : category_theory.ProjectiveResolution Z}
(f : P.complex ⟶ Q.complex)
(comm : f ≫ Q.π = 0) :
An auxiliary definition for lift_homotopy_zero.
Equations
- category_theory.ProjectiveResolution.lift_homotopy_zero_zero f comm = category_theory.exact.lift (f.f 0) (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}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
{P : category_theory.ProjectiveResolution Y}
{Q : category_theory.ProjectiveResolution Z}
(f : P.complex ⟶ Q.complex)
(comm : f ≫ Q.π = 0) :
An auxiliary definition for lift_homotopy_zero.
Equations
- category_theory.ProjectiveResolution.lift_homotopy_zero_one f comm = category_theory.exact.lift (f.f 1 - P.complex.d 1 0 ≫ category_theory.ProjectiveResolution.lift_homotopy_zero_zero f comm) (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}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
{P : category_theory.ProjectiveResolution Y}
{Q : category_theory.ProjectiveResolution Z}
(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)) :
An auxiliary definition for lift_homotopy_zero.
@[irreducible]
noncomputable
def
category_theory.ProjectiveResolution.lift_homotopy_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
{P : category_theory.ProjectiveResolution Y}
{Q : category_theory.ProjectiveResolution Z}
(f : P.complex ⟶ Q.complex)
(comm : f ≫ Q.π = 0) :
homotopy f 0
Any lift of the zero morphism is homotopic to zero.
Equations
- category_theory.ProjectiveResolution.lift_homotopy_zero f comm = homotopy.mk_inductive f (category_theory.ProjectiveResolution.lift_homotopy_zero_zero f comm) _ (category_theory.ProjectiveResolution.lift_homotopy_zero_one f comm) _ (λ (n : ℕ) (_x : Σ' (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)), f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1)), category_theory.ProjectiveResolution.lift_homotopy_zero._match_1 f n _x)
- category_theory.ProjectiveResolution.lift_homotopy_zero._match_1 f n ⟨g, ⟨g', w⟩⟩ = ⟨category_theory.ProjectiveResolution.lift_homotopy_zero_succ f n g g' w, _⟩
@[irreducible]
noncomputable
def
category_theory.ProjectiveResolution.lift_homotopy
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{Y Z : C}
(f : Y ⟶ Z)
{P : category_theory.ProjectiveResolution Y}
{Q : category_theory.ProjectiveResolution Z}
(g h : P.complex ⟶ Q.complex)
(g_comm : g ≫ Q.π = P.π ≫ (chain_complex.single₀ C).map f)
(h_comm : h ≫ Q.π = P.π ≫ (chain_complex.single₀ C).map f) :
homotopy g h
Two lifts of the same morphism are homotopic.
Equations
- category_theory.ProjectiveResolution.lift_homotopy f g h g_comm h_comm = homotopy.equiv_sub_zero.inv_fun (category_theory.ProjectiveResolution.lift_homotopy_zero (g - h) _)
@[irreducible]
noncomputable
def
category_theory.ProjectiveResolution.lift_id_homotopy
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
(X : C)
(P : category_theory.ProjectiveResolution X) :
homotopy (category_theory.ProjectiveResolution.lift (𝟙 X) P P) (𝟙 P.complex)
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}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(P : category_theory.ProjectiveResolution X)
(Q : category_theory.ProjectiveResolution Y)
(R : category_theory.ProjectiveResolution 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}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X : C}
(P Q : category_theory.ProjectiveResolution X) :
Any two projective resolutions are homotopy equivalent.
Equations
- P.homotopy_equiv Q = {hom := category_theory.ProjectiveResolution.lift (𝟙 X) P Q, inv := category_theory.ProjectiveResolution.lift (𝟙 X) Q P, homotopy_hom_inv_id := (category_theory.ProjectiveResolution.lift_comp_homotopy (𝟙 X) (𝟙 X) P Q P).symm.trans (_.mpr (category_theory.ProjectiveResolution.lift_id_homotopy X P)), homotopy_inv_hom_id := (category_theory.ProjectiveResolution.lift_comp_homotopy (𝟙 X) (𝟙 X) Q P Q).symm.trans (_.mpr (category_theory.ProjectiveResolution.lift_id_homotopy X Q))}
@[simp]
theorem
category_theory.ProjectiveResolution.homotopy_equiv_hom_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X : C}
(P Q : category_theory.ProjectiveResolution X) :
@[simp]
theorem
category_theory.ProjectiveResolution.homotopy_equiv_hom_π_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X : C}
(P Q : category_theory.ProjectiveResolution X)
{X' : chain_complex C ℕ}
(f' : (chain_complex.single₀ C).obj X ⟶ X') :
@[simp]
theorem
category_theory.ProjectiveResolution.homotopy_equiv_inv_π_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X : C}
(P Q : category_theory.ProjectiveResolution X)
{X' : chain_complex C ℕ}
(f' : (chain_complex.single₀ C).obj X ⟶ X') :
@[simp]
theorem
category_theory.ProjectiveResolution.homotopy_equiv_inv_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.preadditive C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X : C}
(P Q : category_theory.ProjectiveResolution X) :
@[reducible]
noncomputable
def
category_theory.projective_resolution
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
(Z : C)
[category_theory.has_projective_resolution Z] :
An arbitrarily chosen projective resolution of an object.
@[reducible]
noncomputable
def
category_theory.projective_resolution.π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
(Z : C)
[category_theory.has_projective_resolution Z] :
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]
noncomputable
def
category_theory.projective_resolution.lift
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.has_projective_resolution X]
[category_theory.has_projective_resolution Y] :
The lift of a morphism to a chain map between the arbitrarily chosen projective resolutions.
noncomputable
def
category_theory.projective_resolutions
(C : Type u)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C] :
Taking projective resolutions is functorial,
if considered with target the homotopy category
(ℕ-indexed chain complexes and chain maps up to homotopy).
Equations
- category_theory.projective_resolutions C = {obj := λ (X : C), (homotopy_category.quotient C (complex_shape.down ℕ)).obj (category_theory.projective_resolution X), map := λ (X Y : C) (f : X ⟶ Y), (homotopy_category.quotient C (complex_shape.down ℕ)).map (category_theory.projective_resolution.lift f), map_id' := _, map_comp' := _}