Documentation

Mathlib.CategoryTheory.Abelian.Ext

Ext #

We define Ext R C n : Cᵒᵖ ⥤ C ⥤ Module R for any R-linear abelian category C by (left) deriving in the first argument of the bifunctor (X, Y) ↦ Module.of R (unop X ⟶ Y).

Implementation #

TODO (@joelriou): When the derived category enters mathlib, the Ext groups shall be redefined using morphisms in the derived category, and then it will be possible to compute Ext using both projective or injective resolutions.

Ext R C n is defined by deriving in the first argument of (X, Y) ↦ Module.of R (unop X ⟶ Y) (which is the second argument of linearYoneda).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem ChainComplex.linearYonedaObj_X {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Abelian C] {α : Type u_3} [AddRightCancelSemigroup α] [One α] (X : ChainComplex C α) (A : Type u_4) [Ring A] [CategoryTheory.Linear A C] (Y : C) (i : α) :
    (X.linearYonedaObj A Y).X i = ModuleCat.of A (X.X i Y)
    @[simp]
    theorem ChainComplex.linearYonedaObj_d {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Abelian C] {α : Type u_3} [AddRightCancelSemigroup α] [One α] (X : ChainComplex C α) (A : Type u_4) [Ring A] [CategoryTheory.Linear A C] (Y : C) (i : α) (j : α) :
    (X.linearYonedaObj A Y).d i j = ModuleCat.ofHom (CategoryTheory.Linear.leftComp A Y (X.d j i))

    Given a chain complex X and an object Y, this is the cochain complex which in degree i consists of the module of morphisms X.X i ⟶ Y.

    Equations
    Instances For

      Ext can be computed using a projective resolution.

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

        If X : C is projective and n : ℕ, then Ext^(n + 1) X Y ≅ 0 for any Y.