Category Theory
Zulip Server
Archive

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.


Stream: community: general

Topic: Every cat is one of ordinals


view this post on Zulip David Michael Roberts (Jun 04 2020 at 06:18):

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.

view this post on Zulip David Michael Roberts (Jun 04 2020 at 06:18):

I do wonder the extent to which this is true without global choice, or even plain choice..

view this post on Zulip David Michael Roberts (Jun 04 2020 at 06:59):

Only three pages of content, and the proof ends "The details are left to the reader."

view this post on Zulip Jens Hemelaer (Jun 04 2020 at 09:26):

One assumption that is not made explicit seems to be that the category should be locally small.

view this post on Zulip David Michael Roberts (Jun 04 2020 at 10:09):

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:

view this post on Zulip Jens Hemelaer (Jun 04 2020 at 10:29):

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.

view this post on Zulip David Michael Roberts (Jun 04 2020 at 10:44):

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.

view this post on Zulip Peter Arndt (Jun 04 2020 at 12:22):

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.

view this post on Zulip Martti Karvonen (Jun 04 2020 at 16:31):

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.

view this post on Zulip David Michael Roberts (Jun 04 2020 at 22:35):

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?

view this post on Zulip David Michael Roberts (Jun 06 2020 at 02:34):

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?

view this post on Zulip Jens Hemelaer (Jun 06 2020 at 08:36):

I would also like to understand the construction. At the moment, I don't understand the following claim on page 3 of 4:
"F(m)F(m) and G(m)G(m) are sets for every object mm of LL".

This is my reasoning why this is not a set (if KK is locally small but not small):
F(m)F(m) is the set of all morphisms q(A)q(A) for AA an arbitrary morphism of LL with range/codomain mm.
Take f:nmf : n \to m a morphism in KK, with nn arbitrary. Then (f,1m):nm(f,1_m) : n \to m is a morphism in LL with C(f,1m)=mC(f,1_m) = m.
Further, q((f,1m))=(f,1m)q((f,1_m)) = (f,1_m).
So F(m)F(m) should contain at least all morphisms of LL that are of the form (f,1m)(f,1_m), so it contains a proper class.

view this post on Zulip David Michael Roberts (Jun 06 2020 at 09:12):

@Jens Hemelaer I think nfm1mmn\stackrel{f}{\to} m \stackrel{1_m}{\to} m is only a morphism of LL if mnm\leq n. So while arbitrary nn is not ok, I guess there would still be a proper class of such morphisms.

view this post on Zulip David Michael Roberts (Jun 06 2020 at 09:20):

And of course, in the other direction, one would have n1nnfmn \stackrel{1_n}{\to} n \stackrel{f}{\to} m in LL if nm n\leq m.

view this post on Zulip David Michael Roberts (Jun 06 2020 at 09:21):

Aside from all that, I really do wonder what HH is supposed to be. P ⁣:SetopSetP\colon Set^{op} \to Set 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.

view this post on Zulip David Michael Roberts (Jun 06 2020 at 09:23):

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.

view this post on Zulip Jens Hemelaer (Jun 06 2020 at 09:36):

Oh I see, I read C(f,g)mnC(f,g) \leq m \cdot n but it is C(f,g)m,nC(f,g) \leq m,n as you say. That makes more sense.
I think H=PH = P, because it only needs to be faithful and not necessarily injective on objects?

view this post on Zulip Martti Karvonen (Jun 06 2020 at 12:40):

It seems to me that F(m)F(m) is in bijection with morphisms into mm in KK whose domain is at most mm. As KK is locally small, F(m)F(m) is a set. Similarly G(m)G(m) 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.

view this post on Zulip Todd Trimble (Jun 06 2020 at 13:11):

Fun fact: regarding the universe of sets as partially ordered by inclusion, we have an adjunction ab\cup a \leq b iff aPba \leq Pb.

view this post on Zulip Martti Karvonen (Jun 06 2020 at 13:35):

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 KK (whose objects are now just elements of VV), define LL with the same objects, but maps XYX\to Y in LL are given by factorizations XZYX\to Z\to Y of maps in KK with the property that the rank of ZZ is at most that of X,YX,Y. 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 F(X)F(X) as the set of all morphisms of KK into XX whose domain has rank at most that of XX. Given a morphism (f,g) ⁣:XY(f,g)\colon X\to Y in LL, define F(f,g)kF(f,g)k by doing the composition (f,g)(k,id)(f,g)(k,id) in LL and taking the map from the resulting middle object to YY. GG is done similarly with maps out of XX. The rest follows the original proof, i.e. "The details are left to the reader."

view this post on Zulip Martti Karvonen (Jun 06 2020 at 13:39):

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?

view this post on Zulip Martti Karvonen (Jun 06 2020 at 14:08):

Zooming out, what seems to be the key to the proof is that one can find for each object XX a set of objects S(X)S(X) such that any map XYX\to Y factors via something in S(X)S(Y)S(X)\cap S(Y). Then one would like to define LL with the same objects and maps XYX\to Y to be such factorizations. KK being locally small and S(X)S(X) being a set implies that this is collection is a set, and composition in KK induces a full functor LKL\to K. However, before one gets there one needs to make sure that LL 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 S(X)S(X). In the original proof one sets S(m):={kOrdkm}S(m):=\{k\in Ord|k\leq m\} whereas in what I wrote above I set S(X)S(X) to be the set of objects with rank at most that of XX.

