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 CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} [CategoryTheory.Projective P] {K : CochainComplex C ℤ} {i : ℤ} (π : K ⟶ (singleFunctor C i).obj P) [K.IsStrictlyLE i] [QuasiIsoAt π i] : CategoryTheory.IsSplitEpi π

theorem DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {P : C} [CategoryTheory.Projective P] {L : CochainComplex C ℤ} {i : ℤ} (φ : Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ Q.obj L) (n : ℤ) (hn : n < i) [L.IsStrictlyLE n] : φ = 0

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

theorem CategoryTheory.hasExt_of_enoughProjectives (C : Type u) [Category.{v, u} C] [Abelian C] [LocallySmall.{w, v, u} C] [EnoughProjectives C] : HasExt C

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.