Abelian categories with enough projectives have projective resolutions

Main results

When the underlying category is abelian:

• CategoryTheory.ProjectiveResolution.lift: Given P : ProjectiveResolution X and Q : ProjectiveResolution Y, any morphism X ⟶ Y admits a lifting to a chain map P.complex ⟶ Q.complex. It is a lifting in the sense that P.ι intertwines the lift and the original morphism, see CategoryTheory.ProjectiveResolution.lift_commutes.

• CategoryTheory.ProjectiveResolution.liftHomotopy: Any two such descents are homotopic.

• CategoryTheory.ProjectiveResolution.homotopyEquiv: Any two projective resolutions of the same object are homotopy equivalent.

• CategoryTheory.projectiveResolutions: If every object admits a projective resolution, we can construct a functor projectiveResolutions C : C ⥤ HomotopyCategory C (ComplexShape.down ℕ).

• CategoryTheory.exact_d_f: Projective.d f and f are exact.

• CategoryTheory.ProjectiveResolution.of: Hence, starting from an epimorphism P ⟶ X, where P is projective, we can apply Projective.d repeatedly to obtain a projective resolution of X.

noncomputable def CategoryTheory.ProjectiveResolution.liftFZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : P.complex.X 0 ⟶ Q.complex.X 0

Auxiliary construction for lift.

Equations

• CategoryTheory.ProjectiveResolution.liftFZero f P Q = CategoryTheory.Projective.factorThru (CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (Q.π.f 0)

theorem CategoryTheory.ProjectiveResolution.exact₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) : (CategoryTheory.ShortComplex.mk (P.complex.d 1 0) (P.π.f 0) ⋯).Exact

noncomputable def CategoryTheory.ProjectiveResolution.liftFOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : P.complex.X 1 ⟶ Q.complex.X 1

Auxiliary construction for lift.

Equations

• CategoryTheory.ProjectiveResolution.liftFOne f P Q = ⋯.liftFromProjective (CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftFZero f P Q)) ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftFOne_zero_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftFOne f P Q) (Q.complex.d 1 0) = CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftFZero f P Q)

noncomputable def CategoryTheory.ProjectiveResolution.liftFSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X n) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)) (w : CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g) : (g'' : P.complex.X (n + 2) ⟶ Q.complex.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp g'' (Q.complex.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'

Auxiliary construction for lift.

Equations

• P.liftFSucc Q n g g' w = ⟨⋯.liftFromProjective (CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g') ⋯, ⋯⟩

noncomputable def CategoryTheory.ProjectiveResolution.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : P.complex ⟶ Q.complex

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z✝) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z✝) {Z : ChainComplex C ℕ} (h : (ChainComplex.single₀ C).obj Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) (CategoryTheory.CategoryStruct.comp Q.π h) = CategoryTheory.CategoryStruct.comp P.π (CategoryTheory.CategoryStruct.comp ((ChainComplex.single₀ C).map f) h)

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)

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

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z✝) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z✝) {Z : C} (h : ((ChainComplex.single₀ C).obj Z✝).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.ProjectiveResolution.lift f P Q).f 0) (CategoryTheory.CategoryStruct.comp (Q.π.f 0) h) = CategoryTheory.CategoryStruct.comp (P.π.f 0) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.ProjectiveResolution.lift f P Q).f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : P.complex.X 0 ⟶ Q.complex.X 1

An auxiliary definition for liftHomotopyZero.

Equations

• CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm = ⋯.liftFromProjective (f.f 0) ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z✝} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) {Z : C} (h : Q.complex.X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm) (CategoryTheory.CategoryStruct.comp (Q.complex.d 1 0) h) = CategoryTheory.CategoryStruct.comp (f.f 0) h

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm) (Q.complex.d 1 0) = f.f 0

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : P.complex.X 1 ⟶ Q.complex.X 2

An auxiliary definition for liftHomotopyZero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z✝} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) {Z : C} (h : Q.complex.X 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f comm) (CategoryTheory.CategoryStruct.comp (Q.complex.d 2 1) h) = CategoryTheory.CategoryStruct.comp (f.f 1 - CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm)) h

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f comm) (Q.complex.d 2 1) = f.f 1 - CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm)

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.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) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) : P.complex.X (n + 2) ⟶ Q.complex.X (n + 3)

An auxiliary definition for liftHomotopyZero.

Equations

• CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w = ⋯.liftFromProjective (f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g') ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.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) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) {Z : C} (h : Q.complex.X (n + 2) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w) (CategoryTheory.CategoryStruct.comp (Q.complex.d (n + 3) (n + 2)) h) = CategoryTheory.CategoryStruct.comp (f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g') h

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.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) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w) (Q.complex.d (n + 3) (n + 2)) = f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : Homotopy f 0

