The double powerlocale and exponentiation: A case study in geometric logic

Steven Vickers

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)
30 Downloads (Pure)


If X is a locale, then its double powerlocale PX is defined to be PU(PL(X)) where PU and PL are the upper and lower powerlocale constructions. We prove various results relating it to exponentiation of locales, including the following. First, if X is a locale for which the exponential S^X exists (where S is the Sierpinski locale), then PX is an exponential S^(S^X). Second, if in addition W is a locale for which PW is homeomorphic to S^X, then X is an exponential S^W. The work uses geometric reasoning, i.e. reasoning stable under pullback along geometric morphisms, and this enables the locales to be discussed in terms of their points as though they were spaces. It relies on a number of geometricity results including those for locale presentations and for powerlocales.
Original languageEnglish
Pages (from-to)372-422
Number of pages51
JournalTheory and Applications of Categories
Issue number13
Publication statusPublished - 1 Jan 2004


Dive into the research topics of 'The double powerlocale and exponentiation: A case study in geometric logic'. Together they form a unique fingerprint.

Cite this