Abelian categories with enough injectives have injective resolutions

Main results

When the underlying category is abelian:

• CategoryTheory.InjectiveResolution.desc: Given I : InjectiveResolution X and J : InjectiveResolution Y, any morphism X ⟶ Y admits a descent to a cochain map J.cocomplex ⟶ I.cocomplex. It is a descent in the sense that I.ι intertwines the descent and the original morphism, see CategoryTheory.InjectiveResolution.desc_commutes.

• CategoryTheory.InjectiveResolution.descHomotopy: Any two such descents are homotopic.

• CategoryTheory.InjectiveResolution.homotopyEquiv: Any two injective resolutions of the same object are homotopy equivalent.

• CategoryTheory.injectiveResolutions: If every object admits an injective resolution, we can construct a functor injectiveResolutions C : C ⥤ HomotopyCategory C.

• CategoryTheory.exact_f_d: f and Injective.d f are exact.

• CategoryTheory.InjectiveResolution.of: Hence, starting from a monomorphism X ⟶ J, where J is injective, we can apply Injective.d repeatedly to obtain an injective resolution of X.

noncomputable def CategoryTheory.InjectiveResolution.descFZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : J.cocomplex.X 0 ⟶ I.cocomplex.X 0

Auxiliary construction for desc.

theorem CategoryTheory.InjectiveResolution.exact₀ {C : Type u} [Category.{v, u} C] [Abelian C] {Z : C} (I : InjectiveResolution Z) : { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := I.cocomplex.X 0, X₃ := I.cocomplex.X 1, f := I.ι.f 0, g := I.cocomplex.d 0 1, zero := ⋯ }.Exact

noncomputable def CategoryTheory.InjectiveResolution.descFOne {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : J.cocomplex.X 1 ⟶ I.cocomplex.X 1

Auxiliary construction for desc.

@[simp]

theorem CategoryTheory.InjectiveResolution.descFOne_zero_comm {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : CategoryStruct.comp (J.cocomplex.d 0 1) (descFOne f I J) = CategoryStruct.comp (descFZero f I J) (I.cocomplex.d 0 1)

noncomputable def CategoryTheory.InjectiveResolution.descFSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (I : InjectiveResolution Y) (J : InjectiveResolution Z) (n : ℕ) (g : J.cocomplex.X n ⟶ I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1)) (w : CategoryStruct.comp (J.cocomplex.d n (n + 1)) g' = CategoryStruct.comp g (I.cocomplex.d n (n + 1))) : (g'' : J.cocomplex.X (n + 2) ⟶ I.cocomplex.X (n + 2)) ×' CategoryStruct.comp (J.cocomplex.d (n + 1) (n + 2)) g'' = CategoryStruct.comp g' (I.cocomplex.d (n + 1) (n + 2))

Auxiliary construction for desc.

noncomputable def CategoryTheory.InjectiveResolution.desc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : J.cocomplex ⟶ I.cocomplex

A morphism in C descends to a cochain map between injective resolutions.

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : CategoryStruct.comp J.ι (desc f I J) = CategoryStruct.comp ((CochainComplex.single₀ C).map f) I.ι

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

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) {Z✝ : CochainComplex C ℕ} (h : I.cocomplex ⟶ Z✝) : CategoryStruct.comp J.ι (CategoryStruct.comp (desc f I J) h) = CategoryStruct.comp ((CochainComplex.single₀ C).map f) (CategoryStruct.comp I.ι h)

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

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes_zero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : CategoryStruct.comp (J.ι.f 0) ((desc f I J).f 0) = CategoryStruct.comp f (I.ι.f 0)

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) {Z✝ : C} (h : I.cocomplex.X 0 ⟶ Z✝) : CategoryStruct.comp (J.ι.f 0) (CategoryStruct.comp ((desc f I J).f 0) h) = CategoryStruct.comp (CategoryStruct.comp f (I.ι.f 0)) h

noncomputable def CategoryTheory.InjectiveResolution.descHomotopyZeroZero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) : I.cocomplex.X 1 ⟶ J.cocomplex.X 0

