# Presenting quotient locales

Graham Manuell  CMUC, Department of Mathematics, University of Coimbra,
Coimbra, Portugal<EMAIL_ADDRESS>
(Date: July 2023)

###### 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 $\mathbb{R}$ and $[0,1]$.

###### Key words and phrases:

perfect map, lax proper map, semi-open map, subframe, classifying locale

###### 2010 Mathematics Subject Classification:

06D22, 54B15

The author acknowledges financial support from the Centre for Mathematics of
the University of Coimbra (UIDB/00324/2020, funded by the Portuguese
Government through FCT/MCTES)

##  0\. Introduction

An advantage of the pointfree approach to topology is the ability to present
frames by generators and relations. This can also be interpreted as describing
a locale by giving axioms for a geometric theory which it classifies.

Since sublocales correspond to quotient frames, presentations for them the be
found by simply adding additional relations to the a presentation for the
parent frame. However, there is no such simple relationship between
presentations of a frame and presentations of its subframes, and so quotient
locales can be more difficult to deal with with this approach.

The aim of this paper is to give simple procedures for turning a presentation
of a locale into a presentation of one of its quotients in a number of
important cases. These include open quotients, proper quotients and
triquotients, as well as certain ‘lax’ variants of these.

While the results are straightforward applications of the coverage theorems
stated below, I have not seen these results mentioned before and I hope that
this paper will be a useful reference for dealing with quotients. The last
section provides a number of examples to demonstrate the how the results would
be used in practice and to showcase their utility.

##  1\. Background

We denote the category of frames by $\mathbf{Frm}$ and its opposite category —
the category locales — by $\mathbf{Loc}$. To avoid confusion we will
distinguish notationally between locales and their corresponding frames: we
write $\mathcal{O}X$ for the underlying frame of the locale $X$ and
$f^{*}\colon\mathcal{O}Y\to\mathcal{O}X$ for the frame homomorphism
corresponding to the locale map $f\colon X\to Y$.

The category $\mathbf{Frm}$, and thus $\mathbf{Loc}$, has a natural order-
enrichment given by the usual pointwise ordering on frame homomorphisms. Thus
it makes sense to consider not only locale coequalisers, but also
_coinserters_. The coinserter of a parallel pair $f,g\colon A\rightrightarrows
B$ is the initial map $q\colon B\to C$ such that $qg\leq qf$. In this paper we
use the convention where the lower path in the diagram is the smaller
composite.

A _dcpo_ is a poset admitting joins of directed subsets. To emphasise that a
join $\bigvee S$ is of a directed subset we we will use the notation
$\operatorname*{\bigvee{}^{\\!\uparrow}_{\hskip 2.2604pt}}S$. The usual
morphisms between dcpos preserve these directed joins and are called Scott-
continuous functions. The forgetful functor from $\mathbf{Frm}$ to
$\mathbf{DCPO}$ factors through both the category of suplattices
$\mathbf{Sup}$ and the category of preframes $\mathbf{PreFrm}$. Recall that a
suplattice is a poset which admits all joins and a suplattice homomorphism is
a join-preserving map between these, while a preframe is a dcpo with finite
meets and a preframe homomorphism is a Scott-continuous $\wedge$-semilattice
homomorphism.

Of course, frames and suplattices can be presented by generators and
relations, but so can preframes (see [5]) and dcpos (see [14]). We write
$\langle G\mid R\rangle_{\mathcal{A}}$ for the object of the category
$\mathcal{A}$ presented by the generators from $G$ and the relations from $R$
(which we view as a set of formal equalities and inequalities between elements
of the free structure on $G$). For case the $\mathcal{A}=\mathbf{Frm}$ we will
omit the subscript when there is no chance of confusion.

Sometimes it is useful to take the generators to have more structure than a
mere set. For instance, if $G$ has the structure of a $\wedge$-semilattice,
then we can use the free frame on the $\wedge$-semilattice $G$ to form the
presentation. This is equivalent to taking the free frame on the set $G$ and
adding in relations to force the finite meets in the presented frame to agree
with the finite meets in $G$. To indicate we are viewing $G$ as a
$\wedge$-semilattice and not just a set we will write such a presentation as
$\langle G\text{ $\wedge$-semilattice}\mid R\rangle$.

We now recall some theorems relating different kinds of presentations which
will be crucial for proving our results. See [13, 14] for further details.

######  Definition 1.1.

Let $G$ be a $\wedge$-semilattice. We will call $\langle G\text{
$\wedge$-semilattice}\mid R\rangle_{\mathbf{Frm}}$ a _$\mathbf{Sup}$ -type
frame presentation_ if every relation in $R$ is of the form $\bigvee
A\leq\bigvee B$ and furthermore, when $\bigvee A\leq\bigvee B$ is a relation,
then so is $\bigvee_{a\in A}a\wedge c\leq\bigvee_{b\in B}b\wedge c$ for each
$c\in G$.

######  Theorem 1.2 (Suplattice coverage theorem [1]).

For a $\mathbf{Sup}$-type frame presentation given by $G$ and $R$, there is an
order isomorphism

$\langle G\text{ $\wedge$-semilattice}\mid R\rangle_{\mathbf{Frm}}\cong\langle
G\text{ poset}\mid R\rangle_{\mathbf{Sup}}.$

######  Definition 1.3.

Let $G$ be a $\vee$-semilattice. We will call $\langle G\text{
$\vee$-semilattice}\mid R\rangle_{\mathbf{Frm}}$ a _$\mathbf{PreFrm}$ -type
frame presentation_ if every relation in $R$ is of the form
$\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha}}\bigwedge
A_{\alpha}\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}\bigwedge
B_{\beta}$ where each $A_{\alpha}$ and $B_{\beta}$ is finite, and if
furthermore, when $\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha}}\bigwedge
A_{\alpha}\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}\bigwedge
B_{\beta}$ is a relation, then so is
$\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha}}\bigwedge_{a\in
A_{\alpha}}(a\vee
c)\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}\bigwedge_{b\in
B_{\beta}}(b\vee c)$ for each $c\in G$.

######  Theorem 1.4 (Preframe coverage theorem [5]).

For a $\mathbf{PreFrm}$-type frame presentation given by $G$ and $R$, there is
an order isomorphism

$\langle G\text{ $\vee$-semilattice}\mid R\rangle_{\mathbf{Frm}}\cong\langle
G\text{ poset}\mid R\rangle_{\mathbf{PreFrm}}.$

######  Definition 1.5.

Let $G$ be a (bounded) distributive lattice. We will call a presentation
$\langle G\text{ dist.\ lattice}\mid R\rangle_{\mathbf{Frm}}$ a
_$\mathbf{DCPO}$ -type frame presentation_ if every relation in $R$ is of the
form $\operatorname*{\bigvee{}^{\\!\uparrow}_{\hskip
2.2604pt}}A\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{\hskip 2.2604pt}}B$ and
furthermore, when $\operatorname*{\bigvee{}^{\\!\uparrow}_{\hskip
2.2604pt}}A\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{\hskip 2.2604pt}}B$ is
a relation, then so are $\operatorname*{\bigvee{}^{\\!\uparrow}_{a\in
A}}a\wedge c\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{b\in B}}b\wedge c$ and
$\operatorname*{\bigvee{}^{\\!\uparrow}_{a\in A}}(a\vee
c)\leq\operatorname*{\bigvee{}^{\\!\uparrow}_{b\in B}}(b\vee c)$ for each
$c\in G$.

