Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
If we use 2 living in many categories to generate a range of dualities, including the - one, what about an version?
What would happen if we were to equip the object classifier of -groupoid, , coproduct of the automorphism ∞-groups of all (small) homotopy types , with different structures?
Imitating the - duality, what happens with the map , which is ?
Are those slices special kinds of -topos, like is a special kind of Heyting algbra, i.e., Boolean and complete atomic?
Just two boring remarks:
is not an -topos but just the small core -groupoid inside one. (It should be an -topos if the ambient context were an -topos instead of just an -topos.)
Then I notice that I have trouble finding the page on the Lab which would discuss the duality that you mention. I seem to remember that people wrote it down somewhere, but in any case it seems to need more pointers. None of the entries that one would naively open seem to mention it at all (?)
Oh, now I found it. It’s hidden at BoolAlg. I’ll copy this over to Stone duality now and add some more cross-links.
It’s true that the internal-hom in isn’t itself an -topos but rather the core of one, however the same is true in the uncategorified case: the internal-hom in isn’t itself a Boolean algebra but only the core of one. In the latter case, the BA structure comes from an internal BA structure on ; likewise the internal -topos structure on induces an -topos structure on . Those toposes are indeed very special, but I don’t remember offhand if they have a nice characterization like CABAs. Let’s see, they have a set of tiny generators, which is kind of like “atomicity” for a Boolean algebra and is enough to make them a presheaf category, and they are Boolean (at least, assuming the ambient is). Possibly they are the only Boolean presheaf toposes? Is atomicity of a boolean algebra related to the notion of “atomic topos”?
Ah, right. Thanks. That’s an excellent question of David’s there, it seems.
So we might find two ’concrete’ -categories over , and a dualizing object with as underlying -groupoid.
I wonder if there’s a candidate for .
Maybe some kind of -topos…
I posted about this at MO.
And there followed an answer from Jacob Lurie!
Is Lurie’s answer part of what would make for a homotopified hyperdoctrine?
Hm, I thought the question was more generally about the internal toposes in general ambient -toposes.
Regarding #10: yes, the concept of hyperdoctrine is precisely an axiomatization of the key aspects of the self-indexing of a nice enough category over itself, i.e. of the functor that assigns slice categories . This is in turn pretty much what dependent type theory is about and the homotopy-theoretic version of that (“-hyperdoctrine”) is what dependent homotopy type theory is about.
Re #11, now I’m not so sure what they question was. There could have been a better one I’m sure.
Do we have a Spec-like process to take us back from a slice topos back to , as we do from the powerset of a set? If so, is it by mapping into a dualizing object?
There is this proposition (also due to Jacob Lurie, of course) which says that geometric morphisms between slice -toposes that respect the canonical geometric morphisms to are equivalent to morphisms in . So at least the -groupoid of global points of may be recovered as the -groupoid of suitable maps . If you concentrate on then this means that all of is recovered this way. More generally, all of may be recovered by looking at all such suitable maps as varies over all of . That recovers as what represents this sheaf on with respect to the canonical topology.
And it’s the way geometric morphisms are written in that order, , that makes it seem different from the dualizing object way of recovering set from , ie., the idea of having living in different categories? Now the comparison is between and as in some sense the same thing living in different worlds?
Right, the direction of the morphism drawn for a geometric morphism is subject to some convention. When thinking of toposes as spaces, then it is most natural to draw the geometric morphis the way I did above as pointing along its direct image. If one however thinks of toposes as algebras (algebras of “functions” (sheaves) on a site) then it is natural to draw the geometric morhism is pointing in the direction of its inverse image functor. That might better match the analogy that you are looking at, I suppose.
And, yes is the internal appearance of inside itself (after all, das Wesen muß erscheinen ;-) so one might hope that these statements about slices of over pass along to the internal toposes – as we know they do when .
That’s what I was thinking the question was about, and that’s what I meant I didn’t see really discussed in that MO reply! But I should say that I am not able to concentrate with full energy on this issue, being distracted by other tasks, so I may be missing something.
What happens in the case of an ordinary topos? I mean if the subobject classifier is an internal Heyting algebra object, can whatever there is to be said about the external Heyting algebra of subobjects be passed to the internal Heyting algebra powerset?
Also, there’s still the question of what Mike was pointing to in #4 of special features of and its slices.
I no longer have any idea what the real question is, but the answer to
can whatever there is to be said about the external Heyting algebra of subobjects be passed to the internal Heyting algebra powerset?
is most likely something like “anything constructive”.
If one however thinks of toposes as algebras (algebras of “functions” (sheaves) on a site) then it is natural to draw the geometric morhism is pointing in the direction of its inverse image functor.
However, I thought that when writing it in that direction, one no longer calls it a “geometric morphism”.
That’s true. Or at least it ought to be true. I am afraid I have seen violation of this reasonable convention by otherwise reasonable people ;-)
So are the questions from #16 and Lurie’s answer something like:
Do these even make sense?
They do make sense, and they ought to have good answers. In the case of 1-topoi, the answers are known, and I would expect analogous answers in the ∞-case, but I don’t know whether anyone has written them down.
@Mike #22
so what’s the answer to David C’s first question? I’ve been wondering what internal topos objects in a topos are and how this relates to inner model theory for sets.
Well, an elementary topos is an essentially algebraic structure, so a small one of them can be defined internally in any category with finite limits. Similarly, inside a topos that contains a universe object , we can define a -Grothendieck topos in a straightforward way (an internal category with limits and colimits indexed by elements of , etc.)
If we want to allow “internal” toposes that are of the same size as the ambient topos, then we need to talk instead about indexed toposes over the base, as in Part B of the Elephant.
@Mike
I know this much - when you say we know ’what are the internal topos objects’, I was expecting some sort of theorem or characterisation (like Lawvere-Tierney topologies corresponding to etc…). But do we know when internal topos objects exist? Given the category of ZF(C)-sets, we can talk of the internal topos of L-sets (I think? Perhaps this is only different in the case of ZF, rather than when everything is well-orderable), or the topos of sets of an inner model of (B)Z. But given say a model of ETCS, don’t Gödelian considerations force us to make an internal topos object (with NNO!) an extra assumption? I’m not talking universes here, which are understood.
Given David C’s question, one can further nuance it: what are the internal (-)topos objects corresponding to eg universes? To inner models? To a mixture of these notions, since we have the whole tower of h-levels to play with?
I was expecting some sort of theorem or characterisation
Well, there is the Diaconescu-Giraud theorem for indexed Grothendieck toposes. But I thought David C’s question was about a definition.
Given the category of ZF(C)-sets, we can talk of the internal topos of L-sets
Yes, although it’s really better to say “indexed” rather than “internal” in cases like this, and that answers your other question – if it really were internal, then Godelian considerations would prevent its existence, but since it’s indexed, it’s just analogous to how in material set theory we construct from without any worries about Godel. (Even starting from a model of ZFC we may not have .)
what are the internal (∞-)topos objects corresponding to eg universes? To inner models?
In what sense do you mean “what are”? What do you want to know about them?
Yes, although it’s really better to say “indexed” rather than “internal” in cases like this
Ah, I see! So inner models should be indexed toposes, rather than internal toposes… I may have been barking up the wrong tree for a bit, then. Models of which V is an end extension, however should be some sort of internal topos - but this is getting way off-topic.
What do you want to know about them?
This was just how I was interpreting David’s question, not my own question
There should be another possibility, intermediate between indexed toposes and internal models of the essentially algebraic theory of elementary toposes, namely internal models of the regular theory of elementary toposes. This would correspond to the difference between “merely” having finite limits and power objects and having “chosen” finite limits and power objects. I wonder if it’s possible to strictify? (There’s no problem if we have the axiom of choice, I guess.)
There’s a third option that occurs to me, but this is special to set theory. Ideally L should be some sort of initial or minimal sub-ZF-algebra in the sense of algebraic set theory, since every model of ZF comes with a its own L.
It would be really nice to make this L precise in categorical terms, e.g., via algebraic set theory.
I… don’t think I’ve ever thought of in AST terms before. Someone should pursue that!
@Zhen, good point. I’d probably be inclined to regard the regular theory as the “correct” one to think about. (“Really”, since a 1-topos is a 1-categorical object, we should be talking about internalizing it not in another 1-topos but in a 2-topos or (2,1)-topos, and if we start with a 1-topos then we should be moving to the corresponding 2-topos consisting of internal categories and anafunctors, so that a 2-essentially-algebraic theory therein will correspond to a regular theory back in the original 1-topos.)
And we could consider the 2-category of fibrations, or such like, as in one of the promised stack semantics papers ;-)
More seriously, I think you told me once, Mike, that definability on the material side relates to fibrations on the structural side. This makes the appearance of fibrations in defining L as a ZF-algebra quite compelling.
I see Lurie has an -version of Stone duality in section 3.5.3 of Spectral Algebraic Geometry between profinite -toposes and some kind of bounded -pretoposes.
Does this point the way to some homotopified syntax-semantics duality as Forssell and Awodey did with ordinary Stone duality?
Ooh, did he update again?
EDIT: no, just that I forgot the appendix is numbered ’3’ instead of ’A’. Still only contains up to section 2.1 + appendix
Yes, though at over 400 pages, perhaps the appendix will become part of the main text.
Regarding
…the theory of bounded -pretopoi… seems to provide a good language for extending concepts of first-order logic to the -categorical setting. We offer some evidence for this last assertion in §A.1.9 by proving an ∞-categorical generalization of the “conceptual completeness” theorem of Makkai-Reyes (see [112]), asserting that a morphism of bounded ∞-pretopoi is an equivalence if and only if and have the same “models”. (p. 466 (as of 9 Jan))
I wonder if the topological groupoid approach to the models of first-order theories of Awodey and Forssell might be preferable to Makkai’s, or perhaps better yet in view of the whole book ’Spectral Algebraic Geometry’, the approach of Breiner, another of Awodey’s students, in Scheme representation for first-order logic
Although contemporary model theory has been called “algebraic geometry minus fields” [15], the formal methods of the two fields are radically different. This dissertation aims to shrink that gap by presenting a theory of “logical schemes,” geometric entities which relate to first-order logical theories in much the same way that algebraic schemes relate to commutative rings.
It seems that Breiner has a good scheme-theoretic approach to the Makkai-Reyes result:
we reframe Makkai & Reyes’ conceptual completeness theorem as a theorem about schemes…The theorem follows immediately from our scheme construction. (p. 9)
I see Lurie has an unanswered related MO question about conceptual completeness.
I see that Lurie suggested an answer to his own question. Pro-étaleness appears again.
1 to 37 of 37