# 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 quasi-isomorphism I.ι from the cochain complex consisting just of Z in degree zero to I.cocomplex.

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

structure CategoryTheory.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 from the complex consisting of just Z supported in degree 0.

• cocomplex :

the cochain complex involved in the resolution

• injective : ∀ (n : ), CategoryTheory.Injective (self.cocomplex.X n)

the cochain complex must be degreewise injective

• hasHomology : ∀ (i : ), HomologicalComplex.HasHomology self.cocomplex i

the cochain complex must have homology

• ι : .obj Z self.cocomplex

the morphism from the single cochain complex with Z in degree 0

• quasiIso : QuasiIso self

the morphism from the single cochain complex with Z in degree 0 is a quasi-isomorphism

Instances For
theorem CategoryTheory.InjectiveResolution.injective {C : Type u} {Z : C} (self : ) (n : ) :
CategoryTheory.Injective (self.cocomplex.X n)

the cochain complex must be degreewise injective

theorem CategoryTheory.InjectiveResolution.hasHomology {C : Type u} {Z : C} (self : ) (i : ) :

the cochain complex must have homology

theorem CategoryTheory.InjectiveResolution.quasiIso {C : Type u} {Z : C} (self : ) :
QuasiIso self

the morphism from the single cochain complex with Z in degree 0 is a quasi-isomorphism

An object admits an injective resolution.

• An object admits an injective resolution.

Instances

An object admits an injective resolution.

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

• out : ∀ (Z : C),
Instances
theorem CategoryTheory.InjectiveResolution.exact_succ {C : Type u} {Z : C} (n : ) :
(CategoryTheory.ShortComplex.mk (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) ).Exact
@[simp]
theorem CategoryTheory.InjectiveResolution.ι_f_succ {C : Type u} {Z : C} (n : ) :
I.f (n + 1) = 0
theorem CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc {C : Type u} {Z : C} {Z : C} (h : I.cocomplex.X 1 Z) :
theorem CategoryTheory.InjectiveResolution.complex_d_comp {C : Type u} {Z : C} (n : ) :
CategoryTheory.CategoryStruct.comp (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) = 0

The (limit) kernel fork given by the composition Z ⟶ I.cocomplex.X 0 ⟶ I.cocomplex.X 1 when I : InjectiveResolution Z.

Equations
Instances For

Z is the kernel of I.cocomplex.X 0 ⟶ I.cocomplex.X 1 when I : InjectiveResolution Z.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
@[simp]
@[simp]
theorem CategoryTheory.InjectiveResolution.self_cocomplex {C : Type u} (Z : C) :
.cocomplex = .obj Z

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

Equations
Instances For