Documentation

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

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

    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
        theorem CategoryTheory.InjectiveResolution.exact_succ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {Z : C} (I : InjectiveResolution Z) (n : ) :
        { X₁ := I.cocomplex.X n, X₂ := I.cocomplex.X (n + 1), X₃ := I.cocomplex.X (n + 2), f := I.cocomplex.d n (n + 1), g := I.cocomplex.d (n + 1) (n + 2), zero := }.Exact

        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

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For