doc(category/abelian/ext): update module doc (#16512)

Update future work described in module doc, to reflect previous contributions to mathlib.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/abelian/ext.lean

@@ -14,19 +14,16 @@ import category_theory.abelian.projective
 # 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)`.
+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 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.
+PROJECT: State the alternative definition in terms of
+right deriving in the second argument, and show these agree.
 -/
 
 noncomputable theory