Large Categories in set.mm

[tirix]

A category C is called small if both ob(C) and hom(C) are actually sets and not proper classes, and large otherwise.

In set.mm, categories are structures, and ob(C) and hom(C) are written ( Base ` C ) and ( Hom ` C ) respectively, so they are images by Base and Hom, and by ~fvex, they must be sets and not proper classes.

Therefore, the current definition of categories in set.mm only represents small categories.

Am I correct? Does it matter for more advanced/meaningful category theory? @benjub @digama0

[benjub]

I haven't checked set.mm, so I'm assuming your first paragraph is correct, which implies indeed that set.mm can only define small categories. A now standard way to treat large categories in ZF, due to Grothendieck, is to use universes (which are sets which are models of ZF). Then, one relativizes to universes, that is, one considers U-categories, which are categories whose set of morphisms belongs to U. Since U is stable under most constructions, one can basically do anything within a given universe. Universes were defined (by @digama0 ?) in set.mm. So I think it is not worth, at least before a real need emerges, to introduce special syntax for large categories.

[digama0]

Yes, @benjub is correct. I considered defining large categories using class notations, but I decided against it because the things you can do with those kinds of large categories are rather limited, and it will not be long before you want the category of large categories, at which point the metamath encoding starts to break down. Set categories are much more well behaved.

To handle large categories, then, we relativize to a set U and have U-small and U-large categories. I defined "weak universes" in set.mm as a universe-like concept (a set closed under lots of operations) such that ZFC can prove the existence of a proper class of them. In most cases you can work with Set(U) for any set U, but if you need any closure conditions you can restrict to weak universes. You will need to be doing some rather advanced stuff to actually need Tarski-Grothendieck universes, but ax-groth is there if you need it.

[tirix]

Yes Benoît, Categories are currently defined with respect a Grothendieck Universe U, see for example comments for ~df-setc or ~df-ringc.

The universe U is for example required to be a weak universe in ~catcxpccl.

[tirix]

So, given a weak universe U e. WUni, I understand:

• the set V = ~P ( Base ` U ) can be considered our U-universal class,
• sets A C_ V can be considered the U-classes,
• sets X e. V can be considered the U-sets,
• sets A C_ V /\ A e/ V can be considered the U-proper classes.

And using those, we can have large and small U-Categories.

Very clear, thank you both!

[benjub]

• the set V = ~P ( Base ` U ) can be considered our U-universal class,

The role of a universe U is to mimic the universal class, so I'm not sure why you're taking ~P(Base(U)) instead of simply U ?

[tirix]

The role of a universe U is to mimic the universal class, so I'm not sure why you're taking ~P(Base(U)) instead of simply U ?

You're right, thanks, I was confused with theorems like ~wunstr.

[tirix]

...then, taking one more step, we have ( CatCat ` U ) (~df-catc/~catcval), which the comment says defines the category of small U-categories.

We then have ~catccat stating that ( CatCat ` U ) itself is a large category relative to U.

This puzzles me, my understanding is that ( CatCat ` U ) would actually be the category of all U-Categories (both small and large), and I would have further defined a ( SmallCat ` U ) = { c e. ( CatCat ` U ) | ( Base ` c ) e. U } as the set of small categories (actually it might even be better to define it as a category too...).

[digama0]

...then, taking one more step, we have ( CatCat ` U ) (~df-catc/~catcval), which the comment says defines the category of small U-categories.

We then have ~catccat stating that ( CatCat ` U ) itself is a large category relative to U.

This puzzles me, my understanding is that ( CatCat ` U ) would actually be the category of all U-Categories (both small and large), and I would have further defined a ( SmallCat ` U ) = { c e. ( CatCat ` U ) | ( Base ` c ) e. U } as the set of small categories (actually it might even be better to define it as a category too...).

The adjectives are wrong here. It is not a "small U-category", it is a "U-small category". Being a category here means A e. Cat and so implies sethood, while being U-small means A e. U, i.e. A is a member of the collection of categories U. A U-large category is thus an element of ( Cat \ U ), and ( CatCat ` U ) is one of these. Note that it is not ( Base ` A ) e. U, it is actually the category struct itself that must be an element of U. Simply asking for the base set to be in U is not good enough to make the overall collection a set, since you can have arbitrarily large irrelevant components in the structure. The distinction does not matter if you assume U is a weak universe and that all categories are "trimmed" to the base set and have no unnecessary slots.

[benjub]

Not sure what happened, so I'm copying my email below, which largely says the same things as @digama0, though I'd like to point out that you need to require both the set of objects and the set of morphisms to be small.

(copied email): The vocabulary varies a bit, but what I called U-category above means U-small category, that is, a category whose sets of objects and of morphisms are U-small, that is, belong to U. Looking at ~df-catc, I see that things are a bit different in set.mm: CatCat(U) is the category of all categories which belong to U. This is not standard: probably one should define CatCat(U) as the category of all U-small categories. The precise difference is hard to get since it depends on set.mm's encoding of a category as a particular type of extensible structure. However, since universes are stable under many constructions, the difference is not very important. In any case, the category of all U-small categories is not U-small: you have to "climb the ladder" and need another universe V such that P(U) \in V (or something close to that), and then the category of all U-small categories is V-small. This is why the Tarski--Grothendieck axiom is often assumed for convenience, since it is relatively consistent with ZFC. Where is this really needed ? Not sure... It is used at some places in SGA (Grothendieck and Deligne) from what I heard, and some people looked at Wiles's proof of Fermat's last theorem and concluded it needed used three universes or something like that (although the result itself probably requires far less than ZF).

Edit concerning the last part: Wiles used universes as a mere convenience, and they are straightforwardly removable from it, see https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof

[digama0]

