Documentation

Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

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

Let C : Type u be an abelian category (Category.{v} C) that has enough projectives. 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_enoughProjectives 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. So we must be very selective regarding HasExt instances.

theorem CategoryTheory.Abelian.Ext.eq_zero_of_projective {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {P Y : C} {n : } [Projective P] (e : Ext P Y (n + 1)) :
e = 0

If C is a locally w-small abelian category with enough projectives, 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.