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
.