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.
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.