Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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”?
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 has binary coproducts, an initial object and coequalisers. That’s a better way to put it, I guess.
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.
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:
- 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.
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?
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.
Corrected a mistake copied from infinitary extensive category.
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.
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 ? Because a diagram indexed by a metacategory is in some sense “very large”. Some ideas/questions:
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.
Added algebraic set theory under ’Related notions’
I am moving the subsection on definable classes here, since it appears to duplicate the main text, feel free to move back any parts:
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 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 of sets having well-founded stratifications by sets (for instance the von Neumann cumulative hierarchy ).
I think it worth keeping a mention of Scott’s trick, I will edit it in later.
Re #15: Scott’s trick is already mentioned twice in Section 5 (colimits), when coequalizers are discussed.
Ah, well that’s ok then :-)
1 to 18 of 18