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) ↦ ModuleCat.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.

def Ext (R : Type u_1) [Ring R] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.EnoughProjectives C] (n : ℕ) : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (ModuleCat R))

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

def ChainComplex.linearYonedaObj {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) : CochainComplex (ModuleCat A) α

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.

@[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 = ((CategoryTheory.linearYoneda A C).obj Y).obj (Opposite.op (X.X i))

@[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))

def CategoryTheory.ProjectiveResolution.isoExt {R : Type u_1} [Ring R] {C : Type u_2} [Category.{u_3, u_2} C] [Abelian C] [Linear R C] [EnoughProjectives C] {X : C} (P : ProjectiveResolution X) (n : ℕ) (Y : C) : ((Ext R C n).obj (Opposite.op X)).obj Y ≅ HomologicalComplex.homology (P.complex.linearYonedaObj R Y) n

Ext can be computed using a projective resolution.

theorem isZero_Ext_succ_of_projective {R : Type u_1} [Ring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.EnoughProjectives C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ) : CategoryTheory.Limits.IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)

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