view this post on Zulip Martti Karvonen (Jun 06 2020 at 14:40):

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".

view this post on Zulip Martti Karvonen (Jun 06 2020 at 15:02):

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.

view this post on Zulip David Michael Roberts (Jun 07 2020 at 00:15):

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.

view this post on Zulip Martti Karvonen (Jun 07 2020 at 00:23):

Then I think that it should be doable without choice

view this post on Zulip David Michael Roberts (Jun 07 2020 at 01:05):

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....

view this post on Zulip David Michael Roberts (Jun 07 2020 at 01:16):

@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!

view this post on Zulip Martti Karvonen (Jun 07 2020 at 01:46):

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 XX of our category one can find a structural set of those objects with no larger a rank?

view this post on Zulip Martti Karvonen (Jun 07 2020 at 01:48):

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?

view this post on Zulip Martti Karvonen (Jun 07 2020 at 01:51):

(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 LL one builds, and the proof of faithfulness also uses these being members of F(X)F(X) and G(X)G(X) for every object)

view this post on Zulip David Michael Roberts (Jun 07 2020 at 01:57):

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.

view this post on Zulip David Michael Roberts (Jun 07 2020 at 01:59):

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.

view this post on Zulip Martti Karvonen (Jun 07 2020 at 02:14):

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 CatCat (this sentence understood as weakly as you wish)?

view this post on Zulip David Michael Roberts (Jun 07 2020 at 11:02):

Martti Karvonen said:

Zooming out, what seems to be the key to the proof is that one can find for each object XX a set of objects S(X)S(X) such that any map XYX\to Y factors via something in S(X)S(Y)S(X)\cap S(Y). Then one would like to define LL with the same objects and maps XYX\to Y to be such factorizations. KK being locally small and S(X)S(X) being a set implies that this is collection is a set, and composition in KK induces a full functor LKL\to K. However, before one gets there one needs to make sure that LL 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 S(X)S(X). In the original proof one sets S(m):={kOrdkm}S(m):=\{k\in Ord|k\leq m\} whereas in what I wrote above I set S(X)S(X) to be the set of objects with rank at most that of XX.

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.

view this post on Zulip David Michael Roberts (Jun 07 2020 at 11:05):

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 SetSet and/or change in structure? I'd be interested in exploring these notions further...

view this post on Zulip Mike Shulman (Jun 07 2020 at 13:47):

@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.

view this post on Zulip Martti Karvonen (Jun 07 2020 at 15:43):

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 Fam(C)SetFam(C)\to Set for some category CC, 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 SetSet, even if our SetSet (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 CC, 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 Fam(C)SetFam(C)\to Set 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.

view this post on Zulip Martti Karvonen (Jun 07 2020 at 15:48):

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 SetSet 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.

view this post on Zulip David Michael Roberts (Jun 07 2020 at 23:45):

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.

view this post on Zulip David Michael Roberts (Jun 07 2020 at 23:54):

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.

view this post on Zulip David Michael Roberts (Jun 08 2020 at 00:01):

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

view this post on Zulip Martti Karvonen (Jun 08 2020 at 03:57):

for a category CC, 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 (f,id)(f,id), (id,f)(id,f) 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 LL and RR of morphisms such that (i) any morphism factors as rlr\circ l with rRr\in R and lLl\in L, (ii) for any object XX, the class of LL-morphisms (RR-morphisms) with domain (codomain) XX is a set and (iii) given a morphism r2l2r1l1r_2l_2r_1l_1 we have r2l2r1Rr_2l_2r_1\in R or l2r1l1Ll_2r_1l_1\in L (or both). Having such a preorder then gives LL and RR by considering maps to/from an object lower in the preorder, but perhaps one could find LL and RR 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 (r,l)rl(r,l)\mapsto rl is full.

view this post on Zulip Martti Karvonen (Jun 08 2020 at 04:00):

(iii) can probably be relaxed somehow, as it's enough to get the desired consequence of it for the rest to go through.

view this post on Zulip Martti Karvonen (Jun 08 2020 at 15:26):

In the examples we have, there's more structure (but it's not strictly needed for the argument). Namely: LL and RR are closed under composition and every morphism is in LL or in RR (or both). This implies condition (iii) above, and (i) is implied by by requiring in addition that all identity morphisms are in LRL\cap R (also true in the examples), so one could work with stronger conditions on LL and RR as well.

view this post on Zulip David Michael Roberts (Jun 09 2020 at 05:25):

@Mike Shulman ok, thanks.

view this post on Zulip Martti Karvonen (Jun 09 2020 at 15:03):

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 ff is in LRL\cup R". 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 SetSet has a such a structure, so will any quotient of a small-fibred concrete category, and the converse is also true as discussed above.

view this post on Zulip David Michael Roberts (Jul 30 2020 at 07:58):

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.

view this post on Zulip David Michael Roberts (Jul 30 2020 at 08:00):

In particular, my complaint at the very start of this thread is now very much alleviated, and the proof is not at all mysterious!