Any lift of the zero morphism is homotopic to zero.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (g : P.complex ⟶ Q.complex) (h : P.complex ⟶ Q.complex) (g_comm : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) (h_comm : CategoryTheory.CategoryStruct.comp h Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) : Homotopy g h

Two lifts of the same morphism are homotopic.

Equations

• CategoryTheory.ProjectiveResolution.liftHomotopy f g h g_comm h_comm = Homotopy.equivSubZero.invFun (CategoryTheory.ProjectiveResolution.liftHomotopyZero (g - h) ⋯)

noncomputable def CategoryTheory.ProjectiveResolution.liftIdHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) (P : CategoryTheory.ProjectiveResolution X) : Homotopy (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id X) P P) (CategoryTheory.CategoryStruct.id P.complex)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ProjectiveResolution.liftCompHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (R : CategoryTheory.ProjectiveResolution Z) : Homotopy (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.comp f g) P R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) (CategoryTheory.ProjectiveResolution.lift g Q R))

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ProjectiveResolution.homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) : HomotopyEquiv P.complex Q.complex

Any two projective resolutions are homotopy equivalent.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ C).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).hom (CategoryTheory.CategoryStruct.comp Q.π h) = CategoryTheory.CategoryStruct.comp P.π h

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) : CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).hom Q.π = P.π

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ C).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).inv (CategoryTheory.CategoryStruct.comp P.π h) = CategoryTheory.CategoryStruct.comp Q.π h

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution X) : CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).inv P.π = Q.π

@[reducible, inline]

noncomputable abbrev CategoryTheory.projectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] (Z : C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasProjectiveResolution Z] : CategoryTheory.ProjectiveResolution Z

An arbitrarily chosen projective resolution of an object.

Equations

• CategoryTheory.projectiveResolution Z = ⋯.some

noncomputable def CategoryTheory.projectiveResolutions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] : CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.down ℕ))

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ProjectiveResolution.iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X : C} (P : CategoryTheory.ProjectiveResolution X) : (CategoryTheory.projectiveResolutions C).obj X ≅ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj P.complex

If P : ProjectiveResolution X, then the chosen (projectiveResolutions C).obj X is isomorphic (in the homotopy category) to P.complex.

Equations

• P.iso = HomotopyCategory.isoOfHomotopyEquiv ((CategoryTheory.projectiveResolution X).homotopyEquiv P)

theorem CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (CategoryTheory.projectiveResolutions C).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp P.iso.inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) (CategoryTheory.CategoryStruct.comp Q.iso.inv h)

theorem CategoryTheory.ProjectiveResolution.iso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) : CategoryTheory.CategoryStruct.comp P.iso.inv ((CategoryTheory.projectiveResolutions C).map f) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) Q.iso.inv

theorem CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj Q.complex ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) (CategoryTheory.CategoryStruct.comp Q.iso.hom h) = CategoryTheory.CategoryStruct.comp P.iso.hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) h)

theorem CategoryTheory.ProjectiveResolution.iso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) Q.iso.hom = CategoryTheory.CategoryStruct.comp P.iso.hom ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ)

theorem CategoryTheory.exact_d_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.mk (CategoryTheory.Projective.d f) f ⋯).Exact

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 from the n-th object as Projective.d.

noncomputable def CategoryTheory.ProjectiveResolution.ofComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : ChainComplex C ℕ

Auxiliary definition for ProjectiveResolution.of.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.ProjectiveResolution.ofComplex_d_1_0 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : (CategoryTheory.ProjectiveResolution.ofComplex Z).d 1 0 = CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)

theorem CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ) : HomologicalComplex.ExactAt (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 1)

noncomputable instance CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ) : CategoryTheory.Projective ((CategoryTheory.ProjectiveResolution.ofComplex Z).X n)

Equations

• ⋯ = ⋯

@[irreducible]

noncomputable def CategoryTheory.ProjectiveResolution.of {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.ProjectiveResolution Z

In any abelian category with enough projectives, ProjectiveResolution.of Z constructs an projective resolution of the object Z.

Equations

• @CategoryTheory.ProjectiveResolution.of = CategoryTheory.ProjectiveResolution.wrapped✝.1

theorem CategoryTheory.ProjectiveResolution.of_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.ProjectiveResolution.of Z = CategoryTheory.ProjectiveResolution.mk (CategoryTheory.ProjectiveResolution.ofComplex Z) ⋯ (((CategoryTheory.ProjectiveResolution.ofComplex Z).toSingle₀Equiv Z).symm ⟨CategoryTheory.Projective.π Z, ⋯⟩) ⋯

@[instance 100]

noncomputable instance CategoryTheory.ProjectiveResolution.instHasProjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.HasProjectiveResolution Z

Equations

• ⋯ = ⋯

@[instance 100]

noncomputable instance CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] : CategoryTheory.HasProjectiveResolutions C

Equations

• ⋯ = ⋯