An auxiliary definition for descHomotopyZero.

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) : CategoryStruct.comp (I.cocomplex.d 0 1) (descHomotopyZeroZero f comm) = f.f 0

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) {Z✝ : C} (h : J.cocomplex.X 0 ⟶ Z✝) : CategoryStruct.comp (I.cocomplex.d 0 1) (CategoryStruct.comp (descHomotopyZeroZero f comm) h) = CategoryStruct.comp (f.f 0) h

noncomputable def CategoryTheory.InjectiveResolution.descHomotopyZeroOne {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) : I.cocomplex.X 2 ⟶ J.cocomplex.X 1

An auxiliary definition for descHomotopyZero.

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) : CategoryStruct.comp (I.cocomplex.d 1 2) (descHomotopyZeroOne f comm) = f.f 1 - CategoryStruct.comp (descHomotopyZeroZero f comm) (J.cocomplex.d 0 1)

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) {Z✝ : C} (h : J.cocomplex.X 1 ⟶ Z✝) : CategoryStruct.comp (I.cocomplex.d 1 2) (CategoryStruct.comp (descHomotopyZeroOne f comm) h) = CategoryStruct.comp (f.f 1 - CategoryStruct.comp (descHomotopyZeroZero f comm) (J.cocomplex.d 0 1)) h

noncomputable def CategoryTheory.InjectiveResolution.descHomotopyZeroSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryStruct.comp g (J.cocomplex.d n (n + 1))) : I.cocomplex.X (n + 3) ⟶ J.cocomplex.X (n + 2)

An auxiliary definition for descHomotopyZero.

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryStruct.comp g (J.cocomplex.d n (n + 1))) : CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3)) (descHomotopyZeroSucc f n g g' w) = f.f (n + 2) - CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryStruct.comp g (J.cocomplex.d n (n + 1))) {Z✝ : C} (h : J.cocomplex.X (n + 2) ⟶ Z✝) : CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3)) (CategoryStruct.comp (descHomotopyZeroSucc f n g g' w) h) = CategoryStruct.comp (f.f (n + 2) - CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))) h

noncomputable def CategoryTheory.InjectiveResolution.descHomotopyZero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp I.ι f = 0) : Homotopy f 0

Any descent of the zero morphism is homotopic to zero.

noncomputable def CategoryTheory.InjectiveResolution.descHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) {I : InjectiveResolution Y} {J : InjectiveResolution Z} (g h : I.cocomplex ⟶ J.cocomplex) (g_comm : CategoryStruct.comp I.ι g = CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι) (h_comm : CategoryStruct.comp I.ι h = CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι) : Homotopy g h

Two descents of the same morphism are homotopic.

noncomputable def CategoryTheory.InjectiveResolution.descIdHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (I : InjectiveResolution X) : Homotopy (desc (CategoryStruct.id X) I I) (CategoryStruct.id I.cocomplex)

The descent of the identity morphism is homotopic to the identity cochain map.

noncomputable def CategoryTheory.InjectiveResolution.descCompHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (I : InjectiveResolution X) (J : InjectiveResolution Y) (K : InjectiveResolution Z) : Homotopy (desc (CategoryStruct.comp f g) K I) (CategoryStruct.comp (desc f J I) (desc g K J))

The descent of a composition is homotopic to the composition of the descents.

noncomputable def CategoryTheory.InjectiveResolution.homotopyEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (I J : InjectiveResolution X) : HomotopyEquiv I.cocomplex J.cocomplex

Any two injective resolutions are homotopy equivalent.

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (I J : InjectiveResolution X) : CategoryStruct.comp I.ι (I.homotopyEquiv J).hom = J.ι

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (I J : InjectiveResolution X) {Z : CochainComplex C ℕ} (h : J.cocomplex ⟶ Z) : CategoryStruct.comp I.ι (CategoryStruct.comp (I.homotopyEquiv J).hom h) = CategoryStruct.comp J.ι h

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (I J : InjectiveResolution X) : CategoryStruct.comp J.ι (I.homotopyEquiv J).inv = I.ι

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (I J : InjectiveResolution X) {Z : CochainComplex C ℕ} (h : I.cocomplex ⟶ Z) : CategoryStruct.comp J.ι (CategoryStruct.comp (I.homotopyEquiv J).inv h) = CategoryStruct.comp I.ι h

