# mathlib3documentation

category_theory.abelian.ext

# Ext #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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: State the alternative definition in terms of right deriving in the second argument, and show these agree.

@[simp]
theorem Ext_obj (R : Type u_1) [ring R] (C : Type u_2) (n : ) (k : Cᵒᵖ) :
(Ext R C n).obj k = {obj := λ (j : C), opposite.unop C).obj j).right_op.left_derived n).obj (opposite.unop k)), map := λ (j j' : C) (f : j j'), , map_id' := _, map_comp' := _}
@[simp]
theorem Ext_map (R : Type u_1) [ring R] (C : Type u_2) (n : ) (c c' : Cᵒᵖ) (f : c c') :
(Ext R C n).map f = {app := λ (j : C), C).obj j).right_op.left_derived n).map f.unop).unop, naturality' := _}
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
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