English
Ext is defined as a derived functor in the first argument using a projective resolution and Hom.
Русский
Ext — производная функтор в первом аргументе через проективное разрешение и Hom.
LaTeX
$$$\\text{Ext}(n) \\;=\\; \\text{derived functor of }\\operatorname{Hom}(-,-)\\text{ in the first variable}$$$
Lean4
/-- `Ext R C n` is defined by deriving in
the first argument of `(X, Y) ↦ ModuleCat.of R (unop X ⟶ Y)`
(which is the second argument of `linearYoneda`).
-/
def Ext (n : ℕ) : Cᵒᵖ ⥤ C ⥤ ModuleCat R :=
Functor.flip
{ obj := fun Y => (((linearYoneda R C).obj Y).rightOp.leftDerived n).leftOp
map := fun f => ((((linearYoneda R C).map f).rightOp).leftDerived n).leftOp }
