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.