Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 12th 2020

Created the article. Small limits and large colimits.

• CommentRowNumber2.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 12th 2020

Other properties: infinitary Boolean pretopos.

• CommentRowNumber3.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 13th 2020

There is a paragraph in category of classes that I copied verbatim from proper class, where it was added in Revision 13 by David Roberts on May 7, 2019:

If one is working in the category of (definable) classes for ZF or ZFC, or the category of classes of NBG, then all finite external diagrams D→ClassD\to Class have colimits. The reduction to a coequaliser of a pair of finite coproducts works as per usual. Finite coproducts exist as one can use finite disjunctions of the defining formulas (in ZF(C)) or Class Separation (in NBG) to define a new class. Coequalisers then exist by the above argument, as Scott’s trick is available due to the class VV of sets having well-founded stratifications by sets (for instance the von Neumann cumulative hierarchy V=⋃ α∈ORDV αV = \bigcup_{\alpha\in ORD} V_\alpha).

What is a “definable class”? What is an “external diagram”?

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeDec 13th 2020

Wow, did I really write that? I just came back here to complain about the notion of the category of classes having all colimits, when we don’t necessarily say an elementary topos with NNO (as a first-order theory) has all small colimits.

A class in ZF(C) isn’t a thing, but what I meant was the sense in which set theorists usually refer to proper classes, defined by a formula with a free variable. One can define the syntactic category of ZF(C), where the objects are first-order formulas, and the category of classes of ZF(C), where the objects are first-order formulas with one free variable. These are equivalent, using pairing. The first more obviously has products, the products in the second category are construct via the (I guess adjoint) inverse to the inclusion functor.

On an external diagram … hmm. One can write down what a functor is in first-order terms (hence a diagram in metacategory, to borrow Mac Lane’s term), though I guess finiteness is an issue (standard vs non-standard etc). Certainly $\mathbf{Class}$ has binary coproducts, an initial object and coequalisers. That’s a better way to put it, I guess.

• CommentRowNumber5.
• CommentAuthorDavidRoberts
• CommentTimeDec 13th 2020

Also, the page says “infinitary extensive”, but then goes on to say “finite coproducts”. I think we should at a minimum say just that it’s an extensive category, and note that it can be possible to maybe make sense of the infinitary version, but it’s via internal diagrams, or by having a strong metatheory, like MK + superclasses or something.

• CommentRowNumber6.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 14th 2020
• (edited Dec 14th 2020)

Concerning finite coproducts: this is what the article extensive category says:

An infinitary extensive category is a category EE with all (small) coproducts such that the following analogous equivalent conditions hold:

1. Pullbacks of coproduct injections along arbitrary morphisms exist and finite coproducts are disjoint and stable under pullback.

Unless I am missing something (and the finite case really does imply the infinite case), there is a mistake here, which was copied over to category of classes.

• CommentRowNumber7.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 14th 2020
• (edited Dec 14th 2020)

A class in ZF(C) isn’t a thing, but what I meant was the sense in which set theorists usually refer to proper classes, defined by a formula with a free variable.

This is exactly what the article category of classes means by a class: a formula with a free variable.

On an external diagram … hmm. One can write down what a functor is in first-order terms (hence a diagram in metacategory, to borrow Mac Lane’s term)

This is exactly what the article means by a diagram: a functor written in first-order terms.

So can we remove this paragraph, since it is redundant?

• CommentRowNumber8.
• CommentAuthorDavidRoberts
• CommentTimeDec 14th 2020

Re #6 yes, there’s a mistake. Unless we want to claim that coproducts of internal families means infinitary extensive, which I don’t, then it shouldn’t say infinitary extensive.

I’m just worried that the definition of finite external diagram is a bit slippery, and so this would be better phrased in terms of nullary and binary coproducts, and coequalisers.

• CommentRowNumber9.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 14th 2020

Corrected a mistake copied from infinitary extensive category.

• CommentRowNumber10.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 14th 2020

Re #8: The main text of the article already proves that not only all finite external diagrams have colimits, but all large external diagrams have colimits, where a large diagram is a diagram indexed by a large category, which is not necessarily locally small.

So is it true then that this paragraph is redundant? It appears to me this way.

• CommentRowNumber11.
• CommentAuthorDavidRoberts
• CommentTimeDec 14th 2020

I think so.

I’d like to pin down the statement about large colimits, since it seems a bit iffy to me. By a “large” category, what is meant? An internal category in $\mathbf{Class}$? Because a diagram indexed by a metacategory is in some sense “very large”. Some ideas/questions:

1. Is a cocomplete small category also a preorder? Very cursory search doesn’t help me. The best I can do is Remark 2.4 a paper of Pavlovic (pdf), but it doesn’t help as $\mathbf{Class}$ is not locally cartesian closed.
2. Does the fact every class is a subclass of $V$ help in constructing colimits? There is no universal family, though, for the usual reason.
• CommentRowNumber12.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 15th 2020

By a “large” category, what is meant? An internal category in Class?

Yes. The article tries to clarify this at the end of Section 2: https://ncatlab.org/nlab/show/category+of+classes#relations_and_maps

Because a diagram indexed by a metacategory is in some sense “very large”.

It is, but I think we can treat it correctly, as described here in Section 3: https://ncatlab.org/nlab/show/category+of+classes#diagrams

Is a cocomplete small category also a preorder?

Yes, its opposite category is a complete small category, and we have an article about this: https://ncatlab.org/nlab/show/complete+small+category

But this argument is not applicable to classes, since the argument relies on the existence of powerobjects, which classes lack, they only have powerclasses (the class of all subsets), which do not lead to the same conclusion.

Does the fact every class is a subclass of VV help in constructing colimits? There is no universal family, though, for the usual reason.

The existence of class-indexed coproducts of classes is essentially tautological, because of the way class-indexed families of classes are defined: as maps of classes p:T→B. Likewise, a collection of maps p*{b}→X for all b∈B is by definition a map T→X, since we do not have any other way to express this concept.

So the statement about class-indexed colimits is true, but maybe not as interesting since we essentially define all notions to make it true.

• CommentRowNumber13.
• CommentAuthorDavidRoberts
• CommentTimeDec 16th 2020

Added algebraic set theory under ’Related notions’

• CommentRowNumber14.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 16th 2020

I am moving the subsection on definable classes here, since it appears to duplicate the main text, feel free to move back any parts:

Definable classes

If one is working in the category of (definable) classes for ZF or ZFC, or the category of classes of NBG, then all finite external diagrams $D\to Class$ have colimits. The reduction to a coequaliser of a pair of finite coproducts works as per usual. Finite coproducts exist as one can use finite disjunctions of the defining formulas (in ZF(C)) or Class Separation (in NBG) to define a new class. Coequalisers then exist by the above argument, as Scott’s trick is available due to the class $V$ of sets having well-founded stratifications by sets (for instance the von Neumann cumulative hierarchy $V = \bigcup_{\alpha\in ORD} V_\alpha$).

• CommentRowNumber15.
• CommentAuthorDavidRoberts
• CommentTimeDec 16th 2020

I think it worth keeping a mention of Scott’s trick, I will edit it in later.

• CommentRowNumber16.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 16th 2020

Re #15: Scott’s trick is already mentioned twice in Section 5 (colimits), when coequalizers are discussed.

• CommentRowNumber17.
• CommentAuthorDavidRoberts
• CommentTimeDec 16th 2020

Ah, well that’s ok then :-)

• CommentRowNumber18.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 3rd 2021