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: localic topoi


view this post on Zulip Eduardo Ochs (Mar 07 2021 at 03:10):

Hi all... I am looking for alternative presentations of the material in chapter IX ("Localic Topoi") of Mac Lane and Moerdijk's "Sheaves in Geometry and Logic"... I guess that there must be a bunch of master's theses around that present that in other ways, but I am too outsiderish to know how to found them, and my naïve attempts to google that didn't return anything... hints? Pointers? Links?

My problem with ML&M's book is that the authors don't separate clearly what is the motivating, "archetypal" case and what is the generalization. It took me ages to find out how to do this separation for Grothendieck topologies, and I just spent two days trying to do that on the "functor of points" pt: (Locales) -> (Spaces)... and "two days" means "enough homework", which means "now I can ask", so here is my question. Pointers, please?

Thanks in advance!!! =)

view this post on Zulip Frederick Kintanar (Mar 07 2021 at 06:28):

I would also be interested in pointers to getting started with Localic Topoi. I am looking at Steven Vickers' Topology via Logic, which seems to be locale theory from a the prespective of computation. He talks about a logic of finite observations. I notice that Vickers has a lot of more recent articles about toposes and locales on his web page: https://www.cs.bham.ac.uk/~sjv/papersfull.php

If anybody has suggestions which of his papers, and maybe in what order, would be useful as background for Mac Lane and Moerdijk's chapter IX on Localic Topoi, that would be greatly appreciated.

view this post on Zulip Jens Hemelaer (Mar 07 2021 at 10:17):

Hi! What the motivating examples or typical cases are depends a lot on your personal point of view. Here are some of the points of view that I can think of:

Let me know if you are interested in any of these.

