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ⁿ ---> ...
- cocomplex : cochain_complex C ℕ
- ι : (cochain_complex.single₀ C).obj Z ⟶ self.cocomplex
- injective : (∀ (n : ℕ), category_theory.injective (self.cocomplex.X n)) . "apply_instance"
- exact₀ : category_theory.exact (self.ι.f 0) (self.cocomplex.d 0 1) . "apply_instance"
- exact : (∀ (n : ℕ), category_theory.exact (self.cocomplex.d n (n + 1)) (self.cocomplex.d (n + 1) (n + 2))) . "apply_instance"
- mono : category_theory.mono (self.ι.f 0) . "apply_instance"
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 withinjective
andexact
instances)injective_resolution.ι Z
: the cochain map from(single C _ 0).obj Z
toinjective_resolution Z
(all the components are equipped withmono
instances, and when the category isabelian
we will showι
is a quasi-iso).
Instances for category_theory.InjectiveResolution
- category_theory.InjectiveResolution.has_sizeof_inst
- out : nonempty (category_theory.InjectiveResolution Z)
An object admits a injective resolution.
- out : ∀ (Z : C), category_theory.has_injective_resolution Z
You will rarely use this typeclass directly: it is implied by the combination
[enough_injectives C]
and [abelian C]
.
Instances of this typeclass
An injective object admits a trivial injective resolution: itself in degree 0.
Equations
- category_theory.InjectiveResolution.self Z = {cocomplex := (cochain_complex.single₀ C).obj Z, ι := 𝟙 ((cochain_complex.single₀ C).obj Z), injective := _, exact₀ := _, exact := _, mono := _}