Main result

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 chain 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.

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

Auxiliary construction for desc.

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

Auxiliary construction for desc.

@[simp]

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

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

Auxiliary construction for desc.

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

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

@[simp]

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

@[simp]

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

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

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

An auxiliary definition for descHomotopyZero.

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

An auxiliary definition for descHomotopyZero.

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

An auxiliary definition for descHomotopyZero.

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

Any descent of the zero morphism is homotopic to zero.

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

Two descents of the same morphism are homotopic.

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

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

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

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

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

Any two injective resolutions are homotopy equivalent.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[inline, reducible]

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

An arbitrarily chosen injective resolution of an object.

@[inline, reducible]

abbrev CategoryTheory.injectiveResolution.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (Z : C) [CategoryTheory.HasInjectiveResolution Z] : (CochainComplex.single₀ C).obj Z ⟶ CategoryTheory.injectiveResolution Z

The cochain map from cochain complex consisting of Z supported in degree 0 back to the arbitrarily chosen injective resolution injectiveResolution Z.

@[inline, reducible]

abbrev CategoryTheory.injectiveResolution.desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.HasInjectiveResolution X] [CategoryTheory.HasInjectiveResolution Y] : CategoryTheory.injectiveResolution X ⟶ CategoryTheory.injectiveResolution Y

The descent of a morphism to a cochain map between the arbitrarily chosen injective resolutions.

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

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

theorem CategoryTheory.exact_f_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Exact f (CategoryTheory.Injective.d f)

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.

@[simp]

theorem CategoryTheory.InjectiveResolution.ofCocomplex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) (i : ℕ) (j : ℕ) : HomologicalComplex.d (CategoryTheory.InjectiveResolution.ofCocomplex Z) i j = if h : i + 1 = j then CategoryTheory.CategoryStruct.comp (CochainComplex.mkAux (CategoryTheory.Injective.under Z) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.d (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.snd.snd { fst := CategoryTheory.Injective.syzygies { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := { fst := CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd (CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd) = 0) } }.snd.fst = 0) (fun t => { fst := CategoryTheory.Injective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Injective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst (CategoryTheory.Injective.d t.snd.snd.snd.snd.fst) = 0) } }) i).d₀ (CategoryTheory.eqToHom (_ : (CochainComplex.mkAux (CategoryTheory.Injective.under Z) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.d (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.snd.snd { fst := CategoryTheory.Injective.syzygies { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := { fst := CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd (CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd) = 0) } }.snd.fst = 0) (fun t => { fst := CategoryTheory.Injective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Injective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst (CategoryTheory.Injective.d t.snd.snd.snd.snd.fst) = 0) } }) (i + 1)).X₀ = (CochainComplex.mkAux (CategoryTheory.Injective.under Z) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.d (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.snd.snd { fst := CategoryTheory.Injective.syzygies { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := { fst := CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd (CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd) = 0) } }.snd.fst = 0) (fun t => { fst := CategoryTheory.Injective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Injective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst (CategoryTheory.Injective.d t.snd.snd.snd.snd.fst) = 0) } }) j).X₀)) else 0

@[simp]

theorem CategoryTheory.InjectiveResolution.ofCocomplex_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) (n : ℕ) : HomologicalComplex.X (CategoryTheory.InjectiveResolution.ofCocomplex Z) n = (CochainComplex.mkAux (CategoryTheory.Injective.under Z) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)) (CategoryTheory.Injective.d (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.snd.snd { fst := CategoryTheory.Injective.syzygies { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := { fst := CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd (CategoryTheory.Injective.d { fst := CategoryTheory.Injective.under Z, snd := { fst := CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z), snd := CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z) } }.2.snd) = 0) } }.snd.fst = 0) (fun t => { fst := CategoryTheory.Injective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Injective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst (CategoryTheory.Injective.d t.snd.snd.snd.snd.fst) = 0) } }) n).X₀

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

Auxiliary definition for InjectiveResolution.of.

theorem CategoryTheory.InjectiveResolution.ofCocomplex_sq_01_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.ι Z) (HomologicalComplex.d (CategoryTheory.InjectiveResolution.ofCocomplex Z) 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1) 0

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

theorem CategoryTheory.InjectiveResolution.of_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : CategoryTheory.InjectiveResolution.of Z = CategoryTheory.InjectiveResolution.mk (CategoryTheory.InjectiveResolution.ofCocomplex Z) (CochainComplex.mkHom ((CochainComplex.single₀ C).obj Z) (CategoryTheory.InjectiveResolution.ofCocomplex Z) (CategoryTheory.Injective.ι Z) 0 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.ι Z) (HomologicalComplex.d (CategoryTheory.InjectiveResolution.ofCocomplex Z) 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1) 0) fun n x => { fst := 0, snd := (_ : CategoryTheory.CategoryStruct.comp x.snd.fst (HomologicalComplex.d (CategoryTheory.InjectiveResolution.ofCocomplex Z) (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) (n + 1) (n + 2)) 0) })

@[irreducible]

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

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

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

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

def HomologicalComplex.Hom.HomologicalComplex.Hom.fromSingle₀InjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : CochainComplex C ℕ) (Y : C) (f : (CochainComplex.single₀ C).obj Y ⟶ X) [QuasiIso f] (H : ∀ (n : ℕ), CategoryTheory.Injective (HomologicalComplex.X X n)) : CategoryTheory.InjectiveResolution Y

If X is a cochain complex of injective objects and we have a quasi-isomorphism f : Y[0] ⟶ X, then X is an injective resolution of Y.