Documentation

Mathlib.CategoryTheory.Preadditive.InjectiveResolution

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

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.

Instances For

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

    An object admits an injective resolution.

    Instances

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

      Instances

        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