Joshua Brinkley from the University of Insubria will talk about the logic and geometry of

localic morphisms. Thank you very much to the organizers for allowing me to speak at this presentation. The story I want to share with you today is about how we can think about topos as ways of completing structure. So we might start off with some structure which

doesn't have all of the properties we want it to have and topos are going to give us a way of talking about what structure there should be there and what structure we can add. And so in particular as the title says we'll be looking at how we can add structure to

some certain logics coming from localic morphisms. So the idea behind the presentation I'm going to show you is that we want to utilize our intuition coming from a propositional setting.

So in a propositional setting we have localic toposes classifying propositional theories but we also have localic toposes obviously coming from locales. And so what we want to be able to do

is extend this to where we talk in a relative topos theoretic sense about having a localic morphism over a topos and that corresponding to an internal locale. And then on the theory side we want to be able to talk about what sort of geometric theory we might get out of that.

So that's the overall picture. I'm going to give some idea of what's going on with these branches of the bridge and then I'll give a specific case which ties in very nicely with

the logic. So yes for people who haven't seen the definition before a localic geometric morphism is a geometric morphism from a topos F to a topos E such that every object in our domain topos is a sub quotient of something in the inverse image of E. So some examples of

localic toposes. Every inclusion is localic. That should immediately tell us that every topos comes attached with at least one localic morphism to another one because

every topos has an inclusion into a pre-sheaf topos. And we can also get lots of examples of localic morphisms coming from locales. So when we take sheaves on a locale

this obviously gives us a localic topos but every arrow between two localic toposes is also going to be a localic geometric morphism. And we can do the same with

internal locales and do exactly the same construction relatively. So here we take the locales internal to a topos and we take sheaves, internal sheaves of these locales

and this gives us an embedding of the internal locales into cotton date toposes that has precisely the same properties that you'd expect from the normal localic setting. And every arrow between these localic toposes is going to be localic as well. Although there's

a little caveat to that because obviously when we take this embedding into here there comes a choice of the morphism to E. And so it will be localic up to that

up to that choice of arrow. And so we also have by a result from I believe João and Tierney that every localic geometric morphism is going to be, the domain topos is going to

be of the form given here that F is going to be the internal sheaves on the internal locale given by the direct image of a sub-object classifier. So this result gives us a very nice description of what the internal locales should be corresponding to a localic geometric

morphism. And so this is some examples of localic geometric morphism. So what is an internal locale? For the application I'm going to give at the end we're going to be concerned with internal locales of pre-sheaf toposes. So an internal locale of the pre-sheaf topos where C

has finite limits is going to be a functor from C into the category of locales such that all of our arrows have a left adjoint satisfying Frobenius reciprocity. This condition is Frobenius reciprocity. And also we have the Beck-Shevely condition holding.

These should be Fs down here. I forgot to change that. So those are internal locales. And so now we can appreciate the arches of the bridge here that the localic morphism is going to go to the internal locale given by the direct image

of a sub-object classifier. And similarly internal locales are going to induce localic morphisms by the projection into C. So now I want to move more onto the logic away from

internal locales, but we'll still see lots of localic properties cropping up. And that is in the idea of a localic expansion of a theory. So a localic expansion is where we take a theory,

we take its signature, and we add new relation and function symbols to that signature. And then we take a theory that proves all of the axioms of our previous theory. And now it's a theorem due to Caramello in theory sites and toposys that every

localic expansion produces a localic morphism between the classifying toposys. And so we can make the observation that every theory in a signature sigma is going to be a

localic expansion of the theory of objects without signature. This is the empty theory in the signature containing just the sorts and the signature of our theory. So no function symbols, no relation symbols, just equality. And so we're going to have that every classifying topos

is going to be localic over a topos of the classifying topos of the theory of objects for its signature. So the theory of objects is we're going to build a explicit site for it,

and it's going to involve the category of relabeling sorts, which I've denoted as sort subscript sigma. Now this category has as objects the finite strings of variables in the sorts. And then arrows between these finite strings of variables are going to be relabelings

of variables. So that means they are maps that respect sorts. Now, obviously if sigma is single sorted, then a finite string of variables is going to correspond to a finite set

and any relabeling because every map is going to respect sorts is just going to be every map. And so we have the category of relabelings for a single sorted theory is given by FinSats. And so then we can observe since the classifying topos of the theory of objects

in the signature sigma is going to be isomorphic to this pre-sheaf topos, we're going to have that every classifying topos is the topos of sheaves on an internal locale of this pre-sheaf topos. So that's the sort of motivation for what we're going to do next. We've