######  Theorem 1.6 (Dcpo coverage theorem [14]).

For a $\mathbf{DCPO}$-type frame presentation given by $G$ and $R$, there is
an order isomorphism

$\langle G\text{ dist.\ lattice}\mid R\rangle_{\mathbf{Frm}}\cong\langle
G\text{ poset}\mid R\rangle_{\mathbf{DCPO}}.$

######  Remark 1.7.

The generators in a $\mathbf{Sup}$-type presentation form a _base_ of opens
for the topology in question. In a $\mathbf{PreFrm}$-type presentation, it is
perhaps most intuitive to think of the elements of the frame, not as being
_opens_ , but as _closed_ sublocales with the reverse order. The generators
then give a set of ‘basic’ closed sublocales which are closed under finite
meets and generate all the closed sublocales under finite joins and downward-
directed meets. For $\mathbf{DCPO}$-type presentations either viewpoint is
appropriate.

######  Remark 1.8.

The restriction to $\mathbf{Sup}$-type, $\mathbf{PreFrm}$-type or
$\mathbf{DCPO}$-type presentations does not really constrain us, since it is
easy to turn any presentation into one of the appropriate form by simply
closing the generators under meets or joins as appropriate, manipulating the
relations into the appropriate form, and adding any additional relations
needed for meet- or join-stability.

Finally, let us consider the various kinds of maps we will encounter in this
paper. A locale map $f\colon X\to Y$ is said to be _open_ if
$f^{*}\colon\mathcal{O}Y\to\mathcal{O}X$ has a left adjoint
$f_{!}\colon\mathcal{O}X\to\mathcal{O}Y$ satisfying the so-called Frobenius
condition

$f_{!}(a\wedge f^{*}(b))=f_{!}(a)\wedge b.$

This is equivalent to the map $f^{*}$ being a complete Heyting algebra
homomorphism. Note that as a left adjoint $f_{!}$ preserves joins and is thus
a suplattice homomorphism. We say $f$ is an _open quotient_ if $f$ is open and
epic — or equivalently, if $f$ is open and $f^{*}$ is injective, in which case
$f_{!}$ is a left inverse of $f^{*}$ in $\mathbf{Sup}$.

A locale map $f\colon X\to Y$ such that $f^{*}$ has a left adjoint that does
not necessarily satisfy the Frobenius condition is called _semi-open_. We will
call epic semi-open maps _semi-open quotients_. These are arguably not true
quotient maps, since they need not be regular epimorphisms. However, they do
appear as coinserters, and since many of our results will not need the
Frobenius conditions, they are a natural class of maps to condition in this
setting.

A map $f\colon X\to Y$ is called _proper_ if the right adjoint $f_{*}$ of
$f^{*}$ is Scott-continuous and satisfies the Frobenius condition

$f_{*}(a\vee f^{*}(b))=f_{*}(a)\vee b.$

Note that since right adjoints preserve meets, if $f$ is proper then $f_{*}$
is a preframe homomorphism. An epic proper map is called a _proper quotient_.
In this case $f_{*}$ is a left inverse to $f^{*}$ in $\mathbf{PreFrm}$.
Similarly to above a map $f$ is said to be _semi-proper_ (or sometimes _lax
proper_ or _perfect_) if $f_{*}$ preserves directed joins, but does not
necessary satisfy the Frobenius condition. It will be useful to call epic
semi-proper maps _semi-proper quotients_.

