Preadditive categories are not assumed to be locally small

[ScriptRaccoon]

Before this PR, preadditive categories were assumed to be locally small, or rather locally essentially small so that the property would be invariant under equivalences. This is not natural, however, since our categories are not locally essentially small by default. It also leads to the awkward situation that a functor category $[C,Ab]$ is not necessarily preadditive (an example I was about to add to the database), let alone abelian, since this may depend on the size of $C$.

Hence, the definition has been changed. A preadditive category now has hom-collections equipped with structures of (possibly large) abelian groups. Of course, if we want to talk about $Ab$-enriched categories, we can simply combine the two properties locally small and preadditive.

Luckily, this did not remove any of the properties of the recorded categories. This is because preadditivity previously only required local essential smallness, and all recorded preadditive categories already had a manual assignment stating that they are locally small. (The next PR will add examples of abelian categories that are not locally small.)

However, we need to check whether all implications involving preadditive categories and related notions remain valid. Of course, preadditive ==> locally essentially small needs to be removed. The implications involving the property abelian seem to be OK. However, two implications concerning Grothendieck abelian categories needed to be adjusted:

1. A Grothendieck abelian category (with the new convention that it is not necessarily locally essentially small) need not be locally presentable. A counterexample is $[Set_{\mathrm{disc}}, Ab]$, which will be added in a future PR. However, a locally essentially small Grothendieck abelian category is locally presentable.

2. A Grothendieck abelian category need not have a cogenerator. A counterexample is $[On,Ab]$, which will be added in a future PR. However, a locally essentially small Grothendieck abelian category has a cogenerator.

In this context, the result that a self-dual Grothendieck abelian category is trivial has been double-checked to ensure that its proof does not require local smallness. In fact, the result has been drastically strengthened as follows: an additive balanced category satisfying CSP and CIP is trivial. More precisely, if an object $A$ in an additive category with products and coproducts has the property that the canonical morphism $\bigoplus_n A \to \prod_n A$ is an isomorphism, then $A = 0$. A full proof is given as well. Previously, this was just a reference to an exercise in Freyd's book.

As a nice byproduct, three properties of the category of abelian sheaves $Sh(X,Ab)$ have been proved automatically: CSP is not satisfied, and hence neither exact cofiltered limits nor cofiltered-limit-stable epimorphisms hold. The number of unknown (category, property)-pairs went down from 75 to 72.

But another number went up, unfortunately – the one I want to reduce in the context of this milestone. The number of consistent yet unwitnessed property combinations went up from 595 to 631. The 36 new combinations are:

abelian ∧ ¬locally essentially small
additive ∧ ¬locally essentially small
Grothendieck abelian ∧ ¬accessible
Grothendieck abelian ∧ ¬CIP
Grothendieck abelian ∧ ¬cocartesian cofiltered limits
Grothendieck abelian ∧ ¬cofiltered limits
Grothendieck abelian ∧ ¬cogenerating set
Grothendieck abelian ∧ ¬cogenerator
Grothendieck abelian ∧ ¬complete
Grothendieck abelian ∧ ¬concretizable
Grothendieck abelian ∧ ¬connected limits
Grothendieck abelian ∧ ¬cosifted limits
Grothendieck abelian ∧ ¬cototal
Grothendieck abelian ∧ ¬countable powers
Grothendieck abelian ∧ ¬countable products
Grothendieck abelian ∧ ¬directed limits
Grothendieck abelian ∧ ¬disjoint products
Grothendieck abelian ∧ ¬extremal cogenerating set
Grothendieck abelian ∧ ¬extremal cogenerator
Grothendieck abelian ∧ ¬locally essentially small
Grothendieck abelian ∧ ¬locally multi-presentable
Grothendieck abelian ∧ ¬locally poly-presentable
Grothendieck abelian ∧ ¬locally presentable
Grothendieck abelian ∧ ¬multi-complete
Grothendieck abelian ∧ ¬powers
Grothendieck abelian ∧ ¬products
Grothendieck abelian ∧ ¬sequential limits
Grothendieck abelian ∧ ¬total
Grothendieck abelian ∧ ¬well-copowered
Grothendieck abelian ∧ ¬well-powered
Grothendieck abelian ∧ ¬wide pullbacks
Grothendieck abelian ∧ ¬ℵ₁-cofiltered limits
Grothendieck abelian ∧ ¬ℵ₂-small powers
Grothendieck abelian ∧ ¬ℵ₂-small products
preadditive ∧ ¬locally essentially small
split abelian ∧ ¬locally essentially small

It is a bit awkward that a Grothendieck abelian category (which is not locally essentially small) does not necessarily have products (I think I know a counterexample). Basically, all non-trivial results about Grothendieck abelian categories seem to require local essential smallness. Still, I do not think that this property should be built into the definition.

[ScriptRaccoon]

@varkor I am eager to hear your opinion on this decision that preadditive categories may have large hom-groups. This adds some technical challenges, but on the other hand, I definitely want to say that all functor categories of Ab are abelian.

[varkor]

I think this is a reasonable change. It makes sense to separate properties into (nearly) atomic pieces, and I don't see a good reason to impose local smallness automatically here, given it is not a standing assumption for a category in CatDat. While it does mean there is a slight subtlety regarding the connection to existing literature, I don't anticipate it will cause much confusion.

[ScriptRaccoon]

@varkor Thanks a lot for the feedback! And I'm glad we are on the same page here. Especially since I already have a follow-up branch locally which adds some examples of abelian categories that are not locally small. This also made me realize that it all fits well together.