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 CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {I : C} [CategoryTheory.Injective I] {L : CochainComplex C ℤ} {i : ℤ} (ι : (singleFunctor C i).obj I ⟶ L) [L.IsStrictlyGE i] [QuasiIsoAt ι i] : CategoryTheory.IsSplitMono ι

theorem DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {I : C} [CategoryTheory.Injective I] {K : CochainComplex C ℤ} {i : ℤ} (φ : Q.obj K ⟶ Q.obj ((CochainComplex.singleFunctor C i).obj I)) (n : ℤ) (hn : i < n) [K.IsStrictlyGE n] : φ = 0

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

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

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.