Add the categories of filtered vector spaces and of finite-dimensional vector spaces

[ScriptRaccoon]

This PR adds three categories to the database and decides all of their properties:

FinVect, the category of finite-dimensional vector spaces over a field K.

It is a bit strange that this basic category was missing all the time! After all, we already have several other categories defined by finiteness conditions such as Ab_fg. Also, Split is the category of F₂-vector spaces of dimension $\leq 1$.

To decide all properties, I have actually added three entries (FinVect_f, FinVect_c, FinVect_u), corresponding to three cases:

1. K is finite
2. K is countably infinite
3. K is uncountable

This is required to decide if FinVect is locally finite or essentially countable (http://localhost:5173/category-comparison/FinVect_c/FinVect_f/FinVect_u). This is a bit awkward, but I don't know a better solution right now, cf. #7.

The only non-trivial result is that FinVect is $\aleph_1$-accessible. More generally, if R is a noetherian ring, the category of finitely generated R-modules is $\aleph_1$-accessible. The case R = Z is already in the database.

I have added all 3 instances of FinVect to decided_categories.json, so that its properties must remain decided.

FiltVect, the category of filtered vector spaces over a field K.

Here, quite a bit of work had to be done, in particular for the proof that it is locally finitely presentable.

Surprisingly, it turns out that (currently) it has exactly the same properties as TorsFreeAb! These categories can be distinguished by the property of having a projective generator, which still needs to be added (cf. #162).

BG for uncountable groups G

The cases of BG where G is finite or where G is countably infinite were already added, so it makes sense to add the remaining case. This is consistent with the three instances of FinVect from above.

---

Follow-up categories:

• exhaustive + separated filtered vector spaces
• graded vector spaces*
• chain complexes
• acyclic chain complexes
• spectral sequences

*boring as a plain category, but an important building block