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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (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 : ChainComplex C ℕ

  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 ⟶ (ChainComplex.single₀ C).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

theorem CategoryTheory.ProjectiveResolution.projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : CategoryTheory.Projective (self.complex.X n)

the chain complex must be degreewise projective

theorem CategoryTheory.ProjectiveResolution.hasHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z) (i : ℕ) : HomologicalComplex.HasHomology self.complex i

the chain complex must have homology

theorem CategoryTheory.ProjectiveResolution.quasiIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z) : QuasiIso self.π

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

class CategoryTheory.HasProjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) : Prop

An object admits a projective resolution.

• out : Nonempty (CategoryTheory.ProjectiveResolution Z)

theorem CategoryTheory.HasProjectiveResolution.out {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} [self : CategoryTheory.HasProjectiveResolution Z], Nonempty (CategoryTheory.ProjectiveResolution Z)

class CategoryTheory.HasProjectiveResolutions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop

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), CategoryTheory.HasProjectiveResolution Z

theorem CategoryTheory.HasProjectiveResolutions.out {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.HasProjectiveResolutions C] (Z : C), CategoryTheory.HasProjectiveResolution Z

theorem CategoryTheory.ProjectiveResolution.complex_exactAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : HomologicalComplex.ExactAt P.complex (n + 1)

theorem CategoryTheory.ProjectiveResolution.exact_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : P.π.f (n + 1) = 0

@[simp]

theorem CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z✝) {Z : C} (h : ((ChainComplex.single₀ C).obj Z✝).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.CategoryStruct.comp (P.π.f 0) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (P.π.f 0) = 0

theorem CategoryTheory.ProjectiveResolution.complex_d_succ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : CategoryTheory.CategoryStruct.comp (P.complex.d n (n + 1)) (P.complex.d (n + 1) (n + 2)) = 0

noncomputable def CategoryTheory.ProjectiveResolution.cokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.Limits.CokernelCofork (P.complex.d 1 0)

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

Equations

• P.cokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ (P.π.f 0) ⋯

noncomputable def CategoryTheory.ProjectiveResolution.isColimitCokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.Limits.IsColimit P.cokernelCofork

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.

instance CategoryTheory.ProjectiveResolution.instEpiFNatπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ) : CategoryTheory.Epi (P.π.f n)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.self_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Projective Z] : (CategoryTheory.ProjectiveResolution.self Z).π = CategoryTheory.CategoryStruct.id ((ChainComplex.single₀ C).obj Z)

@[simp]

theorem CategoryTheory.ProjectiveResolution.self_complex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Projective Z] : (CategoryTheory.ProjectiveResolution.self Z).complex = (ChainComplex.single₀ C).obj Z

noncomputable def CategoryTheory.ProjectiveResolution.self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Projective Z] : CategoryTheory.ProjectiveResolution Z

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

Equations

• CategoryTheory.ProjectiveResolution.self Z = CategoryTheory.ProjectiveResolution.mk ((ChainComplex.single₀ C).obj Z) ⋯ (CategoryTheory.CategoryStruct.id ((ChainComplex.single₀ C).obj Z)) ⋯