It's not actually necessary here to assume
C is abelian,
but the hypotheses, involving both
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.
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
X : C is projective and
n : ℕ, then
Ext^(n + 1) X Y ≅ 0 for any