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

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.

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 : ℕ)
:

`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`

).

## Instances For

def
extSuccOfProjective
(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 : C)
(Y : C)
[CategoryTheory.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`

.