[Note from moderator: This item is a digest of a number posts on this subject, and I assume is the last of the thread. ]
Ha ha, you are right!?? G&V didn't make a mistake after all.?? Let me summarize.
Of course, I fully agree with your summary! What a relief that we have converged at an agreement! Thomas ---- From: Paul Blain Levy <P.B.Levy@cs.bham.ac.uk> Date: Sat, 6 Jan 2018 15:59:49 +0000 Ha ha, you are right! G&V didn't make a mistake after all. Let me summarize. Some authors say that a "function from A to B" is a subset of A*B that is functional. [Option 1] Other authors say that a "function from A to B" is a triple (A,B,R) where R is a subset of A*B that is functional. [Option 2] Some authors say that a category is a set of objects and an indexed famly of homsets. [Option 1'] Other authors say that a category is a set of objects and a set of morphisms, with source and target functions. [Option 2'] Option 2' implies that homsets are pairwise disjoint. Therefore those who follow Option 2' and Option 1 are forced to say, when defining U-Set, that a morphism is a triple (A,B,f), where A and B are U-sets and f is a function from A to B. But this means that we have to repeatedly distinguish between a function and the corresponding morphism, and between the set of functions B^A and U-Set(A,B). To avoid this trouble, those who follow Option 2' may prefer Option 2. (On the other hand, those who follow Option 1' are at liberty to follow Option 1 without any problem.) As you guys have cleverly worked out, G&V follow Option 2, perhaps for this reason. A functor C --> D is for them a triple (C,D,...). A natural transformation F --> G is for them a triple (F,G,...). This is incorporated into the definition of a functor category [C,D]. Therefore, for a category C, if C is in the universe U, it doesn't follow that [C,U-Set] satisfies the properties (C1) and (C2). Had they chosen Option 1, they would not have this problem. They would then undoubtedly have defined "x is U-small" to mean "x is an element of U", and "U-category" to mean "category satisfying (C1) and (C2)". Which is what I called "U-included" in my original message. Thank you for solving this mystery! Paul ---- Date: Sat, 6 Jan 2018 11:27:41 +0100 From: streicher@mathematik.tu-darmstadt.de
We are also ouside U in the first case since a functional relation is a subset of C x U, and as such there is no way to prove it is a U-set, only in bijection with a U-set when C is a U-set.
But axiom of replacement allows you to do precisely that! A set-indexed family of sets is a set and not a class, eg P^n(N) for in N. This is a set and not a class! Thomas --- From: Eduardo Julio Dubuc <edubuc@dm.uba.ar> Date: Sat, 6 Jan 2018 00:44:10 -0300 On 1/5/18 22:05, Thomas Streicher wrote:
Dear Paul,
in discussion between Eduardo, R.Williamson and me it appeared that the answer to the problem might be the following. A function from Ob(C) to U may either be considered as a functional relation F from Ob(C) to U or a triple (Ob(C),U,F) in which latter case we are outside U.
We are also ouside U in the first case since a functional relation is a subset of C x U, and as such there is no way to prove it is a U-set, only in bijection with a U-set when C is a U-set.
This is an argument why a contravariant functor from C^op to U cannot be considered as a set in U but only as a set isomorphic to a set in U.
This might explain why in SGA4 they take pains to define U-category the way they did and not simply as a category whose hom-sets are elements of U.
This, BTW would also be the case when we use a type theoretic account. If C is a category in a universe U then functors from C to U would not live inside U but in a next universe U' of which U is an element. Thomas
PS This wasn't immediate to me since I would have considered a functor from C to U as formulated in terms of functional relations.
That's what SGA4 does !!, F \subset C x U
It's not too reassuring too see how such bureaucratic details of foundations make a quite cofusing difference.
bureaucratic detais are the whole difference between being formally rigorous or naive. Either you play the game or not. best e. ---- From: Eduardo Julio Dubuc <edubuc@dm.uba.ar> Date: Sat, 6 Jan 2018 00:27:51 -0300 Some comments intercalated: On 1/5/18 21:49, Thomas Streicher wrote:
Dear William and Eduardo,
I think that the discrepancy that Eduardo pointed out between this argument and mine is that I believe we actually need to refer to U somewhere to formalise the above, and then we will not be able to show that we have a subset of U.
For example, just to be able to define Hom(F,G) in the setup in SGA4, we first need to have defined F and G. And to define a functor from C to D, I believe that it is necessary to refer to the set of objects of D. For instance, we might think of the object part of the definition of a functor C -> D as a map of sets from Ob(C) to Ob(D). The latter is U when D is U-Ens. No matter how one tries to get around it, one must surely refer to Ob(D) somewhere.
And then, since we have referred to U which is not an element of U, how can we conclude that we have something in U? As far as I can see, we cannot: all four axioms (U1) - (U4) involve only sets which we already know are in U.
This is not a question of "having referred to U". An Ob(C)-indexed family of elements of U is a functional relation F from Ob(C) to U
is not, it is only bijective, functional relation ~ Ob(C)-indexed family of elements of U but functional relation not = Ob(C)-indexed family of elements of U
and such an F is an element of U as easily follows from the axioms for a Grothendieck universe. What you say, William, only applies if a function from Ob(F) to U is a triple (Ob(F),U,F) with F as above.
Now it comes the fact that you must have F "rigorously formalized as a set" You have F \subset Ob(C) x U as a functional relation, is this the same that a triple (Ob(C),U,F) ?, probably This subset is in bijection with a U-set if C is a U-set, but is not a U-set. Either you are rigorous or not, if you are, F IS NOT in U. The whole point of SGA in the foundations of category theory with Zermelo-Frankel + the axiom of Universes was to be formally rigorous.
So it really hinges on what you consider as a function!
No !, what you consider as a function does not admit different interpretations, it is a well defined notion in axiomatic set theory.
Of course, third projection establishes an iso between these two different notions of "function from Ob(C) to U".
In axiomatic set theory there is only one notion of function from a set to another set.
There is no question at all that if one relaxes to asking for an isomorphism, then we get something in U, and for us today it is of course very natural to think that way by default.
That's we all do as practitioners of category theory based in naive set theory with universes.
But it does
not seem so strange to me that for Grothendieck, who was deeply steeped in the Bourbaki tradition, and probably Verdier as well, things may have been the other way around: that they would have been quite sensitive to the set-theoretic issues at stake and assumed more sensitivity in this regard of their seminar participants than we would today.
I repeat, there is no place to more or less sensitivity.
So you really think that G&V had the second notion of function in mind and, therefore, saw a need for "up to iso".
There is only one notion of function in axiomatic set theory !!
Could well be... though I am hesitant to believe that G&V were so formalist.
They were, that is the whole point in a rigorous formal foundation.
Best, Thomas
Very best Eduardo --- From: Eduardo Julio Dubuc <edubuc@dm.uba.ar> Date: Fri, 5 Jan 2018 23:35:29 -0300 SGA4 is right and Richard explanation shows why, some comments to this words of Richard: On 1/5/18 19:23, Richard Williamson wrote:
There is no question at all that if one relaxes to asking for an isomorphism, then we get something in U, and for us today it is of course very natural to think that way by default. But it does not seem so strange to me that for Grothendieck, who was deeply steeped in the Bourbaki tradition, and probably Verdier as well, things may have been the other way around: that they would have been quite sensitive to the set-theoretic issues at stake and assumed more sensitivity in this regard of their seminar participants than we would today.
Well, there are no half measures, you are either formal (in a rigourus way) or you are naive, is not a question of sensitivity. best e. --- Date: Sat, 6 Jan 2018 02:05:43 +0100 From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de> Dear Paul, in discussion between Eduardo, R.Williamson and me it appeared that the answer to the problem might be the following. A function from Ob(C) to U may either be considered as a functional relation F from Ob(C) to U or a triple (Ob(C),U,F) in which latter case we are outside U. This is an argument why a contravariant functor from C^op to U cannot be considered as a set in U but only as a set isomorphic to a set in U. This might explain why in SGA4 they take pains to define U-category the way they did and not simply as a category whose hom-sets are elements of U. This, BTW would also be the case when we use a type theoretic account. If C is a category in a universe U then functors from C to U would not live inside U but in a next universe U' of which U is an element. Thomas PS This wasn't immediate to me since I would have considered a functor from C to U as formulated in terms of functional relations. It's not too reassuring too see how such bureaucratic details of foundations make a quite cofusing difference. ---- Date: Sat, 6 Jan 2018 01:49:48 +0100 From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de> Dear William and Eduardo,
I think that the discrepancy that Eduardo pointed out between this argument and mine is that I believe we actually need to refer to U somewhere to formalise the above, and then we will not be able to show that we have a subset of U.
For example, just to be able to define Hom(F,G) in the setup in SGA4, we first need to have defined F and G. And to define a functor from C to D, I believe that it is necessary to refer to the set of objects of D. For instance, we might think of the object part of the definition of a functor C -> D as a map of sets from Ob(C) to Ob(D). The latter is U when D is U-Ens. No matter how one tries to get around it, one must surely refer to Ob(D) somewhere.
And then, since we have referred to U which is not an element of U, how can we conclude that we have something in U? As far as I can see, we cannot: all four axioms (U1) - (U4) involve only sets which we already know are in U.
This is not a question of "having referred to U". An Ob(C)-indexed family of elements of U is a functional relation F from Ob(C) to U and such an F is an element of U as easily follows from the axioms for a Grothendieck universe. What you say, William, only applies if a function from Ob(F) to U is a triple (Ob(F),U,F) with F as above. So it really hinges on what you consider as a function! Of course, third projection establishes an iso between these two different notions of "function from Ob(C) to U".
There is no question at all that if one relaxes to asking for an isomorphism, then we get something in U, and for us today it is of course very natural to think that way by default. But it does not seem so strange to me that for Grothendieck, who was deeply steeped in the Bourbaki tradition, and probably Verdier as well, things may have been the other way around: that they would have been quite sensitive to the set-theoretic issues at stake and assumed more sensitivity in this regard of their seminar participants than we would today.
So you really think that G&V had the second notion of function in mind and, therefore, saw a need for "up to iso". Could well be... though I am hesitant to believe that G&V were so formalist. Best, Thomas ---- Date: Fri, 5 Jan 2018 23:23:44 +0100 From: Richard Williamson <rwilliamson62@gmail.com> Dear Eduardo and Thomas, Thank you for your thoughts. I'll just comment on the following argument given by Thomas.
But if you have presheaves F and G over C taking values in U then Hom(F,G) is a subset of \prod_{I \in Ob(C)} G(I)^{F(I)} which is a set in U. The reason is that Ob(C) is an element of U and I \mapsto G(I)^{F(I)} is a function from Ob(C) to U. Then by replacement the image of this map is an element of U (condition (v) of MacLane's definition of a universe). And finally U is closed under dependent products. Thus Hom(F,G) is an element of U.
I think that the discrepancy that Eduardo pointed out between this argument and mine is that I believe we actually need to refer to U somewhere to formalise the above, and then we will not be able to show that we have a subset of U. For example, just to be able to define Hom(F,G) in the setup in SGA4, we first need to have defined F and G. And to define a functor from C to D, I believe that it is necessary to refer to the set of objects of D. For instance, we might think of the object part of the definition of a functor C -> D as a map of sets from Ob(C) to Ob(D). The latter is U when D is U-Ens. No matter how one tries to get around it, one must surely refer to Ob(D) somewhere. And then, since we have referred to U which is not an element of U, how can we conclude that we have something in U? As far as I can see, we cannot: all four axioms (U1) - (U4) involve only sets which we already know are in U. There is no question at all that if one relaxes to asking for an isomorphism, then we get something in U, and for us today it is of course very natural to think that way by default. But it does not seem so strange to me that for Grothendieck, who was deeply steeped in the Bourbaki tradition, and probably Verdier as well, things may have been the other way around: that they would have been quite sensitive to the set-theoretic issues at stake and assumed more sensitivity in this regard of their seminar participants than we would today. Best wishes, Richard --- From: "Eduardo J. Dubuc" <edubuc@dm.uba.ar> Date: Fri, 5 Jan 2018 16:58:16 -0300 On 05/01/18 16:02, Thomas Streicher wrote:
Dear Richard,
what you write is possibly the reason why G. and V. thought their claim as obvious.
But if you have presheaves F and G over C taking values in U
Richard says: Certainly one needs to involve U to be able to define the Hom sets of Func(C, U-Ens), thus Func(C, U-Ens)(F, G) can not be in U. Thomas says: Func(C, U-Ens)(F, G) \subset \prod_{I \in Ob(C)} G(I)^{F(I)} and then argues that this implies that Func(C, U-Ens)(F, G) is in U. then, both can not be wright.
then Hom(F,G) is a subset of \prod_{I \in Ob(C)} G(I)^{F(I)} which is a set in U. The reason is that Ob(C) is an element of U and I \mapsto G(I)^{F(I)} is a function from Ob(C) to U. Then by replacement the image of this map is an element of U (condition (v) of MacLane's definition of a universe). And finally U is closed under dependent products. Thus Hom(F,G) is an element of U.
But, of course, you need replacement and maybe Bourbaki set theory doesn't have it?? Many people only vaguely familiar with set theory are not fully aware of replacement.
But I have looked up SGA4 and condition (U4) for a G-universe does the job!
It seems to me that Maclane and SGA4 axioms of a Universe are if not the same at least fully equivalent. Mac lane says that the axioms he write are Grothendieck axioms of universe, and he neither "made mistakes", especially in matters of logic and set theory. :=).
So it's really mysterious what G&V might have had in mind.
If you consider that there is no error in SGA4, it is not mysterious. If you are sloppy as in naive category theory with universes, and you identify U-small with U-set, you live happily
Thomas
---- Date: Fri, 5 Jan 2018 20:03:40 +0100 From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de> Dear Richard, what you write is possibly the reason why G. and V. thought their claim as obvious. But if you have presheaves F and G over C taking values in U then Hom(F,G) is a subset of \prod_{I \in Ob(C)} G(I)^{F(I)} which is a set in U. The reason is that Ob(C) is an element of U and I \mapsto G(I)^{F(I)} is a function from Ob(C) to U. Then by replacement the image of this map is an element of U (condition (v) of MacLane's definition of a universe). And finally U is closed under dependent products. Thus Hom(F,G) is an element of U. But, of course, you need replacement and maybe Bourbaki set theory doesn't have it?? Many people only vaguely familiar with set theory are not fully aware of replacement. But I have looked up SGA4 and condition (U4) for a G-universe does the job! So it's really mysterious what G&V might have had in mind. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (1)
-
streicher@mathematik.tu-darmstadt.de