# Start a new discussion

## Not signed in

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

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeOct 13th 2010

started local geometric morphism (which previousy had been just a sub-point at essential geometric morphism)

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeOct 14th 2010

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 $f^!$ has also to be $S$-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.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeOct 14th 2010

Ah, I am sorry Mike. I keep making this mistake. And you keep correcting it.

I’d expect that $f^*$ being full and faithful is the (or a) right condition for the oo-case.

• CommentRowNumber4.
• CommentAuthorZhen Lin
• CommentTimeJun 4th 2013

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.

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeDec 29th 2016

I added to local topos a definition of local elementary topos, with a remark on terminology and the example of the free topos.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeDec 29th 2016

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.

• CommentRowNumber7.
• CommentAuthorTodd_Trimble
• CommentTimeDec 29th 2016

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.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeDec 30th 2016

The difference isn’t just truncation, but also finitary-ness, isn’t it?

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeDec 30th 2016

Just adding truncation to the Grothendieck notion produces something that it would be natural to call “$(-1)$-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 $r_* : O(X) \to O(1)$ of the locale morphism $r:X\to 1$ 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 $r^!$ to exist, just like the tower of notions of local connectedness (open, locally connected, locally 1-connected, …) and properness (compact, tidy, …)

• CommentRowNumber10.
• CommentAuthorTodd_Trimble
• CommentTimeDec 30th 2016

Re finitary: there is an argument that $\hom(c, -)$ preserving binary coproducts means preserving arbitrary coproducts as well in an $\infty$-extensive category. (However, the proof uses LEM in the meta-logic, if that is a concern.)

Very interesting observation in #9!

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeDec 30th 2016

Ah, you mean theorem 3.1 at connected object. Very good, I’d forgotten about that. So a Grothendieck topos over a classical base $Set$ is local iff $hom(1,-)$ preserves binary coproducts and coequalizers, which then $(-1)$-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.

• CommentRowNumber12.
• CommentAuthorTodd_Trimble
• CommentTimeDec 30th 2016

Thanks for pointing all this out, Mike.

• CommentRowNumber13.
• CommentAuthorDavidRoberts
• CommentTimeJan 1st 2017

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.

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeJan 2nd 2017

Constructive well-pointedness also requires ordinary well-pointedness, i.e. $1$ is a generator and nontrivial ($1\ncong 0$). Hyperlocality is what you have to add to classical well-pointedness to get constructive well-pointedness (classically, it’s implied by classical well-pointedness).

• CommentRowNumber15.
• CommentAuthorDavidRoberts
• CommentTimeJan 2nd 2017

Ah, that’s right. Hyperlocality relates to there being a fibration of well-pointed toposes, I remember.

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeJan 5th 2017

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.

• CommentRowNumber17.
• CommentAuthorDavidRoberts
• CommentTimeJan 5th 2017

Nonempty or inhabited with respect to whatever base topos is assumed?

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeJan 6th 2017

“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.

• CommentRowNumber19.
• CommentAuthorDavidRoberts
• CommentTimeJan 6th 2017

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 :-)

• CommentRowNumber20.
• CommentAuthorDavidRoberts
• CommentTimeJan 6th 2017
• (edited Jan 6th 2017)

’(duplicate)

• CommentRowNumber21.
• CommentAuthorTodd_Trimble
• CommentTimeJan 6th 2017

I think your added proof is holding up, Mike. Thanks!! That’s great.

• CommentRowNumber22.
• CommentAuthorMike Shulman
• CommentTimeJan 7th 2017

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).

• CommentRowNumber23.
• CommentAuthorDavidRoberts
• CommentTimeJan 7th 2017

Ok, thanks.