Then there is the point of view of logic (or probably that's multiple points of view as well). I'm not very familiar with this perspective, but others here on Zulip can likely give pointers in that direction.

view this post on Zulip John Baez (Mar 07 2021 at 15:27):

Regarding logic, Stone duality can be seen as a duality between topology (Stone spaces) and logic (boolean algebras) - and then the duality between locales and frames generalizes this to a bunch of non-boolean cases. Maybe this observation is too elementary and Eduardo Ochs is already familiar with it - I don't know! But if someone is trying to understand locales, it seems a bit of preparation thinking about good old Stone duality could be helpful. For example:

The nLab writes:

The monograph is ultimately about the Stone representation theorem, but also a standard reference on using locales in place of topological spaces. Although it is a work of mathematics rather than metamathematics, it shows clearly by example how (usually) results about locales do not require the axiom of choice even when analogous results about topological spaces do.

view this post on Zulip John Baez (Mar 07 2021 at 16:03):

I've never thought about localic topoi, but they seem cool:

In intrinsic terms, a topos is localic if it is generated under colimits by the subobjects of its terminal object 1.

In equivalent but extrinsic terms, a category is a localic topos if it is equivalent to the category of sheaves on a locale with respect to the topology of jointly epimorphic families (accordingly, every localic topos is a Grothendieck topos).

Maybe my blundering first thoughts will be amusing to some.

So when I think "locale" I start by thinking "topological space", since there's a big overlap - namely the sober spaces, the topological spaces where you can figure out the points from the open sets. Locales are basically an improved version of topological spaces, better for category theory. So the second sentence above is saying "a localic topos is a category of sheaves on some t̶o̶p̶o̶l̶o̶g̶i̶c̶a̶l̶ ̶s̶p̶a̶c̶e̶ locale". And that's good because categories of sheaves on topological spaces are one of the two kinds of topoi that are easy for me to understand (the other being the presheaf topoi).

view this post on Zulip John Baez (Mar 07 2021 at 16:07):

Then the first sentence becomes really interesting: a topos is localic if it's generated under colimits by subobjects of the terminal object.

view this post on Zulip John Baez (Mar 07 2021 at 16:08):

This is beautiful!

view this post on Zulip John Baez (Mar 07 2021 at 16:08):

To understand this, I think about the subobjects of the terminal object in the category of sheaves on a topological space, as an example.

I'm pretty sure these correspond to open sets of the topological space. Given any open set U there's a sheaf that has one section over V whenever V \subseteq U, and none otherwise. I mentally visualize this as a very flat thing sitting over U, and nothing anywhere else.

Then the sentence is saying we can build up all sheaves by taking colimits of this kind of sheaf. And that seems plausible. If I try to prove it, I seem to get pushed toward the "etale space" description of sheaves, where a sheaf gives a space that's made by gluing together a bunch of flat things.

view this post on Zulip Fawzi Hreiki (Mar 07 2021 at 16:09):

There's also chapter C1 in the Elephant on sheaves on locales

view this post on Zulip Fawzi Hreiki (Mar 07 2021 at 16:11):

The most interesting thing about locales is that they let you study things which don't even exist, e.g. the locale of surjections NR\mathbb{N} \rightarrow \mathbb{R}.

view this post on Zulip Fawzi Hreiki (Mar 07 2021 at 16:11):

In a sense by pretending like they do exist and studying their 'side effects'

view this post on Zulip Mike Shulman (Mar 07 2021 at 16:11):

Of course, arbitrary toposes do that too.

view this post on Zulip Fawzi Hreiki (Mar 07 2021 at 16:11):

Sure, but at a much higher level of complexity/difficulty

view this post on Zulip Mike Shulman (Mar 07 2021 at 16:12):

Locales let you study "structure" that doesn't exist, while toposes let you study "stuff" that doesn't exist. (-:

view this post on Zulip Fawzi Hreiki (Mar 07 2021 at 16:12):

That's interesting - how so?

view this post on Zulip Mike Shulman (Mar 07 2021 at 16:15):

Localic toposes are the classifying toposes of propositional geometric theories, which are roughly the theories whose forgetful functor to Set (or whatever base category you take models in, since we're interested in theories that don't have any models in Set) forgets at most structure. Arbitrary forgetful functors can forget stuff as well.

view this post on Zulip Mike Shulman (Mar 07 2021 at 16:16):

There's a more extended discussion of this in section 5.4 of Lectures on n-Categories and Cohomology.

view this post on Zulip Fawzi Hreiki (Mar 07 2021 at 16:22):

Nice. Thanks

view this post on Zulip Eduardo Ochs (Mar 07 2021 at 17:37):

For me the archetypal case is the one in which our locales come from topological spaces... i.e., they have "enough points", see ML&M, propositions 2 and 3 in pages 477-479.

My main interests are Logic and formalizing parts of CT in Type Theory using a certain diagrammatic language to help in the translation, as in this preprint. In some situations I use a slightly weirder notion of "archetypal", and in it my archetypal topological spaces are the order topologies on finite posets... this is like the "point-set topology point of view" that Jens mentioned, but I am focusing on finite cases in which everything can be drawn explicitly...

view this post on Zulip Jens Hemelaer (Mar 07 2021 at 19:38):

In the case of presheaves on a poset there are a few results that make things easier. I'll list some results here, I'm not saying they are easy to prove but maybe they give some intuition.

As you already said, the corresponding topological space are order topologies (also known as Alexandrov-discrete spaces).

If PP is a finite poset, then the Alexandrov-discrete space XX such that Sh(X)PSh(P)\mathbf{Sh}(X) \simeq \mathbf{PSh}(P) is again finite. The underlying set of XX is the same as the underlying set of PP, and the open sets in XX correspond to the downwards closed sets in PP. Every point has a smallest open neighborhood, corresponding to the downwards closure in PP. This means that if you have a sheaf F\mathcal{F} and a point xx, then the stalk Fx\mathcal{F}_x is the same thing as the set of sections F(U)\mathcal{F}(U) where UU is the smallest open neighborhood of xx.

If XX is any finite topological space, then you can always find a finite poset PP such that Sh(X)PSh(P)\mathbf{Sh}(X) \simeq \mathbf{PSh}(P). This poset PP is the opposite category of the specialization order on XX. The correspondence between finite posets and finite topological spaces is explained here.

The Grothendieck topologies on a finite poset PP can be completely classified. There is precisely one Grothendieck topology corresponding to each subset SPS \subseteq P. The corresponding subtopos is then PSh(S)PSh(P)\mathbf{PSh}(S) \subseteq \mathbf{PSh}(P), where the poset structure on SS is the one induced by the poset structure on PP.

view this post on Zulip Eduardo Ochs (Mar 07 2021 at 20:17):

Thanks!!! I have a good intuition on most of this, but let me write down the definitions and the calculations and check some details...

view this post on Zulip Eduardo Ochs (Mar 07 2021 at 20:19):

To be honest I am still struggling with this Sh(X). I'll clean up my material and ask some precise questions soon (in a few days).

view this post on Zulip Frederick Kintanar (Mar 08 2021 at 16:43):

Mike Shulman said:

There's a more extended discussion of this in section 5.4 of Lectures on n-Categories and Cohomology.

I read "Lectures on n-Categories and Cohomology" several years ago, and I have come back to it at least once. The intuitions I am trying to make precise come from linguistics, specifically lexical semantics and polysemy. I was thinking of groupoids in some (homotopy?) type theory as spaces of variation within something like "synonymy" of word senses. This notion of synonymy is like families of identifications of word senses, parametrized by something. If the semantic space is the variability of an action verb, some of the parameters would be "referential indices" associated with the head nouns of Noun Phrases dependent on the verb. (This probably connects with the string diagrams of Quantum NLP, the referential indices are like cup products, and the Verb's dependency on an argument (or complement or adjunct) provides a cap product. When a referential index "matches" an argument role, you can yank the zigzag straight.)

The link to locale theory is useful for working with typing judgments as propositional types. Something along these lines was worked out a long time ago by Barwise and Seligman in their book Information Flow: the Logic of Distributed Systems, using Chu spaces of propositional types and tokens that support them. The information flow discussion seems mostly model-theoretic, Vickers' discussion of a logic of finite observations suggests a more proof-theoretic or algorithmic way of constructing witnesses to an entailment between (sets of) propositional types. From scanning some of Vickers' more recent papers, he seems to be trying to use topos theory to do something for predicates similar to what he did with locale theory for propositions. I'd like to understand better what he has done with locales and propositions ("affirmative assertions"), and how he extends this to topoi and predicates.

view this post on Zulip Eduardo Ochs (Mar 23 2021 at 05:59):

Hi @Jens Hemelaer,
I just finished (the first draft of) this:
"Grothendieck Topologies for Children"
The sheaves are the next step... =)

view this post on Zulip Jens Hemelaer (Mar 23 2021 at 07:16):

Hi @Eduardo Ochs, I just had a look at it. Interesting way to draw Grothendieck topologies, it's more compact than I would have thought. Good luck with tackling the sheaves!

view this post on Zulip Matteo Capucci (he/him) (Mar 23 2021 at 07:19):

That's cool! Is that the drawing of the quotient locale associated to the associated nucleus of JJ?

view this post on Zulip Morgan Rogers (he/him) (Mar 23 2021 at 15:41):

That must have taken ages to typeset! :upside_down:

view this post on Zulip Eduardo Ochs (Mar 23 2021 at 16:26):

Hi @Matteo Capucci (he/him)! I have a nice way to draw nuclei in the second paper here - http://angg.twu.net/math-b.html#zhas-for-children-2 - using question marks, but I don't understand all the standard concepts yet... I am using these visual notation to help me in decyphering them...

view this post on Zulip Eduardo Ochs (Mar 23 2021 at 16:30):

@Morgan Rogers (he/him), I used Dednat6! The full source code of the notes are here: http://angg.twu.net/LATEX/2021groth-tops-children.zip

Just unpack the .zip and run "lualatex 2021groth-tops-children.tex".

view this post on Zulip Eduardo Ochs (Apr 04 2021 at 03:31):

Hi @Matteo Capucci (he/him)! I just uploaded a new version, that has some "X-shaped diagrams" like the two that appear in the screenshot below, in which the quotient locales appear at the upper-right side and the JJ appear at the lower right side of the X-shaped diagrams... do they look like what you were expecting?
sshot.png