Documentation

Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Smallness of Ext-groups from the existence of enough injectives #

Let C : Type u be an abelian category (Category.{v} C) that has enough injectives. If C is locally w-small, i.e. the type of morphisms in C are Small.{w}, then we show that the condition HasExt.{w} holds, which means that for X and Y in C, and n : ℕ, we may define Ext X Y n : Type w. In particular, this holds for w = v.

However, the main lemma hasExt_of_enoughInjectives is not made an instance: for a given category C, there may be different reasonable choices for the universe w, and if we have two HasExt.{w₁} and HasExt.{w₂} instances, we would have to specify the universe explicitly almost everywhere, which would be an inconvenience. Then, we must be very selective regarding HasExt instances.

Note: this file dualizes the results in HasEnoughProjectives.lean.

theorem CategoryTheory.Abelian.Ext.eq_zero_of_injective {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X I : C} {n : } [Injective I] (e : Ext X I (n + 1)) :
e = 0

If C is a locally w-small abelian category with enough injectives, then HasExt.{w} C holds. We do not make this an instance though: for a given category C, there may be different reasonable choices for the universe w, and if we have two HasExt.{w₁} C and HasExt.{w₂} C instances, we would have to specify the universe explicitly almost everywhere, which would be an inconvenience. Then, we must be very selective regarding HasExt instances.