# Injective resolutions #

A injective resolution I : InjectiveResolution Z of an object Z : C consists of a ℕ-indexed cochain complex I.cocomplex of injective objects, along with a cochain map I.ι from cochain complex consisting just of Z in degree zero to C, so that the augmented cochain complex is exact.

Z ----> 0 ----> ... ----> 0 ----> ...
|       |                 |
|       |                 |
v       v                 v
I⁰ ---> I¹ ---> ... ----> Iⁿ ---> ...

@[nolint]
structure category_theory.InjectiveResolution {C : Type u} (Z : C) :
Type (max u v)

An InjectiveResolution Z consists of a bundled ℕ-indexed cochain complex of injective objects, along with a quasi-isomorphism to the complex consisting of just Z supported in degree 0.

Except in situations where you want to provide a particular injective resolution (for example to compute a derived functor), you will not typically need to use this bundled object, and will instead use

• injective_resolution Z: the ℕ-indexed cochain complex (equipped with injective and exact instances)
• injective_resolution.ι Z: the cochain map from (single C _ 0).obj Z to injective_resolution Z (all the components are equipped with mono instances, and when the category is abelian we will show ι is a quasi-iso).
Instances for category_theory.InjectiveResolution
• category_theory.InjectiveResolution.has_sizeof_inst
@[class]
• out :

An object admits a injective resolution.

Instances of this typeclass
@[class]
• out : ∀ (Z : C),

You will rarely use this typeclass directly: it is implied by the combination [enough_injectives C] and [abelian C].

Instances of this typeclass
@[simp]
theorem category_theory.InjectiveResolution.ι_f_succ {C : Type u} {Z : C} (n : ) :
I.ι.f (n + 1) = 0
@[simp]
theorem category_theory.InjectiveResolution.ι_f_zero_comp_complex_d {C : Type u} {Z : C}  :
I.ι.f 0 I.cocomplex.d 0 1 = 0
@[simp]
theorem category_theory.InjectiveResolution.complex_d_comp {C : Type u} {Z : C} (n : ) :
I.cocomplex.d n (n + 1) I.cocomplex.d (n + 1) (n + 2) = 0
@[protected, instance]

An injective object admits a trivial injective resolution: itself in degree 0.

Equations