# mathlibdocumentation

category_theory.abelian.ext

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

@[simp]
theorem Ext_obj_map (R : Type u_1) [ring R] (C : Type u_2) (n : ) (k : Cᵒᵖ) (j j' : C) (f : j j') :
((Ext R C n).obj k).map f =
@[simp]
theorem Ext_obj_obj (R : Type u_1) [ring R] (C : Type u_2) (n : ) (k : Cᵒᵖ) (j : C) :
noncomputable def Ext (R : Type u_1) [ring R] (C : Type u_2) (n : ) :

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 linear_yoneda).

Equations
@[simp]
theorem Ext_map_app (R : Type u_1) [ring R] (C : Type u_2) (n : ) (c c' : Cᵒᵖ) (f : c c') (j : C) :
((Ext R C n).map f).app j = C).obj j).right_op.left_derived n).map f.unop).unop
noncomputable def Ext_succ_of_projective (R : Type u_1) [ring R] (C : Type u_2) (X Y : C) (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.

Equations