seen that whenever we have something that's localic over another topos, we're going to get an internal locale. And here, we're going to see that we actually get quite a nice description for the internal locale corresponding to a classifying topos of a theory T. Now, obviously since

every Got and Dick topos is a classifying topos of some theory, we're going to have that we're able to perform this construction for every topos. So let's just review our bridge in this restricted context. We have as the unifying notion topos as being localic over this pre-sheaf topos. And this is going to correspond to

two notions. On the one hand, the geometric notion of internal locales of this pre-sheaf topos, and on the other hand, the notion of geometric theories in a signature sigma.

We already appreciate what's going on with this bridge, but we need to sort of understand this bridge as well and how they interact.

So yeah, in order to do that, I'm just going to quickly recap some of the stuff from LeFouge's lecture earlier. It's not last week. It is last week. It's not this week. So at the end of last week, I'm going to recall some of the notions from syntactic sites for a geometric

theory. So for a geometric theory T, we can take the syntactic category, which has its objects, the formulae in that context, and the arrows between two formulae in context are going to be provable equivalence classes of formulae theta, such that, and then we have

these sequence holding. And these sequence, as LeFouge explained, just express the fact that theta is the graph of a function. So that's the usual definition of a syntactic category, and its syntactic topology has this description that the SID is covering,

if and only if we have this disjunction of existential statements being satisfied.

And then it's very well known that the classifying topos of the theory T is going to be the sheaves on this site with this topology. And it's also going to be important later, but we'll see how we can reconstruct it, that the topology is sub-canonical. So that's the syntactic site,

but, and so it's going to be, the classifying topos is going to be localic over the pre-sheaf topos involving the sorts and the signature. And so we need to describe what the sort of internal locale is going to look like.

And for that, I'm going to introduce this notion of a substitute of syntactic sites. So here, given our geometric theory, we're going to give it an internal locale of the pre-sheaf topos. So it's going to be a functor from the opposite of sorts to locales.

And we're going to associate with every context, every string of variables X, we're going to associate it to the locale given by the formulate in that context ordered by

syntactic proof. And whenever we have a relabeling, we're going to send that to the locale with corresponding frame homomorphism given by relabeling under the arrow sigma.

So here in this notation, the frame homomorphism corresponding to us locale morphism is going to send formulate psi in context Y to the formula in context X, where we substitute every instance of the variable Y by, sorry, every instance of say,

yi in this vector Y, we're going to substitute for yi sigma of yi, which is now going to be a variable in this context. And since we assume all of our context to be disjoint,

there's no issues with, that there's no issues in the order in which we relabel the variables. So this is going to be our associated internal locale. How do we know that it's an internal locale? It's an internal locale because of this pre-chief topos and the Beck-Cheverly

and Frobenius conditions basically are saying that existential quantification behaves well with substitution. They're quite easy to show. And the second remark I want to make is that the

left and right joints, oh, I mean, this is why Beck-Cheverly and Frobenius hold is that the left and right joints of our frame homomorphism are given by existential quantification and universal quantification. So this is the,

yeah, and so we have this internal locale and we're now going to take internal sheaves on that. And we're hoping that the internal sheaves are going to be closely related to the classifying

topos and indeed we're going to see that they are. So yes, when we take the relative construction, when we take the Grottendijk construction of this internal locale, which you can refer back to Olivia's lectures for the definition of this category.

But in this particular instance, we get a very nice description that it's going to be objects formulating context and the arrows in this category are going to be relabelling some variables. Yeah, so if we've got an arrow between phi in context X and psi in context Y

is going to be a relabelling in the other direction such that we have this sequent holding in our theory. And then when we take the induced topology, because

every internal locale has a induced topology coming with it, we end up with a family of in this category being covering if and only if we have this sequent holding.

And so because this is the description of the Grottendijk construction and the induced topology, we have that the sheaves on this internal locale is going to be equal to the sheaves on

this. It looks very much like the usual syntactic category, just that we've got the same objects, but we've got a lot fewer arrows. And sometimes our arrows will be identified. Oh, and I should also mention that this topology is generated by two species of

covering families. And so this corresponds to the fact that we've got horizontal and vertical covering data coming in from our relative toposphere.

And so yes, so indeed we end up with this site being a dense, sorry, having a dense morphism of sites to the usual syntactic site. And the morphism of sites is going to be given by this functor eta, which sends a formula in context to itself. And it's going to send

a relabeling to this provably functional formula here. So I'm claiming that this is a dense morphism of sites. And so if that's the case, then as a corollary, we get that this is a alternative description for the site of a classifying topos of the theory T.

So just to recall what a dense morphism of sites is, it's a function, sorry, a functor from C to D satisfying these conditions. S is J covering if and only if its image is K covering.

