Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorsherman
   • CommentTimeSep 30th 2016
   • PermaLink
   Author: sherman
   Format: MarkdownItexThe [(0,1)-category page](https://ncatlab.org/nlab/show/%280%2C1%29-category) says that a (0,1)-category "with the structure of a Grothendieck topos" is a locale, and a (0,1)-category "with the structure of an elementary topos" is a (complete?) Heyting algebra. I am trying to understand the formal content of these statements. By the Giraud characterization of Grothendieck toposes, I could believe that (0,1)-categories which happen to be "Giraud toposes" (i.e., Grothendieck toposes) are locales. Running through [the Giraud axioms](https://ncatlab.org/nlab/show/Grothendieck+topos#Giraud), we have: 1. "a locally small category with a small generating set" - should be true for any (0,1)-category 2. "with all finite limits" - this means all finite meets for a (0,1)-category, which locales have 3. "with all small coproducts, which are disjoint, and pullback stable" - for a (0,1) category, all small coproducts are small/infinitary disjunctions, and pullback stability corresponds to the "frame distributivity" rule which holds for locales, which says that binary meets distribute over joins. I'm not sure about the "disjoint" condition, though. 4. "where all congruences have effective quotient objects, which are also pullback-stable." I don't understand. But it does not seem that a (0,1)-category which is also an elementary topos is a complete Heyting algebra. The issue is that there is no subobject classifier. One reasons that the subobject classifier must be the terminal object of the cHa (it would be necessary to have a map into the subobject classifier from any object), but then since the pullback of every iso is an iso, every object must be the terminal object (Top), so the category is made only of terminal objects. Is it in fact the case that a (0,1)-category which is a Grothendieck topos is a locale? And is there any *formal* way to view complete Heyting algebras as decategorified elementary toposes?

   The (0,1)-category page says that a (0,1)-category “with the structure of a Grothendieck topos” is a locale, and a (0,1)-category “with the structure of an elementary topos” is a (complete?) Heyting algebra.

   I am trying to understand the formal content of these statements. By the Giraud characterization of Grothendieck toposes, I could believe that (0,1)-categories which happen to be “Giraud toposes” (i.e., Grothendieck toposes) are locales. Running through the Giraud axioms, we have:

   1. “a locally small category with a small generating set” - should be true for any (0,1)-category
   2. “with all finite limits” - this means all finite meets for a (0,1)-category, which locales have
   3. “with all small coproducts, which are disjoint, and pullback stable” - for a (0,1) category, all small coproducts are small/infinitary disjunctions, and pullback stability corresponds to the “frame distributivity” rule which holds for locales, which says that binary meets distribute over joins. I’m not sure about the “disjoint” condition, though.
   4. “where all congruences have effective quotient objects, which are also pullback-stable.” I don’t understand.

   But it does not seem that a (0,1)-category which is also an elementary topos is a complete Heyting algebra. The issue is that there is no subobject classifier. One reasons that the subobject classifier must be the terminal object of the cHa (it would be necessary to have a map into the subobject classifier from any object), but then since the pullback of every iso is an iso, every object must be the terminal object (Top), so the category is made only of terminal objects.

   Is it in fact the case that a (0,1)-category which is a Grothendieck topos is a locale? And is there any formal way to view complete Heyting algebras as decategorified elementary toposes?

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeSep 30th 2016
   • (edited Sep 30th 2016)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexRegarding congruences, these are not very interesting in a poset, all parallel arrows being equal already. So the quotient object is just the codomain. At [[Heyting algebra]] the qualifier 'almost' is used when describing the relation. Todd Trimble writes [on his personal web](https://ncatlab.org/toddtrimble/published/An+elementary+approach+to+elementary+topos+theory): >a topos is a locally cartesian closed Heyting pretopos (in particular an effective regular extensive category with finite colimits, covering all those conditions of Giraud’s theorem that are “elementary”) so aside from arbitrary colimits, you can use a lot of what you wrote already. It may be that the idea of a subobject classifier is just too impredicative to exist in a poset. I wouldn't be surprised if there were a fibration over the poset that played the role of the subobject classifier; maybe the codomain fibration does this, since all arrows are monosyllabic.

   Regarding congruences, these are not very interesting in a poset, all parallel arrows being equal already. So the quotient object is just the codomain.

   At Heyting algebra the qualifier ’almost’ is used when describing the relation.

   Todd Trimble writes on his personal web:

   a topos is a locally cartesian closed Heyting pretopos (in particular an effective regular extensive category with finite colimits, covering all those conditions of Giraud’s theorem that are “elementary”)

   so aside from arbitrary colimits, you can use a lot of what you wrote already.

   It may be that the idea of a subobject classifier is just too impredicative to exist in a poset. I wouldn’t be surprised if there were a fibration over the poset that played the role of the subobject classifier; maybe the codomain fibration does this, since all arrows are monosyllabic.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 30th 2016
   • (edited Sep 30th 2016)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexOf course, that "is" (in the sentence from my web page) isn't an "is" in the same sense as "is the same as" -- it signifies satisfaction of a predicate (as in "Todd is blue-eyed"). Disjointness of coproducts fails badly in a general poset. I'm not sure what was intended on the $(0, 1)$-category page; can someone clarify? I *do* think of lex totality as coming close to capturing the property of being a Grothendieck topos, and that being a locale could be reasonably construed as a $(0, 1)$-version of lex totality. As for the stuff about elementary topos: not sure what was meant there either. We *can* say that a Heyting algebra is a $(0, 1)$-quasitopos: that's very different. (Notice for one thing that toposes are balanced categories, whereas posets are balanced iff they are discrete.)

   Of course, that “is” (in the sentence from my web page) isn’t an “is” in the same sense as “is the same as” – it signifies satisfaction of a predicate (as in “Todd is blue-eyed”).

   Disjointness of coproducts fails badly in a general poset.

   I’m not sure what was intended on the $(0, 1)$-category page; can someone clarify? I do think of lex totality as coming close to capturing the property of being a Grothendieck topos, and that being a locale could be reasonably construed as a $(0, 1)$-version of lex totality.

   As for the stuff about elementary topos: not sure what was meant there either. We can say that a Heyting algebra is a $(0, 1)$-quasitopos: that’s very different. (Notice for one thing that toposes are balanced categories, whereas posets are balanced iff they are discrete.)

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeSep 30th 2016
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex>Of course, that “is” (in the sentence from my web page) isn’t an “is” in the same sense as “is the same as” yes, I hoped that was clear. >Disjointness of coproducts fails badly in a general poset. I _thought_ that would be a bit tricky to satisfy :-) As far as elementary toposes go, I would guess that one could _define_ an elementary (0,1)-topos as a Heyting algebra (not necessarily complete, since that would be a non-elementary notion). Just as a (2,1)-topos is not a (2,1)-category that is a topos, insofar as that makes sense...

   Of course, that “is” (in the sentence from my web page) isn’t an “is” in the same sense as “is the same as”

   yes, I hoped that was clear.

   Disjointness of coproducts fails badly in a general poset.

   I thought that would be a bit tricky to satisfy :-)

   As far as elementary toposes go, I would guess that one could define an elementary (0,1)-topos as a Heyting algebra (not necessarily complete, since that would be a non-elementary notion). Just as a (2,1)-topos is not a (2,1)-category that is a topos, insofar as that makes sense…

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeSep 30th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThe statement that "elementary $(0,1)$-toposes are essentially equivalent to Heyting algebras" was added by Toby in [revision 2](https://ncatlab.org/nlab/revision/diff/%280%2C1%29-topos/2). This was in reaction to me saying "(0,1)-topos" for "Grothendieck (0,1)"-topos in version 1.

   The statement that “elementary $(0,1)$-toposes are essentially equivalent to Heyting algebras” was added by Toby in revision 2. This was in reaction to me saying “(0,1)-topos” for “Grothendieck (0,1)”-topos in version 1.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 30th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItex> yes, I hoped that was clear I knew you knew it, David, but wanted to make sure it was clear to everyone reading. Being a locally cartesian closed Heyting pretopos does come pretty close after all to being a topos. A while back I found a counterexample; I'll have to recall what it is.

   yes, I hoped that was clear

   I knew you knew it, David, but wanted to make sure it was clear to everyone reading. Being a locally cartesian closed Heyting pretopos does come pretty close after all to being a topos. A while back I found a counterexample; I’ll have to recall what it is.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 30th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexJust as a 1-topos (elementary or Grothendieck) is not the same as "a 2-topos that happens to be a 1-category", a (0,1)-topos is not the same as "a 1-topos that happens to be a poset". In the Grothendieck case, the difference is that in an $n$-topos one requires (in addition to existence of all colimits) descent for "quotients of multi-object $n$-groupoids". When $n=1$, that reduces to coproducts and quotients of equivalence relations. When $n=(\infty,1)$ it's equivalent to having descent for *all* $(\infty,1)$-colimits. But when $n=(0,1)$ I think it is a vacuous condition. In the elementary case, the difference is that in an $n$-topos one requires classifiers for $n$-subobjects. When $n=1$ this is an ordinary subobject classifier. When $n=\infty$ it is an classifier for all objects. But when $n=(0,1)$ I think it is again vacuous.

   Just as a 1-topos (elementary or Grothendieck) is not the same as “a 2-topos that happens to be a 1-category”, a (0,1)-topos is not the same as “a 1-topos that happens to be a poset”.

   In the Grothendieck case, the difference is that in an $n$-topos one requires (in addition to existence of all colimits) descent for “quotients of multi-object $n$-groupoids”. When $n=1$, that reduces to coproducts and quotients of equivalence relations. When $n=(\infty,1)$ it’s equivalent to having descent for all $(\infty,1)$-colimits. But when $n=(0,1)$ I think it is a vacuous condition.

   In the elementary case, the difference is that in an $n$-topos one requires classifiers for $n$-subobjects. When $n=1$ this is an ordinary subobject classifier. When $n=\infty$ it is an classifier for all objects. But when $n=(0,1)$ I think it is again vacuous.

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 30th 2016
   • (edited Sep 30th 2016)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexAh, thank you, Mike! So the statements on the [[(0,1)-category]] page are all right after all? It seems to me that [[(0,1)-topos]] could use more fleshing out, e.g., a definition section. The page [[(n,1)-topos]] on the other hand looks useful. It may not be important for this discussion, but the example I wanted at the end of #6 is perhaps the [[ex/lex completion]] of $Set^{\bullet \to \bullet}$, which if I got things right is a locally cartesian closed pretopos but which has no subobject classifier.

   Ah, thank you, Mike! So the statements on the (0,1)-category page are all right after all?

   It seems to me that (0,1)-topos could use more fleshing out, e.g., a definition section. The page (n,1)-topos on the other hand looks useful.

   It may not be important for this discussion, but the example I wanted at the end of #6 is perhaps the ex/lex completion of $Set^{\bullet \to \bullet}$, which if I got things right is a locally cartesian closed pretopos but which has no subobject classifier.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeSep 30th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, I probably wouldn't say "A (0,1)-category with the structure of a topos is a (0,1)-topos", especially since [[topos]] is linked to a page mostly about 1-toposes. I would say something more like "A (0,1)-topos is a (0,1)-category with extra structure" (in fact, property-like structure).

   Well, I probably wouldn’t say “A (0,1)-category with the structure of a topos is a (0,1)-topos”, especially since topos is linked to a page mostly about 1-toposes. I would say something more like “A (0,1)-topos is a (0,1)-category with extra structure” (in fact, property-like structure).

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 1st 2016
    • (edited Oct 1st 2016)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI'm actually a little stuck: what is a [[(0,1)-topos]] from first principles? The Idea section of that page reads as if it's a Heyting algebra *by fiat*, which of course we don't want. The page [[(n,1)-topos]] isn't as helpful for this as I first imagined, since it only seems to deal with Grothendieck (n,1)-toposes, following Lurie. Please correct me if I'm wrong. Edit: looking at Mike's #5 again, I suppose for a terminal $(0, 1)$-topos the terminal object would be the classifier. But then, if we define a $(0, 1)$-topos to be be a cartesian closed $(0, 1)$-category with such a classifier (which is there vacuously), then we get just a cartesian closed poset, which need not have joins to make it a Heyting algebra. Maybe I don't understand what an elementary $(n, 1)$-topos is supposed to be.

    I’m actually a little stuck: what is a (0,1)-topos from first principles? The Idea section of that page reads as if it’s a Heyting algebra by fiat, which of course we don’t want.

    The page (n,1)-topos isn’t as helpful for this as I first imagined, since it only seems to deal with Grothendieck (n,1)-toposes, following Lurie. Please correct me if I’m wrong.

    Edit: looking at Mike’s #5 again, I suppose for a terminal $(0, 1)$-topos the terminal object would be the classifier. But then, if we define a $(0, 1)$-topos to be be a cartesian closed $(0, 1)$-category with such a classifier (which is there vacuously), then we get just a cartesian closed poset, which need not have joins to make it a Heyting algebra. Maybe I don’t understand what an elementary $(n, 1)$-topos is supposed to be.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeOct 1st 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, I don't think the definition of elementary $n$-topos is decided in general yet, but it should certainly include finite colimits. I view it as sort of an accident that when $n=1$ one can construct finite colimits from power objects and so they can be excluded from the definition; in general they should be there.

    Well, I don’t think the definition of elementary $n$-topos is decided in general yet, but it should certainly include finite colimits. I view it as sort of an accident that when $n=1$ one can construct finite colimits from power objects and so they can be excluded from the definition; in general they should be there.