mathlib documentation


Ext #

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

Implementation #

It's not actually necessary here to assume C is abelian, but the hypotheses, involving both C and Cᵒᵖ, are quite lengthy, and in practice the abelian case is hopefully enough.

PROJECT we don't yet have injective resolutions and right derived functors (although this is only a copy-and-paste dualisation) so we can't even state the alternative definition in terms of right-deriving in the first argument, let alone start the harder project of showing they agree.

noncomputable def Ext (R : Type u_1) [ring R] (C : Type u_2) [category_theory.category C] [category_theory.abelian C] [category_theory.linear R C] [category_theory.enough_projectives C] (n : ) :

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

theorem Ext_map_app (R : Type u_1) [ring R] (C : Type u_2) [category_theory.category C] [category_theory.abelian C] [category_theory.linear R C] [category_theory.enough_projectives C] (n : ) (c c' : Cᵒᵖ) (f : c c') (j : C) :
noncomputable def Ext_succ_of_projective (R : Type u_1) [ring R] (C : Type u_2) [category_theory.category C] [category_theory.abelian C] [category_theory.linear R C] [category_theory.enough_projectives C] (X Y : C) [category_theory.projective X] (n : ) :
((Ext R C (n + 1)).obj (opposite.op X)).obj Y 0

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