You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
This is a super-odd result: https://doi.org/10.1016/0022-4049(71)90004-1
"We can suppose the objects of [an arbitrary category] K are ordinals, since we assume the axiom of choice for classes"
then using this show every category is a quotient by a congruence of a concrete one.
I do wonder the extent to which this is true without global choice, or even plain choice..
Only three pages of content, and the proof ends "The details are left to the reader."
One assumption that is not made explicit seems to be that the category should be locally small.
Yeah, I mean, that's a given. That assumption is foundation-independent, and a since a concrete category has a faithful functor to set, a quotient of a concrete category has small hom-sets (as long as one isn't working, for instance, in some kind of setoid/type theory foundations). But being able to well-order the collection of objects of one's category .... :astonished:
I assume that the "Gödel-Bernays set theory with the axiom of choice for classes" is the same as NBG (link to Wikipedia)?
Here classes are collections of sets with a certain property (so they are not as big as the proper classes that are sometimes used in category theory). In this case being able to well-order the collection of all sets is equivalent to global choice.
I'm also curious if result of the paper still holds without this. At the moment I think there is an error in the paper, but that's probably just me :smiley:
Looking forward to answers by others here.
I assume that the "Gödel-Bernays set theory with the axiom of choice for classes" is the same as NBG (link to Wikipedia)?
yes. Though note that in NBG (even without choice) every class is a subclass of the class V of all sets. So "every category" has its objects form a subclass of V. Then choice gets you that every class is in bijection with a class of ordinals, as V is then iso to ORD. The theorem is nice, but suspcious.
Thanks for sharing this - I like it. I only recently became aware that every small category is concrete, and that thus concreteness is a size issue at all.
What are you suspicious about? To me it looks convincing, but I didn't fill in the details left to the reader.
Note that in a set-theoretic context global choice is equivalent to "every fully faithul essentially surjective functor between locally small categories is part of an equivalence", so assuming your objects are ordinals shouldn't be more suspicious than choosing inverses for such half-equivalences.
True. Though one can work in a bicategory of categories, anafunctors and transformations, in the absence of global choice, with no ill effects. So maybe this framework could go at least partway towards resurrecting the result if no global choice is available?
The more I look at this paper I wonder how it got though refereeing. There's three 'It is evident', one 'details left to the reader' and one functor that is just declared to have some non-obvious property and no example of such a thing given. I think I would like to understand this construction and make a good conceptual explanation for it. Does anyone want to join me?
I would also like to understand the construction. At the moment, I don't understand the following claim on page 3 of 4:
" and are sets for every object of ".
This is my reasoning why this is not a set (if is locally small but not small):
is the set of all morphisms for an arbitrary morphism of with range/codomain .
Take a morphism in , with arbitrary. Then is a morphism in with .
Further, .
So should contain at least all morphisms of that are of the form , so it contains a proper class.
@Jens Hemelaer I think is only a morphism of if . So while arbitrary is not ok, I guess there would still be a proper class of such morphisms.
And of course, in the other direction, one would have in if .
Aside from all that, I really do wonder what is supposed to be. is not injective, necessarily. There are models where that fails. And one has issues at singular cardinals, even if one is willing to pull out Easton's theorem to guarantee it injective on regular cardinals in a particular model.
Possibly the fact this paper is not well known (compared to, say, Freyd's Homotopy is not concrete), may be a sign it's known to the "elders" (using Kevin Buzzard's word) to have a flaw, so isn't referenced anywhere prominent.
Oh I see, I read but it is as you say. That makes more sense.
I think , because it only needs to be faithful and not necessarily injective on objects?
It seems to me that is in bijection with morphisms into in whose domain is at most . As is locally small, is a set. Similarly is a set. And taking the contravariant powerset functor should work, as only faithfulness is needed. While it's irrelevant for the proof, note that the powerset functor is injective on objects: to recover a set from its powerset, just take the union! I think @David Michael Roberts was talking about the related fact that "cardinality of the powerset" need not be an injective function on cardinals.
Fun fact: regarding the universe of sets as partially ordered by inclusion, we have an adjunction iff .
I haven't checked all of the details (of the paper or of what I'm about to say), but I think one can follow a similar proof strategy while assuming ordinary AC instead of global AC: Given (whose objects are now just elements of ), define with the same objects, but maps in are given by factorizations of maps in with the property that the rank of is at most that of . Composition of two such factorizations is given by choosing the middle object to be the one of the middle objects with the smaller rank, or if the ranks agree, the rightmost one. Define as the set of all morphisms of into whose domain has rank at most that of . Given a morphism in , define by doing the composition in and taking the map from the resulting middle object to . is done similarly with maps out of . The rest follows the original proof, i.e. "The details are left to the reader."
David Michael Roberts said:
Possibly the fact this paper is not well known (compared to, say, Freyd's Homotopy is not concrete), may be a sign it's known to the "elders" (using Kevin Buzzard's word) to have a flaw, so isn't referenced anywhere prominent.
While there could be a subtle mistake somewhere, the overall proof is starting to look quite reasonable to me, so let me offer an alternative explanation why this isn't that well-known: the result doesn't really buy that much for the purposes of category theory. If you're working with some non-concretisable category, what use it is to know that it is the quotient of some non-canonical concretisable one?
Zooming out, what seems to be the key to the proof is that one can find for each object a set of objects such that any map factors via something in . Then one would like to define with the same objects and maps to be such factorizations. being locally small and being a set implies that this is collection is a set, and composition in induces a full functor . However, before one gets there one needs to make sure that is indeed a category: one needs to be able to compose such factorizations in a canonical way (so far: by choosing one of the two middle objects as the new middle object in a coherent way), and this seems to require more structure on the sets . In the original proof one sets whereas in what I wrote above I set to be the set of objects with rank at most that of .
Btw, this theorem of Kučera is written up (with essentially the same proof as in the paper) in section 6B of Adámek's "Theory of Mathematical Structures".
Some of my set theory is a bit rusty (so correct me if I'm wrong), but it seems that every set has a well-defined rank even without choice, and this rank is an ordinal and hence they can always be compared just fine (whereas for cardinals things can get murky without choice). Hence the proof strategy I outlined above should actually work even without any choice (axiom of foundation is important though). Note that it's still not a categorical construction: the rank of an object is not really a property of the category, but just a property of a particular implementation.
Yeah, so one can define the von Neumann hierarchy and if one has foundation (for instance in ZF), then every set appears somewhere in it. This gives an ordinal-valued rank for every set.
Then I think that it should be doable without choice
So here is a possible further improvement: let's say we start with ETCS as a foundation. Then IIRC the category of sets is equivalent to the category of material sets constructed as well-founded rooted trees in the structural sets. See Shulman's https://arxiv.org/abs/1808.05204, Lemma 9.1. Then one could define a rank-like invariant. Could it then be possible to describe a large category in ETCS foundations such that its objects inherit this rank-like invariant?
If one instead starts with Algebraic Set Theory, then I imagine there is a similar result for NBG (this may be in @Mike Shulman unreleased further work on stack semantics, cited in that paper). Then one could ask whether it is sensible to require that a large category is exactly a category internal to the category of classes (this is what the paper under discussion essentially does), or if it is taken to be an elementarily-defined structure, enriched over the category of sets. In the former case, given a material-structural equivalence one might be able to play the same game with ranks. In the latter case, it's not clear how to proceed....
@Martti Karvonen oh, yes. I was thinking of cardinalities. If one is working with categories up to equivalence, rather than isomorphism, or with structural sets, it's not clear what "injective functor" means, except injective-up-to-isomorphism. But that's not the setup here, so we are safe!
So here is a possible further improvement: let's say we start with ETCS as a foundation. Then IIRC the category of sets is equivalent to the category of material sets constructed as well-founded rooted trees in the structural sets. See Shulman's https://arxiv.org/abs/1808.05204, Lemma 9.1. Then one could define a rank-like invariant. Could it then be possible to describe a large category in ETCS foundations such that its objects inherit this rank-like invariant?
My first hunch is that working with large categories in ETCS would be at least as awkward as it would be in ZF as one can't quantify over classes. So formally the theorem at hand becomes a theorem schema/metatheorem: if we have formula(s) defining a large category, then one can write down formulas defining a concrete category and a congruence on it such that... But as the proof using ranks should go through in ZF I'd (perhaps naively) guess that it would go through in ETCS provided that rank can be defined there. But this Lemma 9.1. gives an an equivalence from material sets to structural sets. Is that enough to define rank on the latter? This direction of the equivalence suggests defining rank of a set as "the smallest rank of a material set that is isomorphic to $$X$", whereas an equivalence in the other direction would suggest "rank of the image". Is either of these enough to ensure that for an object of our category one can find a structural set of those objects with no larger a rank?
If one instead starts with Algebraic Set Theory, then I imagine there is a similar result for NBG (this may be in Mike Shulman unreleased further work on stack semantics, cited in that paper). Then one could ask whether it is sensible to require that a large category is exactly a category internal to the category of classes (this is what the paper under discussion essentially does), or if it is taken to be an elementarily-defined structure, enriched over the category of sets. In the former case, given a material-structural equivalence one might be able to play the same game with ranks. In the latter case, it's not clear how to proceed....
In the latter case, could one prove that such a category is isomorphic/equivalent to a category internal to classes?
(I think that my proof sketch above and the one in Adámek's book tries to cut one corner too many: one _does_ want to add formal identities to the category one builds, and the proof of faithfulness also uses these being members of and for every object)
As far as I can recall, large categories in ETCS foundations are given as fibrations over Set. This is probably in Bénabou's J. Symbolic Logic paper Fibered categories and the foundations of naive category theory.
Well, maybe not. It's not clear skimming the early parts that it's in there. But I'm sure it's been treated somewhere.
I'm also wondering how to formalize the claim one (or more, but then I lack the background to really discuss it) dimension up and whether it holds then. Something like: is every locally small 2-category a quotient of a 2-category that admits a locally faithful functor to (this sentence understood as weakly as you wish)?
Martti Karvonen said:
Zooming out, what seems to be the key to the proof is that one can find for each object a set of objects such that any map factors via something in . Then one would like to define with the same objects and maps to be such factorizations. being locally small and being a set implies that this is collection is a set, and composition in induces a full functor . However, before one gets there one needs to make sure that is indeed a category: one needs to be able to compose such factorizations in a canonical way (so far: by choosing one of the two middle objects as the new middle object in a coherent way), and this seems to require more structure on the sets . In the original proof one sets whereas in what I wrote above I set to be the set of objects with rank at most that of .
I reckon it would be a good idea to axiomatise the structural content of this idea, that is, something that is invariant under equivalence of categories in the abstract (not assuming any particular foundations re: sets), and then prove the theorem. The arguments in the paper and this thread should then show that if large categories are defined using NBGC, or in ZF, then they admit this structure.
Conversely, one could consider what sort of structure a large category has that is the quotient of a concrete one (yes, concrete, not concretisable). Here I would be tempted again to use an equivalence-invariant version of quotient (so something like full, eso + conservative). Does one get the structure I hinted at just above? Are admitting this structure and being the quotient of a concrete category equivalent properties? What about a change of functor to and/or change in structure? I'd be interested in exploring these notions further...
@David Michael Roberts I haven't followed this discussion, but in answer to the question about NBG, no I haven't written out an apg-style reconstruction of it from a category of classes, although that sort of thing is implicit in some of the work on algebraic set theory.
As far as I can recall, large categories in ETCS foundations are given as fibrations over Set. This is probably in Bénabou's J. Symbolic Logic paper Fibered categories and the foundations of naive category theory.
I've now been picking up this pov from chp 8 of Borceux vol 2. It's cool stuff! I'm slightly bothered by the fact that for two internal categories, the category of functors and natural transformations between them is stated to map fully and faithfully into the hom-category of the corresponding fibrations - I'd like this to be essentially surjective as well, so that no new "functors" appear, but I don't see it stated there. Is that true under some reasonable assumptions? Alternatively, is there a neat characterization of those maps of (say locally small) fibrations that should correspond to functors? Similarly, the text by Benabou notes that one shouldn't think of all fibrations as categories over the base (the projection from a product being a non-example), but I didn't quite see a clear answer which fibrations are the relevant ones.
Concretely, if we're working over a fibration of the form for some category , then I think that the relevant factorizations (i.e. the one's where the middle objects have a rank no larger than the endpoints) are definable for the fibration, so I suspect that this could work more generally. Similarly, the class of those families where every object has at most some fixed rank is definable. However, I'm not sure how one would play this game for an arbitrary locally small fibration over , even if our (now taken to be model of ETCS) has rank defined somehow. But I guess that is exactly the problem of finding the structural content of the original argument. Here's a naive attempt (still thinking in terms of rank): for a category , one wants a total preorder on objects such that the down-class of every object is in fact a set, and any morphism factors through something in the downset of the domain and the codomain. Thinking of what structure this induces to should then let one translate it a statement about fibrations, but I'm not yet sure where one would find such preorders without using some tricks within material set theory.
Here I would be tempted again to use an equivalence-invariant version of quotient (so something like full, eso + conservative). Does one get the structure I hinted at just above? Are admitting this structure and being the quotient of a concrete category equivalent properties? What about a change of functor to and/or change in structure? I'd be interested in exploring these notions further...
Yeah this is a fun question, I'll think about it as well. However, I'm not sure you'd want to impose conservativity - at least the functor Kučera constructs is far from it. In fact, given the formally added identities, I think that there are no nontrivial isos in the category built.
Martti Karvonen said:
I'm slightly bothered by the fact that for two internal categories, the category of functors and natural transformations between them is stated to map fully and faithfully into the hom-category of the corresponding fibrations - I'd like this to be essentially surjective as well, so that no new "functors" appear, but I don't see it stated there. Is that true under some reasonable assumptions? Alternatively, is there a neat characterization of those maps of (say locally small) fibrations that should correspond to functors? Similarly, the text by Benabou notes that one shouldn't think of all fibrations as categories over the base (the projection from a product being a non-example), but I didn't quite see a clear answer which fibrations are the relevant ones.
Well :-) :-) Take a look at Marta Bunge's paper Stack completions and Morita equivalence for categories in a topos for part of the story, Stacks and equivalence of indexed categories by Bunge and Pare for some more, and then Strong Stacks and Classifying Spaces by Joyal and Tierney.
However, I'm not sure you'd want to impose conservativity
Oh, of course. Maybe just essential surjectivity, then. But this might be unnecessary generality. Surjectivity on objects is probably reasonable to look at, though.
I'm not yet sure where one would find such preorders without using some tricks within material set theory.
Yeah, but that's a separate problem :-) We have examples from material set theory, and even more, now, than the original paper, since it seems we can do this for categories with a ZF-class of objects, not just an NBG-class. There also might be syntactic or realisability examples that are highly-structured enough to permit the construction
for a category , one wants a total preorder on objects such that the down-class of every object is in fact a set, and any morphism factors through something in the downset of the domain and the codomain.
The second condition is vacuous as at least one of , will do. Instead of a structure on objects, one could think of the argument in terms of a structure on morphisms. I believe the following is sufficient for the argument to go through: having two classes and of morphisms such that (i) any morphism factors as with and , (ii) for any object , the class of -morphisms (-morphisms) with domain (codomain) is a set and (iii) given a morphism we have or (or both). Having such a preorder then gives and by considering maps to/from an object lower in the preorder, but perhaps one could find and through some other means. Roughly: (iii) gives a simple of way of defining an associative composition when morphisms are taken to be such factorizations (plus formal identities), (ii) ensures that the resulting category is concrete and (i) that the functor is full.
(iii) can probably be relaxed somehow, as it's enough to get the desired consequence of it for the rest to go through.
In the examples we have, there's more structure (but it's not strictly needed for the argument). Namely: and are closed under composition and every morphism is in or in (or both). This implies condition (iii) above, and (i) is implied by by requiring in addition that all identity morphisms are in (also true in the examples), so one could work with stronger conditions on and as well.
@Mike Shulman ok, thanks.
A particularly succinct sufficient condition for being the quotient of a concrete category (slightly stronger than (i)-(iii) above) amounts to saying the smallness-condition (ii) above and "any is in ". This behaves quite nicely: such a structure pulls back along small-fibred functors and pushes forward along surjective-on-objects and full small-fibred functors. Thus if our has a such a structure, so will any quotient of a small-fibred concrete category, and the converse is also true as discussed above.
For what it's worth, @Martti Karvonen and I have been thinking a bit more about this. I believe we can now prove Kučera's theorem for an category C internal to a boolean pretopos that models algebraic set theory, as long as C carries wide subcategories L and R with source resp. target small maps, and satisfying three other conditions that always hold when dealing with large categories in ZF or NBG (or really any classical material set theory where there is an ordinal-indexed hierarchy exhausting all the sets). This is the first result of a paper we have in preparation. I will say more about the second result when it is firmed up.
In particular, my complaint at the very start of this thread is now very much alleviated, and the proof is not at all mysterious!