For every D, we have a K covering family of morphisms to D. And whenever we have an arrow between F of C1 and F of C2 that it might not necessarily come in the image of F,

then we want to show that it can be, it's densely generated by arrows in the image of F. And whenever we have two arrows being identified, this is the fourth condition, then whenever we have two arrows being identified by F, then there exists a J covering family of

arrows which exhibit their equality. And so when we have a dense morphism of sites, then we've got an equivalence of categories. So let's show that eta is indeed a dense morphism of sites. So the first one is immediate by definition because the

the Groton-Dick topologies are so similar. The second condition that it has a covering sieve onto every object follows immediately because it's subjective on objects. It's the next two which are less immediate. So let's suppose we have an arrow coming from a provably

functional formula in our syntactic category, which might not necessarily just be a relabeling variables. We're going to consider the diagram here where we take the

formula witnessing this provably functional formula. And now we have, due to all of the sequence that a provably functional formula has to satisfy, we have an arrow going to x pi.

And its composite, we can form the composite as LeFouge showed us in the previous series of lectures, thusly. And now we just need to show that we need to show that this is

coming from our substitutive syntactic site is dense, and this is also coming from our substitutive syntactic site. But this is immediate from all of the extra sequence that provably functional formulae have to satisfy. So this arrow is covering because

we have this secret holding. And this arrow is in the image of eta by the equivalence of these two formulae. And for the final condition, if we've got two relabelings

such that eta associates the two of them, then we're going to have that phi proves that sigma of yi is equal to tau yi for each yi in our context. And so now we need to find a series of, we need to find a covering family that witnesses this

quality. But this comes from this commutative diagram here, where this is the co-equalizer, because of course all of these relabelings go in the opposite

direction. This is the co-equalizer of these two relabelings. And this is the projection. This is the map given by projection from this to the co-equalizer. And we want to show that it's a covering arrow. But the required sequence, namely this,

can be proved easily from the fact that since these two arrows up here are identified, that we have this sequence holding for every yi in our context. So we do indeed have a, in conclusion, we do indeed have a dense morphism of sites,

which is nice because now we have a nice way of talking about what the syntactic site is in terms of a localic morphism. And so just quickly, I want to give some

verifications of previously known results. So for example, if we've got, these are results from theory sites and topices, if we've got T dash being a localic expansion of another theory T, then these are both localic expansions of the empty theory on the

sorts of the signature. And so being a localic expansion, we end up with a morphism of locales, which we can construct very in a hands-on way. We get a morphism of locales, which is internal

to the presheaf topos, sorts on sigma, intersets. And so because we've got a morphism of internal locales, we end up with a localic morphism between the two topos.

And so we verify our motivating result from earlier, but potentially more interestingly, a quotient theory T dash of another theory T is going to be a theory in the, yeah, this is a definition, is a theory in the same signature that proves all of the axioms

of T. And now we're able to sort of recognize the other headline result from theory sites and topos, but there's a correspondence between quotient theories and subtopoi. And the,

I mean, there's more work going on here than is immediately apparent on the page, but we can appreciate where the correspondence is coming from, but subtopoi of a classifying topos

are going to correspond to inclusions of internal sublocals, which in turn are going to correspond to quotient theories. And another result, you, which was, I believe, Joyeux, well, first of all, it appears in Joyeux and Tierney,

and secondly, Joyeux mentioned it at his talk at the topos at IHES, that you can, since we've, since we have that every theory is localic over the,

this pre-Chief topos here, we can use the fact that every theory is Marita equivalent to the, to a theory with a single sort to get that every theory is localic over the object classifier, which is a very nice result that, yes, as mentioned, originally appeared in Joyeux and Tierney.

And so finally, I want to go all the way back to the beginning, where I mentioned that we can think about topos as telling us the information that we're missing out. And so we had this substitute of syntactic site. Now, where do the

provably functional formulae come in? They come in when we take a syntactic, yes, they come in here where the syntactic category is going to be the full subcategory of the representables in the classifying topos. And then additionally, the syntactic topology is

going to be the restriction of the canonical topology. So the way to see this is that because the topology is subcanonical, CT has to be a full subcategory, and indeed, it has to have the same objects as the representables. So this is where our extra arrows are being added. They're being added on the topos theoretic level.

And yeah, indeed, we could also go the other way. And if we didn't know that the topology was subcanonical, we could define the syntactic category as being the full subcategory of representables. And then we would have that the induced topology,

the syntactic topology would then have to be subcanonical. And yeah, and then in Olivia's in an elementary way. So yeah, thank you for listening. That's my talk up. Thank you very much.