Commit 2025-04-22 08:04 df8d984a

feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives (#19591) Let C : Type u be an abelian category (Category.{v} C). We deduce from #19585 that Ext X Y 0 identifies to the type of morphisms from X to Y. Moreover, assuming that C has enough projectives and is locally w-small, i.e. the type of morphisms in C are Small.{w}, 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. This is an important step in order to get a reasonably usable API for Ext-groups.