Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: topos theory

Topic: closed subtoposes

Morgan Rogers (he/him) (Nov 10 2020 at 14:05):

In Johnstone's Sketches of an Elephant Remark C3.2.9, he observes that a closed inclusion of locales is proper, by observing that the right adjoint to the corresponding map of frames is the inclusion of an up-set $(\uparrow U) \subseteq \mathcal{O}(X)$, and so "preserves all non-empty joins". It is intuitively clear what he means by this for locales over $\mathbf{Set}$, but what is the right way to express "non-empty joins" constructively? I quoted that remark in a paper I am writing, and realised that it's not clear what it means in terms of $\mathcal{E}$-indexed colimits.

Morgan Rogers (he/him) (Nov 10 2020 at 14:08):

Describing the internal diagram category indexing the colimits, suggestions that come to mind are that the object of objects should be pointed? Or well-supported? But both of those seem rather strong impositions, and in particular it is not clear whether they would include all of the directed joins which are required for properness in general.

Morgan Rogers (he/him) (Nov 10 2020 at 14:29):

Although I suppose that whatever the "right" definition of non-emptiness is, that will be a pre-requisite to directedness, so that's not so much of a concern...

Morgan Rogers (he/him) (Nov 11 2020 at 16:20):

I've decided that the well-supported version is the right one (being the internal expression of "inhabitedness"), although it's still not clear to me whether this is a description of the maximal collection of colimits preserved by a generic closed inclusion of locales. :shrug:

Steve Vickers (Nov 13 2020 at 17:47):

Even better, a closed inclusion to $X$ is entire. (Elephant B4.4.21, but surely he means $\mathcal{E}=\mathcal{S}$. See Moerdijk-Vermeulen “Proper maps of toposes”, 5.5.) It suffices to treat $X$ as the base topos, so we are dealing with sublocales of 1. Now suppose $P$ is open - a subobject of $1=\{\ast\}$ - with locale presented by $\top \vdash \bigvee P$, and $X-P$ its closed complement, presented by $\bigvee P \vdash \bot$. Then $X-P$ is a Stone locale, with Boolean algebra of clopens presented as $BA\langle \quad\mid 0=1 (\ast\in P)\rangle$. Maietti and I used this in our paper on arithmetic universes, in order to get a structure theorem for closed subspaces.

Morgan Rogers (he/him) (Nov 13 2020 at 18:21):

That is exceptionally useful information to me personally), since it shifts around the big diagram I have mapping relationships between types of geometric morphisms. I hadn't read the section of "Proper maps of toposes" on entire morphisms since I hadn't realised they might be relevant to what I was doing.
Unfortunately, however, this doesn't directly address my problem, unless there are facts about entire morphisms I'm ignorant of: while entire morphisms don't preserve coproducts, closed inclusions do preserve binary joins of subterminal objects. So they're even more special than entire morphisms! However, they don't preserve arbitrary joins, since the empty join is preserved iff it's the trivial inclusion. So they preserve inhabited joins, for some notion of inhabited; that's what I wanted to figure out.

Steve Vickers (Nov 13 2020 at 22:50):

An inclusion is closed iff it is entire. Right to left is because entire maps are proper - in fact they’re proper separated. Entire means fibrewise Stone, proper means fibrewise compact, proper separated means fibrewise compact regular. (By “fibrewise X” I mean that, as an internal locale in sheaves over the codomain, it has property X. That only really makes sense if property X is geometric, so the fibrewise X maps are stable under pullback.)

Morgan Rogers (he/him) (Nov 14 2020 at 10:59):

I had understood the equivalence of closedness and entireness for inclusions. I was trying to articulate the following:
The implication "entire => tidy" means that the direct image functor preserves all directed/filtering colimits.
The implication "pure + entire => equivalence" means that a non-trivial entire morphism never preserves all binary coproducts.
The implication "tidy => proper" means that (of course) a closed inclusion preserves internally indexed directed unions of subterminals.
But at the level of subterminal objects we can say more! Closed inclusions, despite being entire, have direct image functors preserving binary coproducts of subterminal objects, and as far as $\mathbf{Set}$-indexed colimits go, they moreover preserve all inhabited unions of subterminals. That is, closed inclusions also have the property "direct image preserves inhabited colimits of subterminals", extending properness.

Morgan Rogers (he/him) (Nov 14 2020 at 11:02):

I was trying to work out what the correct expression of inhabitedness is, and I came to the conclusion that the internal translation of it (well-supportedness) is the right one.