Abelian categories with enough projectives have projective resolutions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
When C is abelian projective.d f and f are exact.
Hence, starting from an epimorphism P ⟶ X, where P is projective,
we can apply projective.d repeatedly to obtain a projective resolution of X.
theorem
category_theory.exact_d_f
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.enough_projectives C]
{X Y : C}
(f : X ⟶ Y) :
When C is abelian, projective.d f and f are exact.
noncomputable
def
category_theory.preserves_finite_colimits_preadditive_coyoneda_obj_of_projective
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(P : C)
[hP : category_theory.projective P] :
The preadditive Co-Yoneda functor on P preserves colimits if P is projective.
Equations
- category_theory.preserves_finite_colimits_preadditive_coyoneda_obj_of_projective P = let _inst : (category_theory.preadditive_coyoneda_obj (opposite.op P)).preserves_epimorphisms := _ in (category_theory.preadditive_coyoneda_obj (opposite.op P)).preserves_finite_colimits_of_preserves_epis_and_kernels
theorem
category_theory.projective_of_preserves_finite_colimits_preadditive_coyoneda_obj
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(P : C)
[hP : category_theory.limits.preserves_finite_colimits (category_theory.preadditive_coyoneda_obj (opposite.op P))] :
An object is projective if its preadditive Co-Yoneda functor preserves finite colimits.
Our goal is to define ProjectiveResolution.of Z : ProjectiveResolution Z.
The 0-th object in this resolution will just be projective.over Z,
i.e. an arbitrarily chosen projective object with a map to Z.
After that, we build the n+1-st object as projective.syzygies
applied to the previously constructed morphism,
and the map to the n-th object as projective.d.
@[simp]
theorem
category_theory.ProjectiveResolution.of_complex_d
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.enough_projectives C]
(Z : C)
(i j : ℕ) :
(category_theory.ProjectiveResolution.of_complex Z).d i j = dite (i = j + 1) (λ (h : i = j + 1), category_theory.eq_to_hom _ ≫ (chain_complex.mk_aux (category_theory.projective.over Z) (category_theory.projective.syzygies (category_theory.projective.π Z)) (category_theory.ProjectiveResolution.of_complex._match_1 ⟨category_theory.projective.over Z, ⟨category_theory.projective.syzygies (category_theory.projective.π Z) _, category_theory.projective.d (category_theory.projective.π Z) _⟩⟩).fst (category_theory.projective.d (category_theory.projective.π Z)) (category_theory.ProjectiveResolution.of_complex._match_1 ⟨category_theory.projective.over Z, ⟨category_theory.projective.syzygies (category_theory.projective.π Z) _, category_theory.projective.d (category_theory.projective.π Z) _⟩⟩).snd.fst _ (λ (t : Σ' (X₀ X₁ X₂ : C) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), category_theory.ProjectiveResolution.of_complex._match_1 ⟨t.snd.fst, ⟨t.snd.snd.fst, t.snd.snd.snd.snd.fst⟩⟩) j).d₀) (λ (h : ¬i = j + 1), 0)
noncomputable
def
category_theory.ProjectiveResolution.of_complex
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.enough_projectives C]
(Z : C) :
Auxiliary definition for ProjectiveResolution.of.
Equations
- category_theory.ProjectiveResolution.of_complex Z = chain_complex.mk' (category_theory.projective.over Z) (category_theory.projective.syzygies (category_theory.projective.π Z)) (category_theory.projective.d (category_theory.projective.π Z)) (λ (_x : Σ (X₀ X₁ : C), X₁ ⟶ X₀), category_theory.ProjectiveResolution.of_complex._match_1 _x)
- category_theory.ProjectiveResolution.of_complex._match_1 ⟨X, ⟨Y, f⟩⟩ = ⟨category_theory.projective.syzygies f _, ⟨category_theory.projective.d f _, _⟩⟩
@[simp]
theorem
category_theory.ProjectiveResolution.of_complex_X
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.enough_projectives C]
(Z : C)
(n : ℕ) :
(category_theory.ProjectiveResolution.of_complex Z).X n = (chain_complex.mk_aux (category_theory.projective.over Z) (category_theory.projective.syzygies (category_theory.projective.π Z)) (category_theory.ProjectiveResolution.of_complex._match_1 ⟨category_theory.projective.over Z, ⟨category_theory.projective.syzygies (category_theory.projective.π Z) _, category_theory.projective.d (category_theory.projective.π Z) _⟩⟩).fst (category_theory.projective.d (category_theory.projective.π Z)) (category_theory.ProjectiveResolution.of_complex._match_1 ⟨category_theory.projective.over Z, ⟨category_theory.projective.syzygies (category_theory.projective.π Z) _, category_theory.projective.d (category_theory.projective.π Z) _⟩⟩).snd.fst _ (λ (t : Σ' (X₀ X₁ X₂ : C) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), category_theory.ProjectiveResolution.of_complex._match_1 ⟨t.snd.fst, ⟨t.snd.snd.fst, t.snd.snd.snd.snd.fst⟩⟩) n).X₀
@[irreducible]
noncomputable
def
category_theory.ProjectiveResolution.of
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.enough_projectives C]
(Z : C) :
In any abelian category with enough projectives,
ProjectiveResolution.of Z constructs a projective resolution of the object Z.
Equations
- category_theory.ProjectiveResolution.of Z = {complex := category_theory.ProjectiveResolution.of_complex Z, π := (category_theory.ProjectiveResolution.of_complex Z).mk_hom ((chain_complex.single₀ C).obj Z) (category_theory.projective.π Z) 0 _ (λ (n : ℕ) (_x : Σ' (f : (category_theory.ProjectiveResolution.of_complex Z).X n ⟶ ((chain_complex.single₀ C).obj Z).X n) (f' : (category_theory.ProjectiveResolution.of_complex Z).X (n + 1) ⟶ ((chain_complex.single₀ C).obj Z).X (n + 1)), f' ≫ ((chain_complex.single₀ C).obj Z).d (n + 1) n = (category_theory.ProjectiveResolution.of_complex Z).d (n + 1) n ≫ f), ⟨0, _⟩), projective := _, exact₀ := _, exact := _, epi := _}
@[protected, instance]
@[protected, instance]
def
homological_complex.hom.to_single₀_ProjectiveResolution
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X : chain_complex C ℕ}
{Y : C}
(f : X ⟶ (chain_complex.single₀ C).obj Y)
[quasi_iso f]
(H : ∀ (n : ℕ), category_theory.projective (X.X n)) :
If X is a chain complex of projective objects and we have a quasi-isomorphism f : X ⟶ Y[0],
then X is a projective resolution of Y.
Equations
- homological_complex.hom.to_single₀_ProjectiveResolution f H = {complex := X, π := f, projective := H, exact₀ := _, exact := _, epi := _}