@[reducible, inline]

noncomputable abbrev CategoryTheory.injectiveResolution {C : Type u} [Category.{v, u} C] [Abelian C] (Z : C) [HasInjectiveResolution Z] : InjectiveResolution Z

An arbitrarily chosen injective resolution of an object.

noncomputable def CategoryTheory.injectiveResolutions (C : Type u) [Category.{v, u} C] [Abelian C] [HasInjectiveResolutions C] : Functor C (HomotopyCategory C (ComplexShape.up ℕ))

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

noncomputable def CategoryTheory.InjectiveResolution.iso {C : Type u} [Category.{v, u} C] [Abelian C] [HasInjectiveResolutions C] {X : C} (I : InjectiveResolution X) : (injectiveResolutions C).obj X ≅ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj I.cocomplex

If I : InjectiveResolution X, then the chosen (injectiveResolutions C).obj X is isomorphic (in the homotopy category) to I.cocomplex.

theorem CategoryTheory.InjectiveResolution.iso_hom_naturality {C : Type u} [Category.{v, u} C] [Abelian C] [HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) : CategoryStruct.comp ((injectiveResolutions C).map f) J.iso.hom = CategoryStruct.comp I.iso.hom ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ)

theorem CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj J.cocomplex ⟶ Z) : CategoryStruct.comp ((injectiveResolutions C).map f) (CategoryStruct.comp J.iso.hom h) = CategoryStruct.comp I.iso.hom (CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) h)

theorem CategoryTheory.InjectiveResolution.iso_inv_naturality {C : Type u} [Category.{v, u} C] [Abelian C] [HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) : CategoryStruct.comp I.iso.inv ((injectiveResolutions C).map f) = CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) J.iso.inv

theorem CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryStruct.comp f (J.ι.f 0)) {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (injectiveResolutions C).obj Y ⟶ Z) : CategoryStruct.comp I.iso.inv (CategoryStruct.comp ((injectiveResolutions C).map f) h) = CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) (CategoryStruct.comp J.iso.inv h)

theorem CategoryTheory.exact_f_d {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] {X Y : C} (f : X ⟶ Y) : { X₁ := X, X₂ := Y, X₃ := Injective.syzygies f, f := f, g := Injective.d f, zero := ⋯ }.Exact

Our goal is to define InjectiveResolution.of Z : InjectiveResolution Z. The 0-th object in this resolution will just be Injective.under Z, i.e. an arbitrarily chosen injective object with a map from Z. After that, we build the n+1-st object as Injective.syzygies applied to the previously constructed morphism, and the map from the n-th object as Injective.d.

noncomputable def CategoryTheory.InjectiveResolution.ofCocomplex {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] (Z : C) : CochainComplex C ℕ

Auxiliary definition for InjectiveResolution.of.

theorem CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1 {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] (Z : C) : (ofCocomplex Z).d 0 1 = Injective.d (Injective.ι Z)

theorem CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] (Z : C) (n : ℕ) : HomologicalComplex.ExactAt (ofCocomplex Z) (n + 1)

instance CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] (Z : C) (n : ℕ) : Injective ((ofCocomplex Z).X n)

theorem CategoryTheory.InjectiveResolution.of_def {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] [EnoughInjectives C] (Z : C) : of Z = { cocomplex := ofCocomplex Z, injective := ⋯, hasHomology := ⋯, ι := ((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩, quasiIso := ⋯ }

@[irreducible]

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

In any abelian category with enough injectives, InjectiveResolution.of Z constructs an injective resolution of the object Z.

@[instance 100]

instance CategoryTheory.InjectiveResolution.instHasInjectiveResolution {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] (Z : C) : HasInjectiveResolution Z

@[instance 100]

instance CategoryTheory.InjectiveResolution.instHasInjectiveResolutions {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] : HasInjectiveResolutions C

@[reducible, inline]

noncomputable abbrev CategoryTheory.InjectivePresentation.shortComplex {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (ip : InjectivePresentation X) : ShortComplex C

Given an injective presentation M → I, the short complex 0 → M → I → N → 0.

theorem CategoryTheory.InjectivePresentation.shortExact_shortComplex {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (ip : InjectivePresentation X) : ip.shortComplex.ShortExact