A locale map $f\colon X\to Y$ is said to be a _triquotient surjection_ if
there exists a dcpo morphism $f_{\\#}\colon\mathcal{O}X\to\mathcal{O}Y$,
called a _triquotiency assignment_ , satisfying $f_{\\#}(a\wedge
f^{*}(b))=f_{\\#}(a)\wedge b$ and $f_{\\#}(a\vee f^{*}(b))=f_{\\#}(a)\vee b$.
These generalise open and proper quotients (taking $f_{!}$ and $f_{*}$ as the
triquotiency assignments respectively). The map $f_{\\#}$ is automatically a
left inverse of $f^{*}$ in $\mathbf{DCPO}$. See [8] for details.

##  2\. Working with locale quotients

If $q\colon X\twoheadrightarrow Y$ is a semi-open quotient, then the composite
of $q^{*}q_{!}$ gives a suplattice endomorphism on $\mathcal{O}X$. In fact,
this is a closure operator and $\mathcal{O}Y$ is isomorphic to its fixed
points. Moreover, the fixed points of any join-preserving closure operator on
$\mathcal{O}X$ form a frame (since they are closed under all meets and joins)
and give rise to a semi-open quotient. Thus, these will be a useful way for us
to specify the quotient locale $Y$ without already knowing the precise form of
$Y$. The map $q$ will be _open_ if and only if its corresponding closure
operator $j$ satisfies $j(a)\wedge j(b)\leq j(a\wedge j(b))$.

If $q\colon X\twoheadrightarrow Y$ is a semi-proper quotient, then
$q^{*}q_{*}$ similarly gives a preframe endomorphism and interior operator on
$\mathcal{O}X$. As before, $\mathcal{O}Y$ is isomorphic to its fixed points
and the fixed points of any such operator form a frame and give a semi-proper
quotient. The quotient is proper if and only if the interior operator
satisfies $p(a)\vee p(b)\geq p(a\vee p(b))$.

It is shown in [6] that if $p_{1},p_{2}\colon R\rightrightarrows X$ are open
morphisms and are the domain and codomain maps of a localic groupoid (or in
particular, an equivalence relation), then their coequaliser $q\colon
X\twoheadrightarrow Y$ is an open quotient and $\mathcal{O}Y$ is given by the
fixed points of the closure operator $(p_{1})_{!}p_{2}^{*}$ (or
$(p_{2})_{!}p_{1}^{*}$). Furthermore, even if only the upper (domain) map
$p_{1}$ map is open and they form a localic category (or in particular, a
preorder), the coinserter is a semi-open quotient and the corresponding
closure operator is still $(p_{1})_{!}p_{2}^{*}$. Dual results with proper
maps replacing open maps are given in [10, 7]. (There it is only stated for
internal equivalence relations and preorders, but the proofs work equally well
for localic groupoids and categories.) This time the _lower_ map $p_{2}$
should be proper and $\mathcal{O}Y$ is given by the fixed points of the
interior operator $(p_{2})_{*}p_{1}^{*}$.

In fact, we can obtain similar results in a more general situation. Suppose
the following diagram is a coinserter in $\mathbf{Loc}$.

$R$$X$$Y$$f$$g$$q$

Since the forgetful functor from $\mathbf{Frm}$ to $\mathbf{Pos}$ creates
weighted limits, $\mathcal{O}Y$ can be identified with
$\\{u\in\mathcal{O}X\mid g^{*}(u)\leq f^{*}(u)\\}$. If $f$ is semi-open, then
$g^{*}(u)\leq f^{*}(u)\iff f_{!}g^{*}(u)\leq u$ and so $\mathcal{O}Y$ consists
of the _pre-fixed points_ of the suplattice endomorphism $f_{!}g^{*}$ on
$\mathcal{O}X$. Similarly, if $g$ is semi-proper, then $\mathcal{O}Y$ consists
of the _post-fixed points_ of the preframe endomorphism $g_{*}f^{*}$.

######  Remark 2.1.

If the above is a _reflexive_ coinserter (with common section $r$), then
$g_{*}f^{*}=r^{*}g^{*}g_{*}f^{*}\leq r^{*}f^{*}=\mathrm{id}$ and so
$g_{*}f^{*}$ is automatically deflationary. Similarly, if it exists,
$f_{!}g^{*}$ is automatically inflationary. So in this case the coinserter is
given by the _fixed points_ of $f_{!}g^{*}$ or $g^{*}f_{*}$, not just the pre-
fixed points or post-fixed points.

######  Proposition 2.2.

If $j$ is a suplattice endomorphism on a frame $\mathcal{O}X$, then the pre-
fixed points of $j$ form a subframe $\mathcal{O}Y$ of $\mathcal{O}X$. The
frame inclusion $q^{*}\colon\mathcal{O}Y\hookrightarrow\mathcal{O}Y$ has a
left adjoint and thus corresponds to a semi-open locale quotient. The
associated closure operator is given by $\bigvee_{n=0}^{\infty}j^{n}$.

Consequently, given a coinserter diagram as above, if $f$ is semi-open then so
is $q$.

###### Proof.

The map $j\vee\mathrm{id}$ is an inflationary suplattice endomorphism, the
fixed points of which coincide with the pre-fixed points of $j$. As in the
Kleene fixed point theorem, we find the map $\bigvee_{n=0}^{\infty}j^{n}$ is a
join-preserving closure operator, which again has the same fixed points. This
provides a left adjoint to the inclusion
$q^{*}\colon\mathcal{O}Y\hookrightarrow\mathcal{O}X$.

Now consider the coinserter where $f$ is semi-open. The result follows by
applying the above to the suplattice endomorphism $f_{!}g^{*}$. ∎

######  Remark 2.3.

Since $g^{*}(u)=f^{*}(u)$ whenever $g^{*}(u)\leq f^{*}(u)$ and $f^{*}(u)\leq
g^{*}(u)$, it follows that if both $f$ and $g$ are semi-open then their
_coequaliser_ is given by the pre-fixed points of $f_{!}g^{*}\vee g_{!}f^{*}$.
Furthermore, if there is a ‘symmetry’ map $s\colon R\to R$ such that $g=fs$
(as in the case of a localic groupoid) then it can be shown that the
coequaliser and coinserter coincide.

######  Remark 2.4.

The fact that the coequaliser of semi-open maps is semi-open is also immediate
from the fact that equalisers in the category of complete lattices and agree
with those in $\mathbf{Frm}$ (since they are both computed as in
$\mathbf{Set}$). Similarly, we see that the coequaliser of open maps is open
by taking the equaliser in the category of complete Heyting algebras.

The case of proper quotients is somewhat more subtle.

######  Example 2.5.

Let $N$ be $\mathbb{N}$ equipped with the order topology for the reverse of
the usual order (i.e. opens are downsets with respect to the usual order) and
let $s\colon N\to N$ be the successor function. This map is proper. Then the
coequaliser and the coinserter of $s$ and $\mathrm{id}_{N}$ (with
$\mathrm{id}_{N}$ the lower map) are both the terminal locale. But the unique
map ${!}\colon N\to 1$ is proper if and only if it is semi-proper if and only
if $N$ is compact and it is clear that $N$ is not compact. Thus, a coequaliser
or coinserter of proper maps need not even be semi-proper. ∎

The problem is that we cannot iterate the preframe endomorphism to obtain an
idempotent one as we did for the suplattice endomorphism in Proposition 2.2.
The following proposition gives conditions under which idempotence is
automatic and so we do obtain a semi-proper quotient.

######  Proposition 2.6.

Consider a coinserter diagram as above and suppose $g$ is _proper_. Further
suppose that there is a locale map $t\colon R\times_{X}R\to R$ such that
$g\pi_{2}\leq gt$ and $ft\leq f\pi_{1}$ (for example, the transitivity map of
an internal preorder or the composition of an internal category). Then the
coinserter morphism $q$ is semi-proper and $g_{*}f^{*}\wedge\mathrm{id}$ is
the associated interior operator.

$R\times_{X}R$$R$$X$$R$$X$$X$$\pi_{1}$$\pi_{2}$$g$$f$$f$$g$$R$$f$$g$$t$$\leq$

$\leq$

###### Proof.

Since $g$ is proper, so is the pullback projection $\pi_{2}$. Moreover, we
have the Beck–Chevalley condition: $f^{*}g_{*}=(\pi_{2})_{*}\pi_{1}^{*}$.
Thus,

$\displaystyle g_{*}f^{*}g_{*}f^{*}$
$\displaystyle=g_{*}(\pi_{2})_{*}\pi_{1}^{*}f^{*}$ $\displaystyle\geq
g_{*}(\pi_{2})_{*}t^{*}f^{*}$ $\displaystyle\geq
g_{*}(\pi_{2})_{*}t^{*}g^{*}g_{*}f^{*}$ $\displaystyle\geq
g_{*}(\pi_{2})_{*}\pi_{2}^{*}g^{*}g_{*}f^{*}$ $\displaystyle\geq
g_{*}g^{*}g_{*}f^{*}$ $\displaystyle=g_{*}f^{*}.$

Now $g_{*}f^{*}\wedge\mathrm{id}$ is a deflationary preframe endomorphism on
$\mathcal{O}X$ and by the above we have
$(g_{*}f^{*}\wedge\mathrm{id})^{2}=g_{*}f^{*}g_{*}f^{*}\wedge
g_{*}f^{*}\wedge\mathrm{id}=g_{*}f^{*}\wedge\mathrm{id}$ and hence
$g_{*}f^{*}\wedge\mathrm{id}$ is an interior operator. Finally, the elements
of $\mathcal{O}Y$ are precisely the post-fixed points of $g_{*}f^{*}$ and thus
the fixed points of $g_{*}f^{*}\wedge\mathrm{id}$. ∎

######  Remark 2.7.

If $g$ is only semi-proper, then a similar result holds if the domain of $t$
is replaced with the comma object $g/f$.

######  Remark 2.8.

If in the above proposition $f$ and $g$ are both proper, $g\pi_{2}=gt$ and
$f\pi_{1}=ft$, then their _coequaliser_ is given by the fixed points of the
interior operator $g_{*}f^{*}\wedge f_{*}g^{*}\wedge\mathrm{id}$. Moreover,
the resulting quotient map is proper. Finally, if there is a symmetry map as
in Remark 2.3 the coequaliser and coinserter coincide.

More general than proper and open quotients is the case of triquotients. While
there is unfortunately no good result relating these to coequalisers, we can
still represent them by idempotent dcpo endomorphisms in analogy to the
interior and closure operators discussed above. In fact, just as proper and
open quotients can be generalised to semi-proper and semi-open quotients, we
consider general locale maps $q\colon X\twoheadrightarrow Y$ whose
corresponding frame map $q^{*}$ has a Scott-continuous retraction $q_{\\#}$,
but without any additional assumptions. These do not seem to have an
established name, but one might call them _semi-triquotient_ maps or perhaps
even _sesqui-quotient_ maps.

If $q\colon X\twoheadrightarrow Y$ is a semi-triquotient, the map
$q^{*}q_{\\#}$ is an idempotent dcpo endomorphism on $\mathcal{O}X$, whose
poset of fixed points is isomorphic to $\mathcal{O}Y$. This satisfies
$q^{*}q_{\\#}(1)=1$, $q^{*}q_{\\#}(0)=0$, $q^{*}q_{\\#}(a)\wedge
q^{*}q_{\\#}(b)\leq q^{*}q_{\\#}(q^{*}q_{\\#}(a)\wedge q^{*}q_{\\#}(b))$ and
$q^{*}q_{\\#}(a)\vee q^{*}q_{\\#}(b)\geq q^{*}q_{\\#}(q^{*}q_{\\#}(a)\vee
q^{*}q_{\\#}(b))$. Moreover, the fixed points of any dcpo endomorphism $e$ on
a frame $\mathcal{O}X$ satisfying these conditions form a subframe of
$\mathcal{O}X$ whose inclusion corresponds to a semi-triquotient with dcpo
retraction $e$.

An idempotent dcpo endomorphism $e$ corresponds to a _triquotient_ if it
satisfies the stronger laws $e(a)\wedge e(b)\leq e(a\wedge e(b))$ and
$e(a)\vee e(b)\geq e(a\vee e(b))$, in addition to $e(1)=1$ and $e(0)=0$.

Finally, we note that by general categorical principles in all the cases above
the frame of fixed points of the suplattice, preframe or dcpo endomorphism
describing the quotient locale can be found not only as a subobject, but also
a quotient in the appropriate category. For example, the map
$q_{\\#}\colon\mathcal{O}X\twoheadrightarrow\mathcal{O}Y$ is the dcpo
coequaliser of $q^{*}q_{\\#}$ and $\mathrm{id}_{\mathcal{O}X}$. Thus,
$\mathcal{O}Y$ can be obtained as a dcpo quotient of $\mathcal{O}X$ by setting
$a\sim q^{*}q_{\\#}(a)$ for each $a$ in $\mathcal{O}X$ (or equivalently, for
each $a$ in some subset that generates $\mathcal{O}X$ under directed joins).

Similarly, if $j\colon\mathcal{O}X\to\mathcal{O}X$ is a join-preserving
closure operator, the suplattice quotient onto the frame of fixed points is
obtained by setting $j(a)\lesssim a$ for each $a$ in some base of
$\mathcal{O}X$. If $p\colon\mathcal{O}X\to\mathcal{O}X$ is a preframe
endomorphism and an interior operator, the preframe quotient is obtained by
setting $a\lesssim p(a)$ for each $a$ in some subset of $\mathcal{O}X$ which
generates $\mathcal{O}X$ as a preframe.

##  3\. Main results

While presenting quotients of locales is tricky in general, there is one case
where it is trivial. This is when the quotient $q\colon X\twoheadrightarrow Y$
has a section $s\colon Y\hookrightarrow X$. Then $Y$ is a sublocale of $X$ and
so we simply need to add the additional corresponding additional relations to
the presentation of $X$ in the usual way.

In the cases we will consider, we will not be quite so lucky to have a frame
homomorphism which is left inverse to $q^{*}$, but we will instead have
morphisms of suplattices, preframes or dcpos that will play the same role.

###  3.1. Presenting open quotients

We know that a semi-open quotient $q\colon X\twoheadrightarrow Y$ can be
specified by a join-preserving closure operator
$j\colon\mathcal{O}X\to\mathcal{O}X$ and that the map
$q_{!}\colon\mathcal{O}X\to\mathcal{O}Y$ is a suplattice quotient with kernel
congruence generated by $j(a)\lesssim a$.

Now suppose we have a presentation for $\mathcal{O}X$. Without loss of
generality, we may assume that this is a $\mathbf{Sup}$-type presentation
$\mathcal{O}X=\langle G\text{ $\wedge$-semilattice}\mid
R\rangle_{\mathbf{Frm}}$. We can then use the suplattice coverage theorem
(1.2) to obtain $\mathcal{O}X\cong\langle G\text{ poset}\mid
R\rangle_{\mathbf{Sup}}$.

Adding the relations from the suplattice quotient given by $q_{!}$ we obtain a
suplattice presentation for $\mathcal{O}Y$. We find $\mathcal{O}Y\cong\langle
G\text{ poset}\mid R,\ j(g)\leq g,\,g\in G\rangle_{\mathbf{Sup}}$. Note that
here the relations $j(g)\leq g$ can be understood purely in terms of
generators by writing each $j(g)$ as a join of generators in $\mathcal{O}X$.

We still need to turn this into a _frame_ presentation of $\mathcal{O}Y$. In
general if a suplattice $L$ happens to be a frame, then
$L\cong\langle\\{\lozenge a\mid a\in L\\}\text{ suplattice}\mid\lozenge 1=1,\
\lozenge a\wedge\lozenge b=\lozenge(a\wedge b),\,a,b\in
L\rangle_{\mathbf{Frm}}$, where the meet $a\wedge b$ is taken in $L$. In fact,
it suffices to only include (in addition to $\lozenge 1=1$) the relations
$\lozenge a\wedge\lozenge b=\lozenge(a\wedge b)$ for $a$ and $b$ restricted to
some base of $L$, since the remaining relations will follow from these ones by
taking joins and using the fact that $\lozenge(-)$ preserves the joins. In our
case generators $a,b$ in $\mathcal{O}X$ map to $q_{!}(a),q_{!}(b)$ in the
suplattice quotient and so taking the meet in $\mathcal{O}Y$ corresponds to
$j(a)\wedge j(b)$ in our presentation. Thus, combining this with the above
suplattice presentation, we have

$\displaystyle\mathcal{O}Y\cong\langle\\{\lozenge g\mid g\in G\\}\text{
poset}\mid{}$ $\displaystyle R,\ \lozenge j(g)\leq\lozenge g,\,g\in G,\
\lozenge 1=1,$ $\displaystyle\lozenge s\wedge\lozenge t=\lozenge(j(s)\wedge
j(t)),\,s,t\in G\rangle_{\mathbf{Frm}},$

where $\lozenge j(g)$ is defined to mean $\bigvee_{\alpha}\lozenge g_{\alpha}$
for $j(g)=\bigvee_{\alpha}g_{\alpha}$ and similarly, we interpret
$\lozenge(j(s)\wedge j(t))=\bigvee_{\sigma,\tau}\lozenge(g_{\sigma}\wedge
g_{\tau})$ for $j(s)=\bigvee_{\sigma}g_{\sigma}$ and
$j(t)=\bigvee_{\tau}g_{\tau}$ (where the meet is taken in the
$\wedge$-semilattice $G$).

Finally, note that the relation $\lozenge j(g)\leq\lozenge g$ follows from the
meet conditions by taking $s=1$ and $t=g$, and the inequalities from the poset
of generators then also follow from the meet condition by taking $s\leq t$. We
have arrived at the following result.

######  Proposition 3.1.

Suppose $\mathcal{O}X=\langle G\text{ $\wedge$-semilattice}\mid
R\rangle_{\mathbf{Frm}}$ is a $\mathbf{Sup}$-type presentation and let
$q\colon X\twoheadrightarrow Y$ be a semi-open quotient. Then

$\displaystyle\mathcal{O}Y\cong\langle\lozenge g,\,g\in G\mid{}$
$\displaystyle R,\ \lozenge 1=1,$ $\displaystyle\lozenge s\wedge\lozenge
t=\lozenge(q^{*}q_{!}(s)\wedge q^{*}q_{!}(t)),\,s,t\in
G\rangle_{\mathbf{Frm}},$

where we interpret $\lozenge(q^{*}q_{!}(s)\wedge
q^{*}q_{!}(t))=\bigvee_{\alpha,\beta}\lozenge(s_{\alpha}\wedge t_{\beta})$ for
specified representations $q^{*}q_{!}(s)=\bigvee_{\alpha}s_{\alpha}$ and
$q^{*}q_{!}(t)=\bigvee_{\beta}t_{\beta}$ in terms of generators.

If $q$ is an _open_ quotient then we can simply this further still.

######  Corollary 3.2.

Suppose $\mathcal{O}X=\langle G\text{ $\wedge$-semilattice}\mid
R\rangle_{\mathbf{Frm}}$ is a $\mathbf{Sup}$-type presentation and let
$q\colon X\twoheadrightarrow Y$ be an open quotient. Then

$\displaystyle\mathcal{O}Y\cong\langle\lozenge g,\,g\in G\mid{}$
$\displaystyle R,\ \lozenge 1=1,$ $\displaystyle\lozenge s\wedge\lozenge
t=\lozenge(s\wedge q^{*}q_{!}(t)),\,s,t\in G\rangle_{\mathbf{Frm}},$

where we interpret $\lozenge(s\wedge
q^{*}q_{!}(t))=\bigvee_{\beta}\lozenge(s\wedge t_{\beta})$ for specified
representation $q^{*}q_{!}(t)=\bigvee_{\beta}t_{\beta}$.

###### Proof.

Again, taking $s=1$ and $t=g$ gives the relation $\lozenge g=\lozenge
q^{*}q_{!}(g)$. Then the Frobenius condition gives $q^{*}q_{!}(s)\wedge
q^{*}q_{!}(t)=q^{*}q_{!}(s\wedge q^{*}q_{!}(t))$. Combining these we obtain
the meet relations given in Proposition 3.1 and the converse direction is
straightforward. ∎

######  Remark 3.3.

Our derived presentation can be understood as describing the quotient locale
$Y$ as a sublocale of the _lower powerlocale_ of $X$. The frame of opens of
the lower powerlocale is the free frame on the underlying suplattice of
$\mathcal{O}X$ and its points correspond to (overt, weakly) closed sublocales
of $X$. We can identify points of $Y$ with the sublocales of $X$ that appear
as the (weak) closures of their fibres under $q\colon X\to Y$. Intuitively, we
can view it as a space of equivalence classes. See [12, 11] for more details
on the lower powerlocale and its relation to semi-open maps.

###  3.2. Presenting proper quotients

We can proceed similarly for semi-proper quotients. Recall that a semi-proper
quotient $q\colon X\twoheadrightarrow Y$ can be specified by an interior
operator and preframe endomorphism $p\colon\mathcal{O}X\to\mathcal{O}X$. The
map $q_{*}$ is the preframe quotient given by setting $a\lesssim p(a)$.

Suppose $\mathcal{O}X$ has a $\mathbf{PreFrm}$-type presentation $\langle
G\text{ $\vee$-semilattice}\mid R\rangle_{\mathbf{Frm}}$. Applying the
preframe coverage theorem (1.4) and taking the quotient we have
$\mathcal{O}Y\cong\langle G\text{ poset}\mid R,\ g\leq p(g),\,g\in
G\rangle_{\mathbf{PreFrm}}$. Here we expand each $p(g)$ as a directed join of
finite meets of generators.

Now we need to turn this into a frame presentation. Similarly to before, if a
preframe $L$ happens to be a frame, then $L\cong\langle\\{\square a\mid a\in
L\\}\text{ preframe}\mid\square 0=0,\ \square(a\vee b)=\square a\vee\square
b,\,a,b\in L\rangle_{\mathbf{Frm}}$. We may also restrict $a,b$ to lie in a
preframe generating set. In our case, the generators $a,b$ in $\mathcal{O}X$
map to $q_{*}(a),q_{*}(b)$ in the preframe quotient and so their join in
$\mathcal{O}Y$ corresponds to $p(a)\vee p(b)$ in $\mathcal{O}X$. Combining
this with the preframe presentation above and eliminating redundant relations
as before we arrive as the following result.

######  Proposition 3.4.

Suppose $\mathcal{O}X=\langle G\text{ $\vee$-semilattice}\mid
R\rangle_{\mathbf{Frm}}$ is a $\mathbf{PreFrm}$-type presentation and let
$q\colon X\twoheadrightarrow Y$ be a semi-proper quotient. Then

$\displaystyle\mathcal{O}Y\cong\langle\square g,\,g\in G\mid{}$ $\displaystyle
R,\ \square 0=0$ $\displaystyle\square s\vee\square
t=\square(q^{*}q_{*}(s)\vee q^{*}q_{*}(t)),\,s,t\in G\rangle_{\mathbf{Frm}},$

where $\square(q^{*}q_{*}(s)\vee
q^{*}q_{*}(t))=\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha,\beta}}\bigwedge_{i_{\alpha},j_{\beta}}\square(s_{\alpha}^{i_{\alpha}}\vee
t_{\beta}^{j_{\beta}})$ for specified representations
$q^{*}q_{!}(s)=\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha}}\bigwedge_{i_{\alpha}}s_{\alpha}^{i_{\alpha}}$
and
$q^{*}q_{!}(t)=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}\bigwedge_{j_{\beta}}t_{\beta}^{j_{\beta}}$
in terms of generators.

If $q$ is an _proper_ quotient we can again use the Frobenius condition to
give the following simplification.

######  Corollary 3.5.

Suppose $\mathcal{O}X=\langle G\text{ $\vee$-semilattice}\mid
R\rangle_{\mathbf{Frm}}$ is a $\mathbf{PreFrm}$-type presentation and let
$q\colon X\twoheadrightarrow Y$ be a proper quotient. Then

$\displaystyle\mathcal{O}Y\cong\langle\square g,\,g\in G\mid{}$ $\displaystyle
R,\ \square 0=0$ $\displaystyle\square s\vee\square t=\square(s\vee
q^{*}q_{*}(t)),\,s,t\in G\rangle_{\mathbf{Frm}},$

where $\square(s\vee
q^{*}q_{*}(t))=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}\bigwedge_{j_{\beta}}\square(s\vee
t_{\beta}^{j_{\beta}})$ for specified representation
$q^{*}q_{!}(t)=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}\bigwedge_{j_{\beta}}t_{\beta}^{j_{\beta}}$.

######  Remark 3.6.

This time our presentation can be thought of as expressing $Y$ as a sublocale
of the _upper powerlocale_ of $X$. The frame of opens of the upper powerlocale
is the free frame on the underlying preframe of $\mathcal{O}X$ and its points
correspond to compact fitted sublocales of $X$. As before, we can think of $Y$
as a space of equivalence classes: the points of $Y$ correspond to the fitting
of the fibres of $q\colon X\to Y$. Again see [12, 11] for more details on
these concepts. Propositions 3.1 and 3.4 can also be compared to the
construction given in the proof of (ii) $\Rightarrow$ (iii) of [9, Theorem 2].

###  3.3. Presenting triquotient locales

The general semi-triquotient case is again similar. Let $q\colon
X\twoheadrightarrow Y$ be a locale map such that $q^{*}$ has a left inverse
dcpo morphism $q_{\\#}\colon\mathcal{O}X\to\mathcal{O}Y$. Such a semi-
triquotient can represented by a dcpo endomorphism $e$ satisfying the
necessary conditions and the retraction onto the fixed points induced by $e$
corresponds the dcpo quotient map $q_{\\#}$, which is specified by setting
$a\sim e(a)$.

Now suppose $\mathcal{O}X$ has a $\mathbf{DCPO}$-type presentation $\langle
G\text{ dist.\ lattice}\mid R\rangle_{\mathbf{Frm}}$. Using the dcpo coverage
theorem (1.6) and taking the quotient we have $\mathcal{O}Y\cong\langle
G\text{ poset}\mid R,\ g=e(g),\,g\in G\rangle_{\mathbf{DCPO}}$, where each
$e(g)$ is expressed explicitly as a directed join of generators. Then as
before we can turn this into a frame presentation to obtain the following.

######  Proposition 3.7.

Suppose $\mathcal{O}X=\langle G\text{ dist.\ lattice}\mid
R\rangle_{\mathbf{Frm}}$ is a $\mathbf{DCPO}$-type presentation and let
$q\colon X\twoheadrightarrow Y$ be a semi-triquotient with triquotiency
assignment $q_{\\#}\colon\mathcal{O}X\to\mathcal{O}Y$. Then

$\displaystyle\mathcal{O}Y\cong\langle{\boxtimes}g,\,g\in G\mid{}$
$\displaystyle R,\ {\boxtimes}1=1,\ {\boxtimes}0=0$
$\displaystyle{\boxtimes}s\wedge{\boxtimes}t={\boxtimes}(q^{*}q_{\\#}(s)\wedge
q^{*}q_{\\#}(t)),$
$\displaystyle{\boxtimes}s\vee{\boxtimes}t={\boxtimes}(q^{*}q_{\\#}(s)\vee
q^{*}q_{\\#}(t)),\ s,t\in G\rangle_{\mathbf{Frm}},$

where ${\boxtimes}(q^{*}q_{\\#}(s)\wedge
q^{*}q_{\\#}(t))=\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha,\beta}}{\boxtimes}(s_{\alpha}\wedge
t_{\beta})$ and ${\boxtimes}(q^{*}q_{\\#}(s)\vee
q^{*}q_{\\#}(t))=\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha,\beta}}{\boxtimes}(s_{\alpha}\vee
t_{\beta})$ for specified representations
$q^{*}q_{\\#}(s)=\operatorname*{\bigvee{}^{\\!\uparrow}_{\alpha}}s_{\alpha}$
and $q^{*}q_{\\#}(t)=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}t_{\beta}$
in terms of generators.

Finally, if $q$ is an _triquotient_ we can again simplify things a little.

######  Corollary 3.8.

Suppose $\mathcal{O}X=\langle G\text{ dist.\ lattice}\mid
R\rangle_{\mathbf{Frm}}$ is a $\mathbf{DCPO}$-type presentation and let
$q\colon X\twoheadrightarrow Y$ be a triquotient with triquotiency assignment
$q_{\\#}\colon\mathcal{O}X\to\mathcal{O}Y$. Then

$\displaystyle\mathcal{O}Y\cong\langle{\boxtimes}g,\,g\in G\mid{}$
$\displaystyle R,\ {\boxtimes}1=1,\ {\boxtimes}0=0$
$\displaystyle{\boxtimes}s\wedge{\boxtimes}t={\boxtimes}(s\wedge
q^{*}q_{\\#}(t)),$
$\displaystyle{\boxtimes}s\vee{\boxtimes}t={\boxtimes}(s\vee
q^{*}q_{\\#}(t)),\ s,t\in G\rangle_{\mathbf{Frm}},$

where ${\boxtimes}(s\wedge
q^{*}q_{\\#}(t))=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}{\boxtimes}(s\wedge
t_{\beta})$ and ${\boxtimes}(s\vee
q^{*}q_{\\#}(t))=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}{\boxtimes}(s\vee
t_{\beta})$ for specified representation
$q^{*}q_{\\#}(t)=\operatorname*{\bigvee{}^{\\!\uparrow}_{\beta}}t_{\beta}$.

######  Remark 3.9.

While these (semi-)triquotient results technically subsume the previous ones,
they are all useful, since the presentations obtained from the more specific
results will be simpler those given by the most general one.

######  Remark 3.10.

This time the intuition is less clear, but the presentation is related to
viewing $Y$ is a sublocale of the _double powerlocale_ of $X$ (see [13]). The
double powerlocale arises from the adjunction between frames and dcpos is
equal to the composition of the upper and lower powerlocales (in either
order). Its points can be viewed as certain overt collections of compact
sublocales.

It is natural to ask if yet more general quotients might arise by using
further composites of upper and lower powerlocales, but essentially because
the double powerlocale is a retract of the ‘quadruple powerlocale’, no new
quotients are obtained after the second level.

##  4\. Examples and applications

The main utility of these results is in deriving concrete presentations, but
they do have at least one theoretical consequence: namely, that the size of
the presentation of the quotient is not so different from that of the
presentation of the parent locale. In particular, we can immediately deduce
the following.

######  Proposition 4.1.

A semi-triquotient of a countably presented locale is countably presented.

Classically, countably presented locales coincide with _quasi-Polish_ spaces
(see [2, 4]). Thus, as a corollary we obtain the following result, which known
for open quotients, but which I have not seen stated before at this level of
generality.

######  Corollary 4.2.

Let $X$ be a quasi-Polish space, let $Y$ be sober and let $X\twoheadrightarrow
Y$ be a triquotient map. Then $Y$ is quasi-Polish.

We now conclude with some illustrative examples. First we obtain a
presentation of the circle $\mathbb{T}$ from the presentation of $\mathbb{R}$
using the open quotient $\mathbb{R}\twoheadrightarrow\mathbb{T}$.

######  Example 4.3.

The usual presentation for the frame of reals $\mathcal{O}\mathbb{R}$ has a
generator $(\\!(q,\infty)\\!)$ and a generator $(\\!(-\infty,q)\\!)$ for each
$q\in\mathbb{Q}$. They satisfy the following relations.

  * •

$(\\!(p,\infty)\\!)\wedge(\\!(-\infty,q)\\!)=0$ for $p\geq q$,

  * •

$(\\!(p,\infty)\\!)\vee(\\!(-\infty,q)\\!)=1$ for $p<q$,

  * •

$(\\!(q,\infty)\\!)=\bigvee_{p>q}(\\!(p,\infty)\\!)$ and
$(\\!(-\infty,q)\\!)=\bigvee_{p<q}(\\!(-\infty,p)\\!)$ for all
$q\in\mathbb{Q}$,

  * •

$\bigvee_{q\in\mathbb{Q}}(\\!(q,\infty)\\!)=1$ and
$\bigvee_{q\in\mathbb{Q}}(\\!(-\infty,q)\\!)=1$.

To apply our result the presentation must be modified to be of the appropriate
form. In particular, the generators should be closed under finite meets.
Setting $(\\!(p,q)\\!)=(\\!(p,\infty)\\!)\wedge(\\!(-\infty,q)\\!)$ and
$(\\!(-\infty,\infty)\\!)=1$ we have defined generators $(\\!(p,q)\\!)$ for
each $p\in\mathbb{Q}\sqcup\\{-\infty\\}$ and
$q\in\mathbb{Q}\sqcup\\{\infty\\}$. These form a $\wedge$-semilattice with
$(\\!(p,q)\\!)\wedge(\\!(p^{\prime},q^{\prime})\\!)=(\\!(p\vee
p^{\prime},q\wedge q^{\prime})\\!)$. The remaining axioms become:

  * •

$(\\!(p,q)\\!)=0$ for $p\geq q$,

  * •

$(\\!(p,q)\\!)\vee(\\!(p^{\prime},q^{\prime})\\!)=(\\!(p,q^{\prime})\\!)$ for
$p\leq p^{\prime}<q\leq q^{\prime}$,

  * •

$(\\!(p,q)\\!)=\bigvee_{p<p^{\prime}<q^{\prime}<q}(\\!(p^{\prime},q^{\prime})\\!)$
for all $p\in\mathbb{Q}\sqcup\\{-\infty\\}$ and
$q\in\mathbb{Q}\sqcup\\{\infty\\}$.

In fact, the first bullet point here is redundant, since it follows from the
third. We note that these relations (essentially) satisfy the necessary meet-
stability conditions for this to be a $\mathbf{Sup}$-type presentation. Let us
show this for a representative case.

Since $(\\!(a,b)\\!)=(\\!(a,\infty)\\!)\wedge(\\!(-\infty,b)\\!)$, it suffices
to only consider meets with $(\\!(a,\infty)\\!)$ and $(\\!(-\infty,b)\\!)$.
Consider the relation
$(\\!(p,q)\\!)\vee(\\!(p^{\prime},q^{\prime})\\!)=(\\!(p,q^{\prime})\\!)$ for
$p\leq p^{\prime}<q\leq q^{\prime}$. Meeting with $(\\!(a,\infty)\\!)$ we
obtain the equality $(\\!(p\vee a,q)\\!)\vee(\\!(p^{\prime}\vee
a,q^{\prime})\\!)=(\\!(p\vee a,q^{\prime})\\!)$. Meet stability demands that
this is also a relation in the presentation. If $a\leq p^{\prime}$ then $p\vee
a\leq p^{\prime}\vee a<q\leq q$ and so this is indeed an assumed relation of
the same form. If not, then $p^{\prime}<a$ and it becomes
$(\\!(a,q)\\!)\vee(\\!(a,q^{\prime})\\!)=(\\!(a,q^{\prime})\\!)$. Technically,
this is not one of the original relations, but it is trivial in the sense that
it always holds.

Indeed, even more generally, our results will still hold as long as the
desired relations lie in the suplattice congruence generated from the core
relations and the order on the generators, since we can add these relations in
to achieve meet stability, but then omit them from the final presentation
(since they follow from the others by assumption).

Meeting with $(\\!(-\infty,b)\\!)$ works similarly and meet stability for the
final relations can also be shown to hold, at least in this weaker sense.

Now consider the coequaliser

$\mathbb{R}$$\mathbb{R}$$\mathbb{T}$.$\mathrm{id}$$+1$$q$

This is an open coequaliser, since the both of the parallel arrows are
isomorphisms. So by Propositions 2.2 and 2.3, the corresponding closure
operator $q^{*}q_{!}$ is given by
$\bigvee_{n\in\mathbb{N}}(\mathrm{id}_{!}\circ(+1)^{*})^{n}\vee\bigvee_{n\in\mathbb{N}}((+1)_{!}\circ\mathrm{id}^{*})^{n}$,
which equals $\bigvee_{n\in\mathbb{Z}}(+n)^{*}$, since the left adjoint of
$(+1)^{*}$ is simply its inverse. Note that
$(+1)^{*}(\\!(p,q)\\!)=(\\!(p-1,q-1)\\!)$ and so in terms of generators, we
have $q^{*}q_{!}(\\!(p,q)\\!)=\bigvee_{n\in\mathbb{Z}}(\\!(p+n,q+n)\\!)$.

We can now use Corollary 3.2 to obtain a presentation for
$\mathcal{O}\mathbb{T}$ with generators $(\\!(p,q)\\!)$ for
$p\in\mathbb{Q}\sqcup\\{-\infty\\}$ and $q\in\mathbb{Q}\sqcup\\{\infty\\}$ and
the following relations:

  * •

$(\\!(-\infty,\infty)\\!)=1$,

  * •

$(\\!(p,q)\\!)\wedge(\\!(p^{\prime},q^{\prime})\\!)=\bigvee_{n\in\mathbb{Z}}(\\!(p\vee(p^{\prime}+n),q\wedge(q^{\prime}+n))\\!)$,

  * •

$(\\!(p,q)\\!)\vee(\\!(p^{\prime},q^{\prime})\\!)=(\\!(p,q^{\prime})\\!)$ for
$p\leq p^{\prime}<q\leq q^{\prime}$,

  * •

$(\\!(p,q)\\!)=\bigvee_{p<p^{\prime}<q^{\prime}<q}(\\!(p^{\prime},q^{\prime})\\!)$.

This presentation for the circle is essentially the same as the one in [3,
Section 5] which was obtained by ad hoc methods. In contrast, we observe that
our derivation was very natural and mechanistic. ∎

For our next example, we will deduce a different presentation for $\mathbb{T}$
from the proper quotient $[0,1]\twoheadrightarrow\mathbb{T}$.

######  Example 4.4.

A standard presentation for the frame $\mathcal{O}[0,1]$ has generators
$(\\!(q,1\rrbracket$ and $\llbracket 0,q)\\!)$ for each
$q\in\mathbb{Q}\cap[0,1]$ which satisfy the relations:

  * •

$(\\!(p,1\rrbracket\wedge\llbracket 0,q)\\!)=0$ for $p\geq q$,

  * •

$(\\!(p,1\rrbracket\vee\llbracket 0,q)\\!)=1$ for $p<q$,

  * •

$(\\!(q,1\rrbracket=\bigvee_{p>q}(\\!(p,1\rrbracket$ and $\llbracket
0,q)\\!)=\bigvee_{p<q}\llbracket 0,p)\\!)$ for all $q\in\mathbb{Q}\cap[0,1]$.

To use our result for proper quotients this presentation must also be
modified. This time we want the generators to be closed under finite joins. We
set ${\rrparenthesis p,q\llparenthesis}=\llbracket
0,p)\\!)\vee(\\!(q,1\rrbracket$. Intuitively, these are the complements of
closed intervals.

Indeed, recall that for $\mathbf{PreFrm}$-type presentations the elements of
the frame are best thought of as _closed_ sublocales under the reverse order,
so we can imagine the generator ${\rrparenthesis p,q\llparenthesis}$ as
corresponding to the closed interval $[p,q]$. From this perspective it is
intuitive that under intersections of the corresponding closed intervals these
form a very similar semilattice to the formal open intervals considered above.
Formally, we can check that these indeed form a $\vee$-semilattice with
${\rrparenthesis p,q\llparenthesis}\vee{\rrparenthesis
p^{\prime},q^{\prime}\llparenthesis}={\rrparenthesis p\vee p^{\prime},q\wedge
q^{\prime}\llparenthesis}$ and ${\rrparenthesis 0,1\llparenthesis}=0$.

In terms of these new generators the remaining axioms become:

  * •

${\rrparenthesis p,q\llparenthesis}\wedge{\rrparenthesis
p^{\prime},q^{\prime}\llparenthesis}={\rrparenthesis
p,q^{\prime}\llparenthesis}$ for $p\leq p^{\prime}\leq q\leq q^{\prime}$,

  * •

${\rrparenthesis p,q\llparenthesis}=1$ for $p>q$,

  * •

${\rrparenthesis
p,q\llparenthesis}=\operatorname*{\bigvee{}^{\\!\uparrow}_{q^{\prime}>q}}{\rrparenthesis
p,q^{\prime}\llparenthesis}$ for $p,q<1$ and ${\rrparenthesis
p,q\llparenthesis}=\operatorname*{\bigvee{}^{\\!\uparrow}_{p^{\prime}<p}}{\rrparenthesis
p^{\prime},q\llparenthesis}$ for $0<p,q$.

Again note that these essentially satisfy the join-stability conditions for
these to form a $\mathbf{PreFrm}$-style presentation.

We can now consider the locale coequaliser

$1$$[0,1]$$\mathbb{T}$.$0$$1$$q$

The parallel arrows are closed inclusions and hence proper — the right
adjoints are given by taking joins with ${\rrparenthesis 0,0\llparenthesis}$
and ${\rrparenthesis 1,1\llparenthesis}$ respectively. The pullback of these
parallel arrows is the empty locale and so the unique map $t\colon 0\to 1$
trivially satisfies the assumptions of Propositions 2.6 and 2.8 and hence $q$
is a proper quotient and the corresponding interior operator $q^{*}q_{*}$ is
$(1)_{*}(0)^{*}\wedge(0)_{*}(1)^{*}\wedge\mathrm{id}$.

In terms of generators we have that $(0)^{*}({\rrparenthesis
p,q\llparenthesis})=1\iff p>0$ and $(1)^{*}({\rrparenthesis
p,q\llparenthesis})=1\iff{q<1}$. Thus, we find

$q^{*}q_{*}\colon{\rrparenthesis
p,q\llparenthesis}\mapsto\begin{cases}{\rrparenthesis
p,q\llparenthesis}&\text{ if $p>0$ and $q<1$}\\\ {\rrparenthesis
p,q\llparenthesis}\wedge{\rrparenthesis 1,1\llparenthesis}&\text{ if $p=0$ and
$q<1$}\\\ {\rrparenthesis p,q\llparenthesis}\wedge{\rrparenthesis
0,0\llparenthesis}&\text{ if $p>0$ and $q=1$}\\\ 0&\text{ if $p=0$ and
$q=1$}\\\ \end{cases},$

which intuitively adds $\\{0\\}$ to any closed interval containing $1$ and
$\\{1\\}$ to any closed interval containing $0$.

We are now in a position to use Corollary 3.5 to immediately obtain a
presentation for $\mathcal{O}\mathbb{T}$ with generators ${\rrparenthesis
p,q\llparenthesis}$ for $p,q\in\mathbb{Q}\cap[0,1]$ and the relations:

  1. i)

${\rrparenthesis 0,1\llparenthesis}=0$,

  2. ii)

${\rrparenthesis p,q\llparenthesis}\vee{\rrparenthesis
p^{\prime},q^{\prime}\llparenthesis}={\rrparenthesis p\vee p^{\prime},q\wedge
q^{\prime}\llparenthesis}$ for $p^{\prime}>0$ and $q^{\prime}<1$,

  3. iii)

${\rrparenthesis p,q\llparenthesis}\vee{\rrparenthesis
0,q^{\prime}\llparenthesis}={\rrparenthesis p,q\wedge
q^{\prime}\llparenthesis}\wedge{\rrparenthesis 1,q\llparenthesis}$,

  4. iv)

${\rrparenthesis p,q\llparenthesis}\vee{\rrparenthesis
p^{\prime},1\llparenthesis}={\rrparenthesis p\vee
p^{\prime},q\llparenthesis}\wedge{\rrparenthesis p,0\llparenthesis}$,

  5. v)

${\rrparenthesis p,q\llparenthesis}\wedge{\rrparenthesis
p^{\prime},q^{\prime}\llparenthesis}={\rrparenthesis
p,q^{\prime}\llparenthesis}$ for $p\leq p^{\prime}\leq q\leq q^{\prime}$,

  6. vi)

${\rrparenthesis p,q\llparenthesis}=1$ for $p>q$,

  7. vii)

${\rrparenthesis
p,q\llparenthesis}=\operatorname*{\bigvee{}^{\\!\uparrow}_{q^{\prime}>q}}{\rrparenthesis
p,q^{\prime}\llparenthesis}$ for $p,q<1$ and ${\rrparenthesis
p,q\llparenthesis}=\operatorname*{\bigvee{}^{\\!\uparrow}_{p^{\prime}<p}}{\rrparenthesis
p^{\prime},q\llparenthesis}$ for $0<p,q$.

This can be further simplified by noting that ${\rrparenthesis
1,q\llparenthesis}=1$ unless $q=1$ by relation (vi) and similarly for
${\rrparenthesis p,0\llparenthesis}$. Thus, we can extend relation (ii) to
hold for all $p,p^{\prime},q,q^{\prime}$ such that
$(p^{\prime},q),(p,q^{\prime})\neq(0,1)$. Then the remaining cases of (iii)
and (iv) can be reduced to a single rule: ${\rrparenthesis
0,q\llparenthesis}\vee{\rrparenthesis
p^{\prime},1\llparenthesis}={\rrparenthesis
p^{\prime},q\llparenthesis}\wedge{\rrparenthesis
0,0\llparenthesis}\wedge{\rrparenthesis 1,1\llparenthesis}$. ∎

## References

  * [1] S. Abramsky and S. Vickers.  Quantales, observational logic and process semantics.  Math. Structures Comput. Sci., 3(2):161–227, 1993.
  * [2] M. de Brecht.  Quasi-Polish spaces.  Ann. Pure Appl. Logic, 164(3):356–381, 2013.
  * [3] J. Gutiérrez García, I. Mozo Carollo, and J. Picado.  Presenting the frame of the unit circle.  J. Pure Appl. Algebra, 220(3):976–1001, 2016.
  * [4] R. Heckmann.  Spatiality of countably presentable locales (proved with the Baire category theorem).  Math. Structures Comput. Sci., 25(7):1607–1625, 2015.
  * [5] P. Johnstone and S. Vickers.  Preframe presentations present.  In A. Carboni, M. C. Pedicchio, and G. Rosolini, editors, Category theory: Proceedings of the International Conference held in Como, volume 1488 of Lecture Notes in Mathematics, pages 193–212, Berlin, 1991\. Springer.
  * [6] A. Kock.  A Godement theorem for locales.  Math. Proc. Cambridge Philos. Soc., 105(3):463–471, 1989.
  * [7] M. Korostenski and C. C. A. Labuschagne.  Lax proper maps of locales.  J. Pure Appl. Algebra, 208(2):655–664, 2007.
  * [8] T. Plewe.  Localic triquotient maps are effective descent maps.  Math. Proc. Cambridge Philos. Soc., 122(1):17–43, 1997.
  * [9] C. F. Townsend.  A categorical account of the Hofmann–Mislove theorem.  Math. Proc. Cambridge Philos. Soc., 139(3):441–456, 2005.
  * [10] J. J. C. Vermeulen.  Proper maps of locales.  J. Pure Appl. Algebra, 92(1):79–107, 1994.
  * [11] S. Vickers.  Locales are not pointless.  In C. Hankin, I. Mackie, and R. Nagarajan, editors, Theory and Formal Methods of Computing 94: Proceedings of the Second Imperial College Workshop, pages 199–216, London, 1995. Imperial College Press.
  * [12] S. Vickers.  Constructive points of powerlocales.  Math. Proc. Cambridge Philos. Soc., 122(2):207–222, 1997.
  * [13] S. Vickers.  The double powerlocale and exponentiation: a case study in geometric logic.  Theory Appl. Categ., 12(13):372–422, 2004.
  * [14] S. J. Vickers and C. F. Townsend.  A universal characterization of the double powerlocale.  Theoret. Comput. Sci., 316(1-3):297–321, 2004.