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: theory: category theory

Topic: Overtness of the localic group of automorphisms on a set A

Christopher Townsend (Apr 23 2026 at 15:33):

It is well known that if A and B are two sets then we can form their localic function space: A^B. That is, the exponential exists in the category of locales, treating A and B as discrete locales. It is also known that A^B is overt (i.e. !:A^B->1 is an open locale map). (For example, see the remarks after Proposition 2 of 5.2 in Joyal and Tierney 1984.)

I can follow the argument and it is very elegant, as it relies on the simple fact that provided you take only quotients using non-empty covers then being open descends (and certainly the free suplattice on a poset is the frame of an open locale).

On the other hand we can construct A^B by applying (_)^B to an equaliser in Loc: A>->S^{A}=>S^{AxA}xS. Then the opens of A^B are a quotient of UF(AxB), where U is the set of upper subsets and F is the set of finite subsets (this is just an explicit description of the opens of S^{AxB}, here S is the Sierpinski locale). But in this case the nice argument cannot be applied to derive the fact that A^B is overt/open simply from the fact that S^{AxB} is overt. (To see this examine the case B=1.)

These facts are annoying me. I find the approach via S^{AxB} much more intuitive, but to derive that A^B is therefore overt/open seems to need me to translate it back to the Joyal and Tierney way of looking at things. And, as per the title, I want to specialise the approach to isolate the automorphisms on A (a localic group) and so provide a proof that it is open (which again, I know is true ... but ... )

Is there anyone who has thought about this specific query? Anything in the literature that might iron things out?

Thanks, and if this isn't the right sort of Q for this forum please, mods, feel free to move/delete.

Graham Manuell (Apr 23 2026 at 16:43):

One thing I'll note is that since $X^Y$ isn't generally compact when $X$ and $Y$ are compact Hausdorff, any proof of this cannot respect the duality between opens and closeds. This might explain why there isn't an obvious clean proof.

But also, I'm not convinced this result is true? Take $A$ to be the empty set and $B$ to be a subterminal. It's definitely true if $A$ is inhabited and $B$ has decidable equality. Maybe there is a somewhat more general result, but I do not know it. (And this counterexample suggests some additional restrictions at least are necessary.)

David Michael Roberts (Apr 23 2026 at 23:27):

But also, I'm not convinced this result is true?

Do you mean the result that A^B is overt, or that the exponential can be constructed in both the ways Christopher describes?

Graham Manuell (Apr 24 2026 at 06:39):

Oh, sorry. It can be constructed that way. I just don't think it's always overt.

Graham Manuell (Apr 24 2026 at 07:10):

Christopher will understand, but I'll say more for other people. If $P = \{* \mid p\} \hookrightarrow 1$ for a truth value $p$ then the exponential $0^P$ should be the closed complement of P in 1. Since 1 is discrete, every overt sublocale of it is open. But any open sublocale of a set will be a set, which forces $p \vee \neg p$. Thus, the result implies excluded middle.

David Michael Roberts (Apr 24 2026 at 07:15):

OK, thanks!

Christopher Townsend (Apr 24 2026 at 10:16):

Ah, yes, this rings true and the way I was seeing things seemed to be forcing A to be inhabited; but I had thought that a more careful examination would remove this; so thanks for the specific pointer. However, it was more about easing proof complexity in terms of not having to change the presentation in order to get at the result (let's call the result: A^B is overt if A is inhabited and A and B are discrete).

Graham Manuell (Apr 24 2026 at 12:01):

Do you know that it is true even for inhabited $A$ without restricting $B$ to have decidable equality? It could be, but it's not obvious to me.

Christopher Townsend (Apr 24 2026 at 16:06):

Graham Manuell said:

Do you know that it is true even for inhabited $A$ without restricting $B$ to have decidable equality? It could be, but it's not obvious to me.

Well, how could I put it, I think so, but I haven't written out the proof clearly enough to be sure. I think the proof is that you put a coverage on the poset of partial functions from B to A (where partial means finite domain); then the coverage is non-empty always and so the thing being presented is open. However, I've been so absorbed in various variations on the theme of trying to work out how to obtain that coverage from S^{AxB} that I sort of lost track as to whether I was in fact assuming B is decidable in the original set up ...