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.
David Michael Roberts (Feb 23 2022 at 03:13):Skepticism, in the sense that he used at some point étale cohomology, and the citation chain went back to SGA4, where universes are used.
John Baez (Feb 23 2022 at 03:15):What? Was there really "skepticism" about Wiles' proof of FLT because it used the axiom of universes? Did anyone come out and say they doubted it for that reason?
John Baez (Feb 23 2022 at 03:15):I'd love to see a quote like that.
John Baez (Feb 23 2022 at 04:04):I know McLarty and others spent a lot of time trying to eliminate the use of universes, but I always thought that was just out of interest in seeing if it could be done, not to allay actual doubts.
David Michael Roberts (Feb 23 2022 at 09:52):Not by experts, perhaps, but you got things like this: https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof, where the "proof" that universes wasn't needed is that Brian Conrad says
For etale cohomology all of that universe stuff is entirely irrelevant. I say this not as an "article of faith", but because I've read all of the proofs of the theorems of etale cohomology.
So do we have to believe this guy who says he read all the references from Wiles' papers back to SGA4 and figured out how to eliminate universes, but never wrote up his argument? This is not just my take, but here's Ekedahl, responding
I completely agree with BCnrd opinions here but as far as I know there is no published complete proof of the relevant results that bypasses SGA IV so in that sense it is not an established fact.
There is mention on that post that Manin once asked publicly about whether universes could be eliminated from the proof of the Weil conjectures by Deligne, so perhaps that's another data point
Zhen Lin Low (Feb 23 2022 at 11:12):Not to mention Brian Conrad's heuristic for rejecting universes hinges on being able to work around the impredicativity inherent to category-theoretic universal properties:
The 2nd issue is univ. mapping properties on "entire category" (your comment about "whole categories of sheaves"). That's an issue for category theory in general, not just SGA; handled as for flatness against "all" mods over a ring.
Even I as a category theorist agree that this is an issue that needs to be taken more seriously by category theorists and advocates of category theory in general – with or without universes. Not for nothing did I make it the subject of my first paper. So I feel I understand where the sceptics (of category theory!) are coming from.
Jens Hemelaer (Feb 23 2022 at 12:14):Am I correct that the axiom of universes is not just independent of ZFC, but that it might even be false?
This is something that does not happen with older approaches to universes, such as NBG set theory. The drawback of NBG set theory is that you only have two universes (a universe of sets and a universe of classes), but it seems that the construction can be iterated to get more universes. Here is a relevant MathOverflow question by @Mike Shulman: https://mathoverflow.net/questions/51257/
David Michael Roberts (Feb 23 2022 at 13:05):@Jens Hemelaer if you can the axiom of universes is false, then you have just disproved some large cardinal axioms, and not very big ones at that. I really don't think you can have "independent of ZFC" and false at the same time.
Reid Barton (Feb 23 2022 at 13:06):The discussion about universes is interesting to be sure, but quite far removed from the original topic--maybe a moderator could separate it out?
David Michael Roberts (Feb 23 2022 at 13:12):@Reid Barton quite right.
Nathanael Arkor (Feb 23 2022 at 13:20):Didn't know exactly where to split, but hopefully this helps a little :)
Jens Hemelaer (Feb 23 2022 at 14:01):David Michael Roberts said:
Jens Hemelaer if you can the axiom of universes is false, then you have just disproved some large cardinal axioms, and not very big ones at that. I really don't think you can have "independent of ZFC" and false at the same time.
I agree that it can not be false and independent at the same time, but I believe it is not known which of the two it is. Whereas for NBG set theory it is known that it is consistent if and only if ZFC is consistent.
Graham Manuell (Feb 23 2022 at 15:22):Universes can be used to prove the consistency of ZFC, so this is a clearly a different situation from NBG. But I think saying we don't know if universes are inconsistent or not, while true, is overstating the case since we don't know that ZFC or PA are consistent either. I don't think anyone seriously thinks adding universes makes things inconsistent here.
Zhen Lin Low (Feb 23 2022 at 15:48):It does seem to me that the objection is not probably not something like "I believe ZFC is consistent but large cardinals are not" but rather "I never needed universes in my work before, why do you?" – that is, it's an objection of parsimony. And maybe some maximalists also object on the grounds that the category of "all sets" should be literally that and not secretly replaced with "all sets in U".
Jens Hemelaer (Feb 23 2022 at 16:47):Yes, ideally there would be some theorem that says that any classical statement without universes (i.e. about "small things") is provable in ZFC+universes if and only if it is provably in ZFC. This would be very practical, for example it would eliminate the discussion about whether or not universes are needed to prove FLT (without having to look at the proof of FLT).
However, as long as we don't even know that ZFC+universes is equiconsistent with ZFC, we can't hope for a theorem like this.
Mike Shulman (Feb 23 2022 at 16:48):That would be nice, but unfortunately, ZFC+U proves Con(ZFC) while ZFC doesn't (assuming it's consistent), and Con(ZFC) is a statement purely about natural numbers, which are pretty "small".
Mike Shulman (Feb 23 2022 at 16:49):Also, I think the fact that ZFC+U proves Con(ZFC) means it can't be equiconsistent with ZFC unless they are both inconsistent.
Jens Hemelaer (Feb 23 2022 at 16:58):Ah yes, this shows that the theorem can't exist. But the theorem does exist if you use NBG set theory rather than universes. So I'm a bit confused as to why universes are used more often. Maybe there is some advantage of universes over NBG set theory that I'm missing.
Graham Manuell (Feb 23 2022 at 16:59):Mike Shulman said:
Also, I think the fact that ZFC+U proves Con(ZFC) means it can't be equiconsistent with ZFC unless they are both inconsistent.
I almost said something similar, but is this right? I thought equiconsistent just meant the one is consistent iff the other one is. If they are both consistent then this would be true. Of course, we couldn't prove it.
Mike Shulman (Feb 23 2022 at 17:07):Yes, if they are both absolutely consistent (insofar as that means anything) then they would also be equiconsistent.
Mike Shulman (Feb 23 2022 at 17:07):@Jens Hemelaer There are some things you can do with universes that you can't do with NBG, like form the functor category between two large categories.
Mike Shulman (Feb 23 2022 at 17:08):Almost always this sort of stuff can be avoided if you work at it, but sometimes it requires clever tricks or unnatural encoding, while universes are easy to use and think about.
Jens Hemelaer (Feb 23 2022 at 17:24):Thanks!
John Baez (Feb 23 2022 at 18:15):I think part of the point is that the axiom of universes is so easy and natural to use if you're already using ZFC, while using NBG requires actually learning new stuff. I typically work with ZFC in the back of my mind, and if I accidentally say something like "the category of all categories" I whip out the axiom of universes to save my butt.
Jens Hemelaer (Feb 23 2022 at 18:34):I'm convinced that we need more than two universes, just maybe not as many as provided by the axiom of universes. Maybe countably many would be enough? Then the category of sets is a class, the category of classes is a 2-class, the category of 2-classes is a 3-class, and so on.
Jon Sterling (Feb 23 2022 at 18:37):The thing is that classes are fundamentally different from sets --- they are not closed under function spaces, for instance --- so I would not expect a notion of 2-class and 3-class to be as useful as it sounds. This is where universes play an important role --- they say, roughly, that we should think about sets rather than classes.
Jon Sterling (Feb 23 2022 at 18:38):I don't personally know what I think about universes. There is something very unattractive about everything being stratified in a universe, because I feel that part of what is objective about category theory is its ability to speak about "all" things (even if the need to speak about "all" things is also a weakness).
Jon Sterling (Feb 23 2022 at 18:38):But I do not yet know how to do my work without universes. I wouldn't mind it if I figured out how.
Jens Hemelaer (Feb 23 2022 at 18:41):Jonathan Sterling said:
The thing is that classes are fundamentally different from sets --- they are not closed under function spaces, for instance --- so I would not expect a notion of 2-class and 3-class to succeed. This is where universes play an important role --- they say, roughly, that we should think about sets rather than classes.
Ok, thanks! That is probably the point where my naive construction fails.
Jon Sterling (Feb 23 2022 at 18:43):Btw Lawvere seems to take a different position on the matter --- I think that Lawvere believes that the failure of cartesian closure for classes is more of a failure of imagination, and we should just assert that classes do whatever we want them to do. I guess Lawvere's view is not so different from the universe perspective.
The difficulty for me is that I am torn between the fibrational perspective, where I use relative category theory to deal with the relationship between "large" and "small", and the fact that it remains difficult even to develop fibered category theory without a pre-existing notion of large and small. I think these things could be dealt with in principle, but I do not yet have the skills.
Graham Manuell (Feb 23 2022 at 19:02):Jonathan Sterling said:
I don't personally know what I think about universes. There is something very unattractive about everything being stratified in a universe, because I feel that part of what is objective about category theory is its ability to speak about "all" things (even if the need to speak about "all" things is also a weakness).
I feel similarly. Often introducing universes 'solves' the size issues, but leads to constructions which are sensitive to exactly what level of the hierarchy they are done at. And if you want the constructions to be invariant with respect to this level in a nice way or whatever, you then end up needing to solve the same things you would have needed to if you just dealt with the size issues in the first place.
Mike Shulman (Feb 23 2022 at 21:36):Graham Manuell said:
Often introducing universes 'solves' the size issues, but leads to constructions which are sensitive to exactly what level of the hierarchy they are done at. And if you want the constructions to be invariant with respect to this level in a nice way or whatever, you then end up needing to solve the same things you would have needed to if you just dealt with the size issues in the first place.
This is something I've thought about a fair amount. One way to deal with the sensitivity to level is to use something like Feferman set theory or a reflection principle, where the "smallness" cutoff doesn't have any special properties.
Zhen Lin Low (Feb 23 2022 at 22:24):Just to clarify for Jens, the collection of all classes (as conventionally understood in the ontology of NBG or MK) is not a "universe" in the same way that the collection of all sets is. If we write V for the collection of all sets then, roughly speaking, the collection of all classes is P(V), and though V is an element of P(V), P(V) is not, and we want universes to be closed under P.
Zhen Lin Low (Feb 23 2022 at 22:42):@Mike Shulman I seem to remember that you once wrote about an ontology where "small" things behave like sets in classical set theory but "large" things behave like types in homotopy type theory, or something like that. That sounded quite interesting to me, but I don't remember the details now. Did you develop it further?
Mike Shulman (Feb 23 2022 at 22:56):@Zhen Lin Low You may be thinking of this. I haven't finished writing the paper yet, but it's close to the top of my stack.
Zhen Lin Low (Feb 23 2022 at 23:05):I don't think I've seen those slides before – at least, it's more detailed than what I remembered! I'm glad to hear it's being developed.
Jon Sterling (Feb 24 2022 at 07:46):@Mike Shulman This discussion also reminds me of a suggestion of Hamkins --- which is that rather than having simply a hierarchy of grothendieck universes, you want their inclusions to be elementary embeddings. I think (but am not sure) that this corresponds to a hierarchy linked by logical functors (??). Have you thought about such an arrangement and whether it helps with the problems we are discussing?
Zhen Lin Low (Feb 24 2022 at 10:19):I think, despite the name, logical functors are incomparable to elementary embeddings. It is easy to check that the category of sets in is a elementary topos for every limit ordinal . Furthermore if are limit ordinals then the corresponding categories of sets embed logically. But is not always (maybe even rarely??) an elementary substructure of .
Zhen Lin Low (Feb 24 2022 at 10:21):Conversely (?) I think it is possible to have elementary substructures of that correspond to subcategories that are not logically embedded.
Mike Shulman (Feb 24 2022 at 14:52):@Jonathan Sterling Yes, Feferman set theory goes more or less in same direction as using elementary embeddings between universes.
Mike Shulman (Feb 24 2022 at 14:55):It's definitely true that not every logical functor is an elementary embedding. One reason is that general logical functor only preserves the truth of statements, while an elementary embedding preserves and reflects them. A conservative logical functor also reflects truth, so it is closer to an EE. The second reason I can think of is that logical functors deal only with bounded statements, while EEs deal with arbitrary ones. That makes me think that an elementary embedding is strictly stronger than a conservative logical functor. @Zhen Lin Low , can you think of an example of the last sort you suggested, an elementary substructure that is not a logical functor?
Zhen Lin Low (Feb 24 2022 at 15:00):I was thinking it would be possible to have the substructure disagree on what powersets are… but maybe that doesn’t happen if you have an elementary embedding rather than a mere elementary equivalence.
Mike Shulman (Feb 24 2022 at 15:17):I would think that " is the powerset of " is a statement whose truth would have to be preserved by the embedding.
Jon Sterling (Feb 25 2022 at 07:51):Thanks @Zhen Lin Low and @Mike Shulman for the discussion!