Presenting quotient locales

TL;DR

This paper develops methods to derive presentations of quotient locales from given locale presentations, enabling better understanding and construction of quotient structures in locale theory.

Contribution

It introduces simple procedures for obtaining presentations of open, proper, and general quotient locales from parent locale presentations.

Findings

Presented procedures for quotient locale presentations

Applied methods to derive circle presentations from reals and intervals

Proved results using suplattice, preframe, and dcpo coverage theorems

Abstract

It is often useful to be able to deal with locales in terms of presentations of their underlying frames, or equivalently, the geometric theories which they classify. Given a presentation for a locale, presentations for its sublocales can be obtained by simply appending additional relations, but the case of quotient locales is more subtle. We provide simple procedures for obtaining presentations of open quotients, proper quotients or general triquotients from presentations of the parent locale. The results are proved with the help of the suplattice, preframe and dcpo coverage theorems and applied to obtain presentations of the circle from ones for the reals and the closed unit interval.