Documentation

Mathlib.CategoryTheory.Abelian.Ext

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.

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

    If X : C is projective and n : ℕ, then Ext^(n + 1) X Y ≅ 0 for any Y.

    Instances For