THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Ext R C n : Cᵒᵖ ⥤ C ⥤ Module R for any
R-linear abelian category
by (left) deriving in the first argument of the bifunctor
(X, Y) ↦ Module.of R (unop X ⟶ Y).
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