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

source

structure CategoryTheory.InjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImages C] (Z : C) :

Type (max u v)

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)
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 : ∀ (n : ℕ), CategoryTheory.Exact (HomologicalComplex.d s.cocomplex n (n + 1)) (HomologicalComplex.d s.cocomplex (n + 1) (n + 2))
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).
mono : CategoryTheory.Mono (HomologicalComplex.Hom.f s.ι 0)
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).

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