# Injective resolutions #

An injective resolution `I : InjectiveResolution Z`

of an object `Z : C`

consists of
an `ℕ`

-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ⁿ ---> ...
```

- cocomplex : CochainComplex C ℕ
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

`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

- ι : (CochainComplex.single₀ C).obj Z ⟶ s.cocomplex
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

`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

- injective : ∀ (n : ℕ), CategoryTheory.Injective (HomologicalComplex.X s.cocomplex n)
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

`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

- exact₀ : CategoryTheory.Exact (HomologicalComplex.Hom.f s.ι 0) (HomologicalComplex.d s.cocomplex 0 1)
`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`

.`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

- exact : ∀ (n : ℕ), CategoryTheory.Exact (HomologicalComplex.d s.cocomplex n (n + 1)) (HomologicalComplex.d s.cocomplex (n + 1) (n + 2))
`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`

.`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

- mono : CategoryTheory.Mono (HomologicalComplex.Hom.f s.ι 0)
`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`

.`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

`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`

.

`injectiveResolution Z`

: the`ℕ`

-indexed cochain complex (equipped with`injective`

and`exact`

instances)`InjectiveResolution.ι Z`

: the cochain map from`(single C _ 0).obj Z`

to`InjectiveResolution Z`

(all the components are equipped with`Mono`

instances, and when the category is`Abelian`

we will show`ι`

is a quasi-iso).

## Instances For

- out : Nonempty (CategoryTheory.InjectiveResolution Z)
An object admits an injective resolution.

An object admits an injective resolution.

## Instances

- out : ∀ (Z : C), CategoryTheory.HasInjectiveResolution Z

You will rarely use this typeclass directly: it is implied by the combination
`[EnoughInjectives C]`

and `[Abelian C]`

.

## Instances

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