Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeAug 20th 2011
   • (edited Aug 20th 2011)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI'm confused at [[cocomplete well-pointed topos]]. In the bottom section, it says that the theorem and its corollary fail constructively and gives a weak counterexample. Now, I think that I understand the corollary. Its direct proof uses excluded middle, and the weak counterexample violates it. However, I don't understand: * how the proof of the theorem uses excluded middle, * how the corollary follows from the theorem (with or without excluded middle), * how the weak counterexample violates the theorem. Any help? (Mike?)

   I’m confused at cocomplete well-pointed topos. In the bottom section, it says that the theorem and its corollary fail constructively and gives a weak counterexample.

   Now, I think that I understand the corollary. Its direct proof uses excluded middle, and the weak counterexample violates it. However, I don’t understand:

   • how the proof of the theorem uses excluded middle,
   • how the corollary follows from the theorem (with or without excluded middle),
   • how the weak counterexample violates the theorem.

   Any help? (Mike?)

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeAug 21st 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHmm, it's been a while since I thought about this. First of all, it should be clarified that in the intuitionistic case, we are not talking about models of *classical* ETCS (since intuitionistically, even Set is not such a thing), but models of "IETCS", that is, constructively well-pointed topoi with NNO. Looking at the proof of the theorem, I don't see any use of excluded middle in the first two paragraphs, so it should still be true intuitionistically that a locally small model of IETCS with coproducts indexed by its homsets is equivalent to a full subcategory of Set. But in the third paragraph we find the coproduct $\coprod_{x\colon 1\to x} Z_x$ where $Z_x$ is 1 if $x\in Y$ and 0 otherwise, which looks to me like excluded middle. This argument is what's being used to show that this full subcategory of Set is closed under subobjects; closure under unions doesn't seem to require it. So perhaps the question is that the definition of "Grothendieck universe" requires a bit more thought intuitionistically -- of course intuitionistically we talk about large sets rather than large cardinals, but should a Grothendieck universe be closed under subsets in addition to unions? That is, classically, the replacement axiom implies the separation axiom, but in IZF we assert both separately (and generalize replacement to collection). It seems to me that similarly, an intuitionistic Grothendieck universe should satisfy relativized second-order versions of both replacement and separation, and the latter should mean it's closed under subsets. But we do, I guess, get a weaker version of the theorem intuitionistically, where "either all of Set or a Grothendieck universe" is replaced by something else -- a full subcategory of Set with some properties or other. As to how the corollary follows from the theorem, since the category of sets in some Grothendieck universe does not admit all small coproducts (for instance, not those of the size of the universe), if the conclusion of the theorem holds for a cocomplete topos, it must be all of Set. Finally, the weak counterexample is (according to the intuitionistic version of the theorem) equivalent to a full subcategory of Set. The "inclusion" functor is not the forgetful one from the slice category, but rather $\Pi_{\mathcal{U}}$ (global sections, as in the theorem). This full subcategory is constructively well-pointed, locally small (since Set is), coreflective ($\Pi_{\mathcal{U}}$ is a [[direct image functor]]), hence cocomplete, and in particular admits colimits indexed by its homsets, but is not equivalent to a Grothendieck universe (since it is large) nor, in general, to Set itself (since $\mathcal{U}$ need not be $\top$).

   Hmm, it’s been a while since I thought about this. First of all, it should be clarified that in the intuitionistic case, we are not talking about models of classical ETCS (since intuitionistically, even Set is not such a thing), but models of “IETCS”, that is, constructively well-pointed topoi with NNO.

   Looking at the proof of the theorem, I don’t see any use of excluded middle in the first two paragraphs, so it should still be true intuitionistically that a locally small model of IETCS with coproducts indexed by its homsets is equivalent to a full subcategory of Set. But in the third paragraph we find the coproduct $\coprod_{x\colon 1\to x} Z_x$ where $Z_x$ is 1 if $x\in Y$ and 0 otherwise, which looks to me like excluded middle. This argument is what’s being used to show that this full subcategory of Set is closed under subobjects; closure under unions doesn’t seem to require it.

   So perhaps the question is that the definition of “Grothendieck universe” requires a bit more thought intuitionistically – of course intuitionistically we talk about large sets rather than large cardinals, but should a Grothendieck universe be closed under subsets in addition to unions? That is, classically, the replacement axiom implies the separation axiom, but in IZF we assert both separately (and generalize replacement to collection). It seems to me that similarly, an intuitionistic Grothendieck universe should satisfy relativized second-order versions of both replacement and separation, and the latter should mean it’s closed under subsets. But we do, I guess, get a weaker version of the theorem intuitionistically, where “either all of Set or a Grothendieck universe” is replaced by something else – a full subcategory of Set with some properties or other.

   As to how the corollary follows from the theorem, since the category of sets in some Grothendieck universe does not admit all small coproducts (for instance, not those of the size of the universe), if the conclusion of the theorem holds for a cocomplete topos, it must be all of Set.

   Finally, the weak counterexample is (according to the intuitionistic version of the theorem) equivalent to a full subcategory of Set. The “inclusion” functor is not the forgetful one from the slice category, but rather $\Pi_{\mathcal{U}}$ (global sections, as in the theorem). This full subcategory is constructively well-pointed, locally small (since Set is), coreflective ($\Pi_{\mathcal{U}}$ is a direct image functor), hence cocomplete, and in particular admits colimits indexed by its homsets, but is not equivalent to a Grothendieck universe (since it is large) nor, in general, to Set itself (since $\mathcal{U}$ need not be $\top$).

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeAug 22nd 2011
   • (edited Aug 22nd 2011)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>it should be clarified Yes, I took that for granted. In fact, instead of $ETCS$, all we need is the elementary theory of a well-pointed topos; if I'm not mistaken, everything else comes from the infinite coproducts. (I don't see anything else used.) >which looks to me like excluded middle Not to me. This just says that $Z_x$ is the truth value of $x \in Y$. Ah, but now I see it: without excluded middle, how do we know that every truth value is in this category? We don't! And with $Set/U$, that is kind of the point. >should a Grothendieck universe be closed under subsets Arguably, it should only be closed under *detachable* subsets. For one thing, we can actually prove that above. But also, this is the property of lots of large (collections of) cardinals that people use in constructive mathematics; for example, people often use finite or K-finite sets, rarely S-finite sets. (Without choice, we should also specify closure under certain quotient sets. In this case, we can prove closure under quotients by detachable equivalence relations.) I didn't think very much about this before, since $Set/U$, the category of those sets $X$ such that $U$ is true if $X$ is inhabited, *is* closed under subsets. (Well, but see below.) So I assumed that the problem must be with power sets. >The "inclusion" functor is not the forgetful one from the slice category, I think that this is what I was missing! As I said above, $Set/U$ is the category of sets that are inhabited only if $U$ is true, but it's also the category of those sets of the form $Fun(U,X)$. And this is the way we need to think of it to have the inclusion functor preserve the terminal object. (I think that we've discussed this before, but I forgot the lesson.) This collection of sets, of course, might *not* be closed under subsets. >As to how the corollary follows from the theorem, Of course; I'm in the joke where the mathematician says, after a day's thinking, "Yes, it *is* obvious.". >a full subcategory of Set with some properties or other. Right, and whether you call that thing a Grothendieck universe or not is less important. One thing that *is* important, to avoid the corollary, is that such a category might be (co)complete without being $Set$. Come to think of it, even classically, might we need the axiom of choice to know that a Grothendieck universe (defined as a full subcategory of $Set$ closed under certain operations) must be small if it's not all of $Set$? (without going through the direct proof of the corollary).

   it should be clarified

   Yes, I took that for granted. In fact, instead of $ETCS$, all we need is the elementary theory of a well-pointed topos; if I’m not mistaken, everything else comes from the infinite coproducts. (I don’t see anything else used.)

   which looks to me like excluded middle

   Not to me. This just says that $Z_x$ is the truth value of $x \in Y$. Ah, but now I see it: without excluded middle, how do we know that every truth value is in this category? We don’t! And with $Set/U$, that is kind of the point.

   should a Grothendieck universe be closed under subsets

   Arguably, it should only be closed under detachable subsets. For one thing, we can actually prove that above. But also, this is the property of lots of large (collections of) cardinals that people use in constructive mathematics; for example, people often use finite or K-finite sets, rarely S-finite sets. (Without choice, we should also specify closure under certain quotient sets. In this case, we can prove closure under quotients by detachable equivalence relations.)

   I didn’t think very much about this before, since $Set/U$, the category of those sets $X$ such that $U$ is true if $X$ is inhabited, is closed under subsets. (Well, but see below.) So I assumed that the problem must be with power sets.

   The “inclusion” functor is not the forgetful one from the slice category,

   I think that this is what I was missing! As I said above, $Set/U$ is the category of sets that are inhabited only if $U$ is true, but it’s also the category of those sets of the form $Fun(U,X)$. And this is the way we need to think of it to have the inclusion functor preserve the terminal object. (I think that we’ve discussed this before, but I forgot the lesson.) This collection of sets, of course, might not be closed under subsets.

   As to how the corollary follows from the theorem,

   Of course; I’m in the joke where the mathematician says, after a day’s thinking, “Yes, it is obvious.”.

   a full subcategory of Set with some properties or other.

   Right, and whether you call that thing a Grothendieck universe or not is less important. One thing that is important, to avoid the corollary, is that such a category might be (co)complete without being $Set$. Come to think of it, even classically, might we need the axiom of choice to know that a Grothendieck universe (defined as a full subcategory of $Set$ closed under certain operations) must be small if it’s not all of $Set$? (without going through the direct proof of the corollary).

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeAug 26th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI have further expanded the discussion of the intuitionistic case on the page [[cocomplete well-pointed topos]]. It does seem that we need at least total ordering of cardinal numbers.

   I have further expanded the discussion of the intuitionistic case on the page cocomplete well-pointed topos. It does seem that we need at least total ordering of cardinal numbers.