Note that (for a weak universe U) every category whose sets of objects and morphisms are elements of U is isomorphic to a category in CatCat(U), constructed by combining these sets into an extensible structure, and the converse holds as well (every category in CatCat(U) has its set of objects and morphisms as elements of U). The advantage of this definition is that it works even on categories that have additional structure (like monoidal categories), rather than imposing that all categories in CatCat(U) are just defined by their objects and morphisms. This is consistent with the usual way in which classes like Mnd allow for additional structure so that Rng C_ Mnd holds.

My strategy for avoiding T-G in category theory is to have the trappings of a hierarchy of universes, but using weaker assumptions on the closure conditions of said universes (i.e. weak universes) and using targeted assumptions for any specific theorems (for example, a weak universe which is also closed under replacement by sets of cardinality less than kappa). In this way we can still prove all the theorems in category theory but without actually assuming the existence of a Grothendieck universe or inaccessible cardinal. I was planning to tackle individual relativization problems as they come, but I didn't have much use for categories in the first place so I left it at the basics and nothing even close to inaccessible cardinals popped up when proving the basic theory.

[benjub]

@digama0's 1st paragraph: I agree, and this indeed plays well with the rest of the extensible structure machinery. My point was that you seemed to imply above that by trimming the extensible structures to the categorical slots, requiring Objects(C) to be U-small was sufficient, whereas you actually need to require that also Morphisms(C) be U-small. Now, as you just wrote, requiring that the whole extensible structure be U-small is essentially equivalent by your argument of finding an isomorphic category in CatCat(U) to any U-small category. Some of these comments should be added to df-catc since that definition is different from the standard one.

Your 2nd paragraph: I appreciate this effort to find weaker notions of universes. I remember a nice answer by JD Hamkins on mathoverflow comparing various notions of universes but can't find it now...

[tirix]

Thanks again! I've posted a PR detailing that U-large categories are ( Cat \ U )... mainly for my own peace of mind.

The remark 3.45 of [Adamek] p.39 states:

3.45 REMARK Notice that when Ob(A) is a set, then Mor(A) must be a set, so that the category A = (Ob(A), hom, id, ⚬) must also be a set (cf. Exercise 3M).

...so actually in set.mm, there is no need to prove that, since our definition of U-small categories is somewhat stronger and also covers morphisms.

[digama0]

The analogue of that theorem for U-small categories is that if A is a category and Ob(A) e. U, and U is a weak universe, then there is a U-small category which is strictly isomorphic to A (that is, has the same set of objects and morphisms and composition).

[tirix]

The analogue of that theorem for U-small categories is that if A is a category and Ob(A) e. U, and U is a weak universe, then there is a U-small category which is strictly isomorphic to A (that is, has the same set of objects and morphisms and composition).

Great, I'll keep that as an exercise!

I'll close this issue if there is nothing else you or Benoît wants to react about.

[benjub]

I'm a bit skeptical about the remark above from the joy of cats and Mario's. Consider the monoid of ordinals under addition, seen as a category on one object. Its set of objects is small but its morphisms form a proper class. Are we assuming somewhere that categories are locally small ?

[digama0]

@benjub You're right, I read too quickly. The reason the proof goes through in Adamek is because the way things are set up there, part of the definition is that a category consists of a set hom(A, B) for every pair of objects A,B e. Ob(C). (In other words, yes all categories are locally small in Adamek.) To do this in the U-small setting you need to assume that hom(A, B) e. U for all A, B e. Ob(C); but actually I believe this is not sufficient for a weak universe because the claim that Mor(C) e. U follows from this is essentially the axiom of replacement, which is the one thing that weak universes don't have. You would need to assume Mor(C) e. U directly.

[benjub]

The vocabulary varies a bit, but what I called U-category above means U-small category, that is, a category whose sets of objects and of morphisms are U-small, that is, belong to U. Looking at ~df-catc, I see that things are a bit different in set.mm: CatCat(U) is the category of all categories which belong to U. This is not standard: probably one should define CatCat(U) as the category of all U-small categories. The precise difference is hard to get since it depends on set.mm's encoding of a category as a particular type of extensible structure. However, since universes are stable under many constructions, the difference is not very important. In any case, the category of all U-small categories is not U-small: you have to "climb the ladder" and need another universe V such that P(U) \in V (or something close that), and then the category of all U-small categories is V-small. This is why the Tarski--Grothendieck axiom is often assumed for convenience, since it is relatively consistent with ZFC. Where is this really needed ? Not sure... It is used at some places in SGA (Grothendieck and Deligne) from what I heard, and some people looked at Wiles's proof of Fermat's last theorem and concluded it needed three universes or something like that (although the result itself probably requires far less than ZF).

So ( CatCat ` U ) morphisms is U an element of U, and hence whose set of objects is also an element of U (at least this is the case for Grothendieck.

On Thu, Apr 14, 2022 at 11:49 AM tirix @.***> wrote:

...then, taking one more step, we have ( CatCat ` U ) (~df-catc http://us2.metamath.org:88/mpeuni/df-catc.html), which the comment says defines the category of small categories.

We then have ~df-catccat http://us2.metamath.org:88/mpeuni/catccat.html stating that ( CatCat ` U ) itself is a large category relative to U.

This puzzles me, my understanding is that ( CatCat U ) would actually be the category of all U-Categories (both small and large), and I would have further defined a ( SmallCat U ) = { c e. ( CatCat U ) | ( Base c ) e. U } as the set of small categories (actually it might even be better to define it as a category too...).

— Reply to this email directly, view it on GitHub https://github.com/metamath/set.mm/issues/2579#issuecomment-1098951079, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJZP563G5ZA45PIX2YUZI4TVE7SY7ANCNFSM5TMTDJUA . You are receiving this because you were mentioned.Message ID: @.***>