mathlib3 documentation

category_theory.preadditive.injective_resolution

Injective resolutions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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ⁿ ---> ...
source
@[nolint]
structure category_theory.InjectiveResolution {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] (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
source
@[class]
structure category_theory.has_injective_resolution {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] (Z : C) :
Prop

An object admits a injective resolution.

Instances of this typeclass
source
@[class]
structure category_theory.has_injective_resolutions (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] :
Prop

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

Instances of this typeclass
source
@[simp]
theorem category_theory.InjectiveResolution.ι_f_succ {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {Z : C} (I : category_theory.InjectiveResolution Z) (n : ℕ) :
I.ι.f (n + 1) = 0
source
@[simp]
theorem category_theory.InjectiveResolution.ι_f_zero_comp_complex_d {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {Z : C} (I : category_theory.InjectiveResolution Z) :
I.ι.f 0 ≫ I.cocomplex.d 0 1 = 0
source
@[simp]
theorem category_theory.InjectiveResolution.complex_d_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {Z : C} (I : category_theory.InjectiveResolution Z) (n : ℕ) :
I.cocomplex.d n (n + 1) ≫ I.cocomplex.d (n + 1) (n + 2) = 0
source
@[protected, instance]
def category_theory.InjectiveResolution.f.category_theory.mono {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {Z : C} (I : category_theory.InjectiveResolution Z) (n : ℕ) :
category_theory.mono (I.ι.f n)
source
noncomputable def category_theory.InjectiveResolution.self {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] (Z : C) [category_theory.injective Z] :
category_theory.InjectiveResolution Z

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

Equations