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.
started local geometric morphism (which previousy had been just a sub-point at essential geometric morphism)
Looks like we got bit again by the difference between Set-toposes and S-toposes for other bases. In general, for an S-topos to be local, the right adjoint has also to be -indexed, which isn’t automatic except when S=Set. I fixed this at local geometric morphism, but not yet at local (infinity,1)-topos since I don’t know which of the conditions remain equivalent and which is the right generalization.
Ah, I am sorry Mike. I keep making this mistake. And you keep correcting it.
I’d expect that being full and faithful is the (or a) right condition for the oo-case.
I added one of the more intriguing examples of a local geometric morphism, namely the one that relates a big topos to its corresponding little topos.
I added to local topos a definition of local elementary topos, with a remark on terminology and the example of the free topos.
Hmm, I can’t say I like that terminology, especially since it doesn’t specialize to the standard notion if the elementary topos happens to be Grothendieck.
Oh, that’s funny. I seemed to have jumped over a distinction I was emphasizing in the aIVT thread. :-\
Nevertheless, this terminology does appear in the literature! Let me think if there’s some sort of salvage.
The difference isn’t just truncation, but also finitary-ness, isn’t it?
Just adding truncation to the Grothendieck notion produces something that it would be natural to call “-local”: if the terminal object is the union of a family of subterminals, then one object of the family is already terminal. This is an extension back to 1-toposes of the natural notion of locality for 0-toposes, namely that the right adjoint of the locale morphism has a further right adjoint, or equivalently preserves joins. I don’t think I’ve seen anyone define this before, but there’s a natural tower of notions of “local” depending on at what categorical dimension we ask the right adjoint to exist, just like the tower of notions of local connectedness (open, locally connected, locally 1-connected, …) and properness (compact, tidy, …)
Re finitary: there is an argument that preserving binary coproducts means preserving arbitrary coproducts as well in an -extensive category. (However, the proof uses LEM in the meta-logic, if that is a concern.)
Very interesting observation in #9!
Ah, you mean theorem 3.1 at connected object. Very good, I’d forgotten about that. So a Grothendieck topos over a classical base is local iff preserves binary coproducts and coequalizers, which then -izes to the “elementary” notion of “local topos”. Unfortunately the infinitary-extensive argument doesn’t work for posets, which are never extensive, so there’s still a mismatch even disregarding classicality.
Thanks for pointing all this out, Mike.
Isn’t Awodey’s notion of hyperlocal elementary topos (re-dubbed in the section on local toposes as just ’local’) what Mike calls a constructively well-pointed topos? I do that access to either paper at the moment.
Constructive well-pointedness also requires ordinary well-pointedness, i.e. is a generator and nontrivial (). Hyperlocality is what you have to add to classical well-pointedness to get constructive well-pointedness (classically, it’s implied by classical well-pointedness).
Ah, that’s right. Hyperlocality relates to there being a fibration of well-pointed toposes, I remember.
Okay, here’s what I think is true: a Grothendieck topos is local iff 1 is connected, projective, and nonempty. Since this only alters the definition with respect to whether it includes the trivial topos, I took the liberty of changing the definition at local topos. I sketched the argument for the equivalence too; does it sound right? My brain is kind of fried at the moment, so I could be making a dumb mistake.
Nonempty or inhabited with respect to whatever base topos is assumed?
“Inhabited” only makes sense for objects of the base topos. “Nonempty” here means “not isomorphic to the initial object”, which may sound odd constructively since it has a negation, but is really just the nullary version of connectedness.
I guess a topos might not have any points, but still be in some sense, in the internal logic of the 2-category of toposes be ’inhabited’. But I see what you mean, and you know better than me :-)
’(duplicate)
I think your added proof is holding up, Mike. Thanks!! That’s great.
Thanks Todd! I’m glad to have this mostly cleared up.
David, I think this sort of inhabited/nonempty (for the terminal object of a topos) is completely different from the question of whether the topos has any points. But there do certainly exist toposes without any points but that are “inhabited” in the sense that their geometric morphism to Set is surjective (for instance, some non-spatial locales have this property).
Ok, thanks.
1 to 23 of 23