Overlap Algebras: a Constructive Look at Complete Boolean Algebras

TL;DR

This paper introduces overlap algebras as a constructive alternative to complete Boolean algebras, capturing natural structures like powersets and relating to locales, with foundational categorical properties explored.

Contribution

It develops the theory of overlap algebras, extending the category of sets and relations, and connects them to locale theory in a constructive setting.

Findings

Overlap algebras generalize complete Boolean algebras constructively.

The category of overlap algebras has well-understood mono-epi-isomorphisms and (co)limits.

Constructive connections between overlap algebras and locales are established.

Abstract

The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales.

Equations

$$a\ne 0$$

$$\mathrm{Pos}(x)\wedge (x\le y)\Rightarrow \mathrm{Pos}(y)$$

$$\mathrm{Pos}(\bigvee X)\Rightarrow (\exists x\in X)\mathrm{Pos}(x)$$

$$(\mathrm{Pos}(x)\Rightarrow (x\le y))⟹x\le y$$

$$y\le \bigvee \{x\in L|\mathrm{Pos}(x)\wedge (x\le y)\}.$$

$$\mathrm{Pos}(a)\land(\forall x\in L)\big{(}\mathrm{Pos}(x)\wedge(x\leq a)\Longrightarrow(x=a)\big{)}\ .$$

$$(\forall x\in L)\big{(}\mathrm{Pos}(a\wedge x)\Longleftrightarrow(a\leq x)\big{)}\ .$$

$$(\forall z\in L)(\mathrm{Pos}(z\wedge x)\Rightarrow \mathrm{Pos}(z\wedge y))⟹x\le y$$

$$(\forall x\in L)\big{(}(a>\mkern-13.5mu<x)\Longleftrightarrow(a\leq x)\big{)}\ .$$

$$R^{-1}(Y^{\prime })><X^{\prime }\text{ in }\mathrm{Pow}(X)⟺Y^{\prime }><(R^{†}{)}^{-1}(X^{\prime })\text{ in }\mathrm{Pow}(Y).$$

$$f(x)><y⟺x><g(y)$$

$$(g\circ f{)}^{†}=f^{†}\circ g^{†}$$

$$L_j\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

Full text

In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales.

Introduction

A typical phenomenon in constructive mathematics is the split of classical notions: several definitions which are equivalent over classical logic can become deeply different over intuitionistic logic. In this paper we study an alternative way to define complete Boolean algebras, as proposed by Giovanni Sambin [10, 2] who named them overlap algebras. There are some facts which make overlap algebras interesting, we believe, from the constructive point of view; for instance, the collection of all subsets of a set is an overlap algebra, actually an atomistic one, although it cannot ever be Boolean (apart from the trivial case of the power of the empty set).

Roughly speaking, an overlap algebra is a complete lattice (actually a complete Heyting algebra) equipped with a new primitive relation, the overlap relation $>\mkern-13.5mu<$. The intended meaning of $x>\mkern-13.5mu<y$ is that the infimum $x\wedge y$ is “inhabited”. The distinction between inhabited and non-empty is enlightening. Indeed, constructively $\exists x(x\in X)$ is a stronger statement than $\neg\forall x\neg(x\in X)$. In an arbitrary complete Heyting algebra we can use $x\neq 0$ as the algebraic counterpart of the set-theoretic $X\neq\emptyset$, but there is no way to express the positive statement of being inhabited. Overlap algebras give an elegant answer to this question.

Overlap algebras and complete Boolean algebras have just one element in common, the trivial one-element algebra, unless classical logic is assumed, in which case the two notions coincide.

In this paper we investigate two natural notions of morphism between overlap algebras which are both inspired by the powerset construction. First we study the category OA as originally introduced by Sambin; OA is a dagger category which contains the category Rel of sets and relations as a full subcategory; classically, OA is the category of complete Boolean algebras and join preserving maps. In particular, we characterize monomorphisms, epimorphisms, and isomorphisms in OA, and we establish some basic facts about limits and colimits. Then we specialize to the subcategory OFrm whose arrows preserve also finite meets. This is a subcategory of Frm, the category of frames; morphisms in OFrm correspond to open maps in the sense of locale theory. Classically, OFrm is the usual category of complete Boolean algebras; we are therefore able to obtain new constructive versions of some standard results about Boolean locales.

If not otherwise stated, we assume to work over intutionistic logic and without choice. In other words, we understand “constructive” as “topos-valid”. In particular, we shall usually think of powersets as perfectly legitimate sets even if we shall make some remark on predicativity in the last section: it is a fact that most of the paper could be adapted to a predicative framework (such as that presented in [8]) by a systematic use of “bases”.

Part of the material in the present paper appeared in the second author’s master thesis [3].

1. Atomic Heyting algebras

Given a set $X$, its subsets form a complete Heyting algebra $\mathrm{Pow}(X)$ with respect to the usual set-theoretic operations. Here we write $-Y$ for the pseudo-complement of the subset $Y\subseteq X$. We write $\Omega$ for $\mathrm{Pow}(1)$, where $1=\{0\}$, which we interpret as the type of truth values. It is well-known that the following statements are equivalent:

• •

the Law of Excluded Middle (LEM);

• •

$(\forall p\in\Omega)(p\cup-p=1)$, that is, $\Omega\cong 2=\{0,1\}$;

• •

$\mathrm{Pow}(X)$ is a complete Boolean algebra for every $X$.

Classically, powersets are precisely the atomic Boolean algebras (this means that every element is the join of the atoms below it, where an atom is a minimal non-zero element). In other words, a Boolean algebra is atomic if and only if it is isomorphic to the powerset of the set of its atoms. The problem of finding a constructive characterization of powersets is related to the problem of finding a suitable algebraization of the notion of a singleton. Apparently, none of the first-order (in the sense of the language of lattices) attempts to define when $a\in L$ is an atom is satisfactory from an intuitionistic point of view; consider, for instance, the following.

[TABLE]

Indeed, when applied to the case $L=\mathrm{Pow}(X)$, singletons cannot be proven to be atoms in the sense of (1) or (2), and it is impossible to prove that every subset satisfying (3) or (4) is a singleton, although a singleton satisfies (3) and (4). All this comes up clear already when inspecting the case $L=\Omega$: its only singleton $1=\{0\}$ satisfies (1) or (2) if and only if LEM holds; and LEM is equivalent to assuming that $1$ is the only $a\in\Omega$ satisfying (3) or (4). A possible well-known solution is to adopt a second-order definition, as follows.

Definition \thethm.

Given a poset $(L,\leq)$, we say that $a\in L$ is an atom if the poset ${\downarrow a}$ = $\{x\in L\ |\ x\leq a\}$ is order-isomoprhic to $\Omega$. And $(L,\leq)$ is atomic if the join of all atoms below a given $x$ exists and equals $x$, for every $x\in L$.

If $L=\mathrm{Pow}(X)$, then ${\downarrow\{x\}}$ = $\mathrm{Pow}(\{x\})$ is isomorphic to $\Omega$ = $\mathrm{Pow}(\{0\})$, for all $x\in X$. So every singleton is an atom and hence every element is a join of atoms. Actually, we can show that the atoms in $\mathrm{Pow}(X)$ are precisely the singletons. Let $Y$ be an atom, that is, ${\downarrow Y}=\mathrm{Pow}(Y)\cong\Omega$; and let $\varphi:\mathrm{Pow}(Y)\to\Omega$ be an order isomorphism (which then preserves joins and meets). Then $1$ = $\varphi(Y)$ = $\varphi(\bigcup_{x\in Y}\{x\})$ = $\bigvee_{x\in Y}\varphi(\{x\})$. So $Y$ is inhabited, actually there is some $x\in Y$ with $\varphi(\{x\})$ = 1, and hence $Y$ = $\varphi^{-1}(1)$ = $\{x\}$.

Proposition \thethm.

A frame $L$ is atomic if and only if it is order isomorphic to $\mathrm{Pow}(X)$, where $X$ is the set of atoms of $L$.

Proof.

One direction follows from the discussion above. As for the other, let us define $f:L\to\mathrm{Pow}(X)$ to be the function which maps a given $x$ to the set of atoms below it, and let $g:\mathrm{Pow}(X)\to L$ be the function which maps a set of atoms to its join. The two mapping are clearly monotone. Moreover, $g(f(x))=x$ because $L$ is atomic. It remains to show that $f(g(Y))=Y$ for every $Y\subseteq X$. The inclusion $Y\subseteq f(g(Y))$ is clear. As for the other, we must show that $x\leq\bigvee Y$ implies $x\in Y$ for every $x\in X$. Now $x\leq\bigvee Y$ can be written as $x$ = $x\wedge\bigvee Y$ = $\bigvee\{x\wedge y\ |\ y\in Y\}$. Since $x$ is an atom (that is, ${\downarrow x}$ behaves like $\Omega$), $x\wedge y$ must be $x$ for some $y$. So $x\leq y$. Since $y$ is an atom too, this happens precisely when $x=y$ (there is only one atom in ${\downarrow y}$ $\cong$ $\Omega$ = $\mathrm{Pow}(1)$). ∎

1.1. The positivity predicate on a frame

For $X$ a set, the statement “$X$ is inhabited” is stronger than “$X\neq\emptyset$”, constructively; and the two statements are equivalent for all sets $X$ if and only if LEM holds. There exists a quite standard way to “algebraize” the concept of an inhabited set.

Definition \thethm.

Let $L$ be a complete lattice. A unary predicate $\mathrm{Pos}$ on $L$ is a positivity predicate if the following conditions hold identically.

[TABLE]

It is easy to check that (7) can be replaced by

[TABLE]

By extending the terminology which is used for frames/locales, we call a complete lattice overt if it has a positivity predicate.

It is well-known that if $L$ is overt, then $\mathrm{Pos}$ is equivalent to the second-order predicate $POS$, where $POS(x)$ is $(\forall X\subseteq L)(x\leq\bigvee X\Longrightarrow X\textrm{ is inhabited})$. This has a couple of (almost) immediate consequences. First, the positivity predicate, when it exists, is unique and it is uniquely determined by the ordering. Second, $L$ is overt if and only if $POS$ is a positivity predicate. Classically, every complete lattice is overt and $\mathrm{Pos}(x)$ is just $x\neq 0$. Constructively, $\mathrm{Pos}(x)$ always implies $x\neq 0$, but not the other way around, in general; and it cannot be proven that every complete lattice is overt.

The notion of overteness for a frame can be characterized in a more categorical fashion. Given a frame $L$, there is a unique frame homomorphism $!:\Omega\to L$ (that is, $\Omega$ is the initial frame, that is, the terminal locale). Then $L$ is overt precisely when $!$ has a left adjoint $\exists_{!}$ (which happens precisely when $!$ preserves arbitrary meets), in which case $\exists_{!}=\mathrm{Pos}$.

1.2. Atoms of an overt frame

The positivity predicate $\mathrm{Pos}$ can be used to characterize the atoms. In the case of a powerset, a singleton is precisely a minimal inhabited subset. So the following variation of (1) is the natural candidate for a first-order definition of an atom:

[TABLE]

Proposition \thethm.

Let $L$ be an overt complete lattice; $a\in L$ is an atom if and only if $a$ satisfies (9).

Proof.

If $L$ is overt and $x\in L$, then also ${\downarrow x}$ is overt with respect to the restriction of $\mathrm{Pos}$.

Let $a$ be an atom, that is, ${\downarrow a}$ $\cong$ $\Omega$. So $\mathrm{Pos}(x)$ becomes “$x$ is inhabited” under such an isomorphism, and hence (9) is true on ${\downarrow a}$ (because it is true on $\Omega$; recall that the positivity predicate is uniquely determined by the ordering and so has to be preserved by order-isomorphism).

Conversely, if $a$ satisfies (9), $\mathrm{Pos}:{\downarrow a}\to\Omega$ is an order-isomorphism whose inverse is $p\mapsto\bigvee\{x\leq a\ |\ p\}$. Indeed, the two mappings are monotone, and $\mathrm{Pos}(\bigvee\{x\leq a\ |\ p\})=p$; moreover, for $b\leq a$, it is $\bigvee\{x\leq a\ |\ \mathrm{Pos}(b)\}\leq b$ because $\mathrm{Pos}(b)$ is just $b=a$ by (9), and $b\leq\bigvee\{x\leq a\ |\ \mathrm{Pos}(b)\}$ because $\mathrm{Pos}$ is a positivity predicate on ${\downarrow a}$, in particular it satisfies (7). ∎

As noticed by Giovanni Sambin, (9) is equivalent to the following elegant condition:

[TABLE]

2. Overlap Algebras

Every complete Boolean algebra is a frame and, classically, every atomic frame (that is, a powerset by proposition 1) is a complete Boolean algebra. The latter fails constructively; a constructive version can be obtained by replacing complete Boolean algebras by Sambin’s overlap algebras, as we now see.

Definition \thethm.

An overlap-algebra (o-algebra) is an overt frame $L$ such that

[TABLE]

for all $x,y\in L$.

The motivating example is given by powersets, where $\mathrm{Pos}(x)$ means “$x$ is inhabited”. To see that (11) holds in this case it is sufficient to make $z$ vary over singletons. Note that for $p\in\Omega$ the statement $\mathrm{Pos}(p)$ is equivalent to $p=1$.

Note that a frame $L$ is an o-algebra if and only if there exists a unary predicate $\mathrm{Pos}$ on $L$ such that (5), (6) and (11) hold. Indeed (7) follows from (5) and (11): assume $\mathrm{Pos}(x)\Rightarrow(x\leq y)$; if $\mathrm{Pos}(z\wedge x)$, then $\mathrm{Pos}(x)$ and so $x\leq y$ by assumption; therefore $z\wedge x\leq z\wedge y$, and hence $\mathrm{Pos}(z\wedge y)$.

Proposition \thethm.

Classically, o-algebras and complete Boolean algebras coincide.

Proof.

Classically, overtness is for free, and $\mathrm{Pos}(x)$ is $x\neq 0$. So the implication $\mathrm{Pos}(z\wedge x)\Rightarrow\mathrm{Pos}(z\wedge y)$ in (11) can be rewritten as $z\wedge y=0\Rightarrow z\wedge x=0$, that is, $z\leq-y\Rightarrow z\leq-x$. Therefore $(\forall z\in L)(\mathrm{Pos}(z\wedge x)\Rightarrow\mathrm{Pos}(z\wedge y))$ becomes simply $-y\leq-x$ and (11) becomes $-y\leq-x\Longrightarrow x\leq y$. This holds identically in an Heyting algebra if and only if it is in fact a Boolean algebra. ∎

Constructively, the previous proposition fails badly, because LEM is equivalent to the statement that $\Omega$ (which is an o-algebra) is Boolean.111The statement “every complete Boolean algebra is an o-algebra” is equivalent to LEM as well (see, for instance, [1] proposition $1.1$).

Given an o-algebra $L$, it is sometimes convenient to introduce a new relation symbol, say $x>\mkern-13.5mu<y$, for the binary predicate $\mathrm{Pos}(x\wedge y)$: this is the overlap relation which gives the name to the structure. If $L$ is a powerset, then $x>\mkern-13.5mu<y$ means that $x$ and $y$ overlap, that is, their intersection is inhabited. Classically, $x>\mkern-13.5mu<y$ is $x\wedge y\neq 0$. Clearly, $\mathrm{Pos}(x)$ is equivalent to $x>\mkern-13.5mu<x$ (and also to $x>\mkern-13.5mu<1$); this suggests that the definition of an o-algebra can be given in terms of $>\mkern-13.5mu<$ (which was Sambin’s original definition).

Proposition \thethm.

For $L$ a complete lattice, the following are equivalent:

1. (1)

$L$* is an o-algebra;* 2. (2)

there exists a binary relation $>\mkern-13.5mu<$ on $L$ that satisfies the following properties identically.

• •

$x>\mkern-13.5mu<y\Longrightarrow y>\mkern-13.5mu<x$* $(\textit{symmetry})$*

• •

$x>\mkern-13.5mu<y\Longrightarrow x>\mkern-13.5mu<(x\wedge y)$* $(\textit{meet closure})$*

• •

$x>\mkern-13.5mu<\bigvee Y\Longrightarrow(\exists y\in Y)(x>\mkern-13.5mu<y)$* $(\textit{splitting of joins})$*

• •

$(x>\mkern-13.5mu<y)\land(y\leq z)\Longrightarrow x>\mkern-13.5mu<z$* $(\textit{monotonicity})$*

• •

$(\forall z\in L)(z>\mkern-13.5mu<x\Rightarrow z>\mkern-13.5mu<y)\Longrightarrow x\leq y$* $(\textit{density})$*

Proof.

The implication $1\Rightarrow 2$ is easy once $x>\mkern-13.5mu<y$ is defined as $\mathrm{Pos}(x\wedge y)$. For instance, splitting of joins holds because binary meets distribute over arbitrary joins (since $L$ is a frame).

As for the reverse implication, we first note that $x>\mkern-13.5mu<y$ is equivalent to $(x\wedge y)>\mkern-13.5mu<(x\wedge y)$ thanks to symmetry, meet closure and monotonicity. Therefore $(x\wedge y)>\mkern-13.5mu<z$ is always equivalent to $z>\mkern-13.5mu<(y\wedge z)$. We now show that $L$ is a frame, that is, $x\wedge\bigvee Y\leq\bigvee\{x\wedge y\ |\ y\in Y\}$. By density, it is sufficient to check that $z>\mkern-13.5mu<x\wedge\bigvee Y$ implies $z>\mkern-13.5mu<\bigvee\{x\wedge y\ |\ y\in Y\}$. Now $z>\mkern-13.5mu<x\wedge\bigvee Y$ is equivalent to $z\wedge x>\mkern-13.5mu<\bigvee Y$; so there is a $y\in Y$ with $z\wedge x>\mkern-13.5mu<y$, that is, $z>\mkern-13.5mu<x\wedge y$. So $z>\mkern-13.5mu<\bigvee\{x\wedge y\ |\ y\in Y\}$ by monotonicity. Finally, let us define $\mathrm{Pos}(x)$ as $x>\mkern-13.5mu<x$. The only condition on $\mathrm{Pos}$ which needs some proof is (7) which follows from (5) and (11), as already noticed. ∎

For $L$ an o-algebra, the characterization (10) of an atom $a\in L$ becomes

[TABLE]

By proposition 1, atomic frames, atomic o-algebras and powersets all amount to the same thing.

2.1. Non-atomic o-algebras

Given any complete Heyting algebra $L$, the set $L_{--}$ = $\{y\in L\ |\ y=--y\}$ has a natural structure of complete Boolean algebra (and every complete Boolean algebra is of this form, because $L_{--}=L$ if $L$ is Boolean).

A similar result holds for o-algebras [1]: if $L$ is an overt frame, then the set of all $y\in L$ such that $y$ = $\bigvee\{x\ |\ \forall z(\mathrm{Pos}(z\wedge x)\Rightarrow\mathrm{Pos}(z\wedge y))\}$ is an o-algebra. In particular, if $L=\tau$ where $(X,\tau)$ is a topological space, then we get an o-algebra by considering the set of all $Y\subseteq X$ such that $Y=\mathrm{int}\,\mathrm{cl}\,\mathrm{int}\,Y$, where $\mathrm{int}$ and $\mathrm{cl}$ are the interior operator and the closure operator corresponding to $\tau$.222Here $x\in\mathrm{cl}Y$ means that every open neighbourhood of $x$ overlaps $Y$. Assuming that $\mathrm{cl}Y$ is the (set-theoretic pseudo-)complement of the interior of the (set-theoretic pseudo-)complement of $Y$ is tantamount to assuming LEM. This is a constructive version of the well-known fact that the regular open sets in a topological space form a complete Boolean algebra, which is not atomic, in general, and often with no atoms [2].

3. Morphisms between overlap algebras

In section 5 we whall study a category of overlap algebras which, from a classical point of view, is just the category cBa of complete Boolean algebras. For the time being, instead, we are going to study a more general kind of morphisms between o-algebras which, classically, correspond to join-preserving maps between complete Boolean algebras.

Sambin’s aim in introducing the category $\mathbf{OA}$ of o-algebras was to obtain an extension of the category $\mathbf{Rel}$ of sets and relations. The definition of an arrow in OA makes the assignment $X\mapsto\mathrm{Pow}(X)$ a functor $\mathrm{Pow}$ from $\mathbf{Rel}$ to $\mathbf{OA}$ which is full, faithful and injective on objects (Proposition 4).

In the category $\mathbf{Rel}$ a morphism is a binary relation and the composition $S\circ R\subseteq X\times Z$ of the relations $R\subseteq X\times Y$ and $S\subseteq Y\times Z$ is defined by $x(S\circ R)z\Leftrightarrow(\exists y\in Y)(xRy\land ySz)$.

Given $R\subseteq X\times Y$, its inverse image $R^{-1}:\mathrm{Pow}(Y)\to\mathrm{Pow}(X)$ is the function which maps $Y^{\prime}\subseteq Y$ to $R^{-1}(Y^{\prime})$ = $\{x\in X\ |\ (\exists y\in Y^{\prime})(xRy)\}$. Clearly, $R^{-1}$ is the identity function on $\mathrm{Pow}(X)$ if, and only if, $R$ is the equality on $X$.

Lemma \thethm.

For $R\subseteq X\times Y$ and $S\subseteq Y\times Z$, $(S\circ R)^{-1}=R^{-1}\circ S^{-1}$.

Proof.

For every $x\in X$ and $D\subseteq Z$, $x\in(S\circ R)^{-1}(D)$ iff $x(S\circ R)z$ for some $z\in D$; this means that $xRy$ and $ySz$ for some $y\in Y$, and some $z\in D$. In other words, $x\in R^{-1}(S^{-1}(D))$. ∎

Each binary relation $R\subseteq X\times Y$ has a “symmetric” $R^{\dagger}\subseteq Y\times X$, where $yR^{\dagger}x$ iff $xRy$. Its inverse image is a function $(R^{\dagger})^{-1}:\mathrm{Pow}(X)\to\mathrm{Pow}(Y)$, the direct image of $R$, such that

[TABLE]

This motivates the following study of symmetrizable functions.

3.1. Symmetrizable functions

Definition \thethm.

Let $L$ and $M$ be two o-algebras.333Such a notion makes sense also for $L$ and $M$ overt frames, with $x>\mkern-13.5mu<y$ replaced by $\mathrm{Pos}(x\wedge y)$. Two functions $f:L\to M$ and $g:M\to L$ are symmetric (or conjugated [6]) if

[TABLE]

for every $x\in L$ and $y\in M$.444Classically, the same idea can be expressed by the condition $f(x)\wedge y=0$ $\Leftrightarrow$ $x\wedge g(y)=0$, which is the definition originally proposed [6].

For instance, the function $a\wedge\_:L\to L$ is self-symmetric, for every element $a$ in an o-algebra $L$.

A function between o-algebras $f:L\to M$ has at most one symmetric.555This fact fails, in general, when $L$ is an overt frame but not an o-algebra. Indeed, if $g_{1},g_{2}:M\to L$ are symmetric of $f$, then $x>\mkern-13.5mu<g_{1}(y)$ $\Leftrightarrow$ $x>\mkern-13.5mu<g_{2}(y)$ for every $x$ and $y$; and hence $g_{1}(y)=g_{2}(y)$ for every $y$, by density in $L$.

Definition \thethm.

A function $f:L\to M$ between two o-algebras is symmetrizable if $f$ has a symmetric. In that case, we write $f^{\dagger}$ for the symmetric of $f$.

Clearly if $f$ is symmetrizable, then $f^{\dagger}$ is symmetrizable too and $(f^{\dagger})^{\dagger}=f$. Note that if $f$ is symmetrizable, then $f^{\dagger}$ can be defined in terms of $f$ by means of the formula $f^{\dagger}(y)$ = \bigvee\{x\in L\ |\ (\forall z\in L)\big{(}z>\mkern-13.5mu<x\Rightarrow f(z)>\mkern-13.5mu<y\big{)}\}.

Proposition \thethm.

Let $f:L\to M$ be a function between o-algebras. If $f$ is symmetrizable, then $f$ preserves all joins; and the converse holds classically.

Proof.

For every $y\in M$, we have $y>\mkern-13.5mu<f(\bigvee_{i}x_{i})$ iff $f^{\dagger}y>\mkern-13.5mu<\bigvee_{i}x_{i}$ iff $f^{\dagger}y>\mkern-13.5mu<x_{i}$ for some $i$ iff $y>\mkern-13.5mu<fx_{i}$ for some $i$ iff $y>\mkern-13.5mu<\bigvee_{i}fx_{i}$. This shows (by density) that $f(\bigvee_{i}x_{i})=\bigvee_{i}fx_{i}$.

Classically, an o-algebra is exactly a cBa. If $f:L\rightarrow M$ preserves all joins, then it has a right adjoint $\forall_{f}$. We claim that $f^{\dagger}$ does exist and $f^{\dagger}(y)=-\forall_{f}(-y)$. For $x>\mkern-13.5mu<-\forall_{f}(-y)$ $\Leftrightarrow$ $x\wedge-\forall_{f}(-y)\neq 0$ $\Leftrightarrow$ $x\nleq\forall_{f}(-y)$ $\Leftrightarrow$ $f(x)\nleq-y$ $\Leftrightarrow$ $f(x)\wedge y\neq 0$ $\Leftrightarrow$ $f(x)>\mkern-13.5mu<y$. ∎

Remark \thethm.

Classical logic is necessary in the second part of the previous proposition in the sense that LEM follows from the assumption that every join-preserving function between o-algebras is symmetrizable, as we now see. The argument is based on the fact that LEM is equivalent to assuming that every topological space in which $\mathrm{cl}$ is the identity operator must be discrete.666The following is essentially the same proof given in [1]. Let us start by constructing a family of topological spaces $(2,\tau_{p})$ where $2=\{0,1\}$ and $p\in\Omega$. Let $\tau_{p}$ be the topology of those subsets $X\subseteq 2$ such that if $X$ is inhabited, then either $p$ holds or $p$ implies $X=2$. It is not difficult to check that $\tau_{p}$ is a topology (and $\tau_{p}$ is discrete if either $p$ or $\neg p$, which is always the case classically). We claim that every $X\subseteq 2$ is closed. If $x\in\mathrm{cl}X$, then the open set $\{y\ |\ (y=x)\vee p\}$ must overlap $X$. So either $x\in X$ or $p$; in the latter case, however, $\tau_{p}$ is the discrete topology, and hence $x\in X$ anyway. Therefore $\mathrm{cl}$ is the identity. Now if $\tau_{p}$ were discrete, then $\{0\}$ (and $\{1\}$) would be open, hence $p\vee\neg p$ would be true. Let us consider any topological space $(X,\tau)$ such that $cl=id$; so $\tau$ is an o-algebra (because every open set is regular). Let $f$ be the inclusion map $\tau\hookrightarrow\mathrm{Pow}(X)$ and let us assume that $f^{\dagger}$ exists, that is, $U>\mkern-13.5mu<Y$ $\Leftrightarrow$ $U>\mkern-13.5mu<f^{\dagger}(Y)$ for every subset $Y$ and every open $U$. This means that $cl(Y)=clf^{\dagger}(Y)$ for every $Y$. Since $cl=id$, we get $Y=f^{\dagger}(Y)$, and hence $Y$ is open, for every $Y$.

Proposition \thethm.

Let $f:L\to M$ be a join preserving function between two o-algebras. If $L$ is atomic, then $f$ is symmetrizable.

Proof.

Up to order-isomorphism, we can assume that $L$ is $\mathrm{Pow}(X)$ for some $X$. Put $f^{\dagger}y=\{x\in X\ |\ f(\{x\})>\mkern-13.5mu<y\}$. ∎

It is a corollary of the previous proposition (but it can be easily checked directly) that the mapping $X\mapsto\bigvee X$ gives a symmetrizable map from $\mathrm{Pow}(L)$ to $L$. Its symmetric is given by $y\mapsto\{x\in L\ |\ x>\mkern-13.5mu<y\}$.

Remark \thethm.

Note that a function $f:L\to\Omega$ is symmetrizable if and only if there is $a\in L$ such that $f(x)=(x>\mkern-13.5mu<a)$ for all $x\in L$. Indeed, given $a\in L$, the mapping $x\mapsto(x>\mkern-13.5mu<a)$ is symmetrizable, and its symmetric maps $p\in\Omega$ to $\bigvee\{x\in L\ |\ (x=a)\land p\}$ (classically, of course, this is just $a$ if $p=1$, and [math] if $p=0$). Conversely, given a symmetrizable $f$, put $a=f^{\dagger}(1)$. Also note that $a$ is an atom if and only if $f$ preserves finite meets.

{propC}

[[6, Theorem $1.15.(iii)$]] Let $f:L\to M$ and $g:M\to L$ be two functions between o-algebras. Then $f$ and $g$ are symmetric if and only if all the following conditions hold identically:

1. (1)

$\mathrm{Pos}(f(x))\Rightarrow\mathrm{Pos}(x)$ (classically, $f(0)=0$); 2. (2)

$\mathrm{Pos}(g(y))\Rightarrow\mathrm{Pos}(y)$ (classically, $g(0)=0$); 3. (3)

$f(x)\wedge y\leq f(x\wedge g(y))$; 4. (4)

$x\wedge g(y)\leq g(f(x)\wedge y)$.

Proof.

Assume that $f$ and $g$ are symmetric. Now $\mathrm{Pos}(f(x))$ can be rewritten as $x>\mkern-13.5mu<g(f(x))$; so $x>\mkern-13.5mu<1$, that is, $\mathrm{Pos}(x)$; this proves 1, and hence 2 by symmetry.777Note that $\mathrm{Pos}(fx)$ $\Rightarrow$ $\mathrm{Pos}(x)$ holds true already in the case of overt frames. Indeed, since $x$ = $\bigvee\{x^{\prime}\ |\ \mathrm{Pos}(x^{\prime})\land(x^{\prime}\leq x)\}$ by (8), $fx$ = $\bigvee\{fx^{\prime}\ |\ \mathrm{Pos}(x^{\prime})\land(x^{\prime}\leq x)\}$. So if $\mathrm{Pos}(fx)$, then $\mathrm{Pos}(fx^{\prime})$ for some $x^{\prime}\leq x$ with $\mathrm{Pos}(x^{\prime})$; in particular, $\mathrm{Pos}(x^{\prime})$ for some $x^{\prime}\leq x$, and hence $\mathrm{Pos}(x)$. To check 3 (and 4) we use density: $z>\mkern-13.5mu<f(x)\wedge y$ is equivalent to $f(x)>\mkern-13.5mu<z\wedge y$ and hence to $x>\mkern-13.5mu<g(z\wedge y)$; since $g$ is monotone (because it preserves joins), we also have $x>\mkern-13.5mu<g(z)\wedge g(y)$, which is equivalent to $g(z)>\mkern-13.5mu<x\wedge g(y)$ and hence to $z>\mkern-13.5mu<f(x\wedge g(y))$.

Conversely, if $f(x)>\mkern-13.5mu<y$, that is, $\mathrm{Pos}(f(x)\wedge y)$, then also $\mathrm{Pos}(f(x\wedge g(y)))$ by 3; so $\mathrm{Pos}(x\wedge g(y))$ by 1, that is, $x>\mkern-13.5mu<g(y)$; and symmetrically for the other direction. ∎

As a corollary, if $f$ is symmetrizable, then $fx$ = $fx\wedge 1$ $\leq$ $f(x\wedge f^{\dagger}(1))$ $\leq$ $ff^{\dagger}(fx\wedge 1)$ = $ff^{\dagger}fx$. And, similarly, $f^{\dagger}y$ $\leq$ $f^{\dagger}ff^{\dagger}y$.

Proposition \thethm.

Let $f:L\to M$ be a symmetrizable function between o-algebras. Then the following conditions are equivalent:

1. (1)

if $fx_{1}>\mkern-13.5mu<fx_{2}$, then $x_{1}>\mkern-13.5mu<x_{2}$; 2. (2)

$f$* preserves binary meets;* 3. (3)

$f^{\dagger}fx\leq x$* for every $x$.*

Moreover the following are equivalent:

1. (4)

if $x_{1}>\mkern-13.5mu<x_{2}$, then $fx_{1}>\mkern-13.5mu<fx_{2}$; 2. (5)

if $\mathrm{Pos}(x)$, then $\mathrm{Pos}(fx)$; 3. (6)

$f^{\dagger}1=1$; 4. (7)

$x\leq f^{\dagger}fx$* for every $x$.*

Proof.

$1\Rightarrow 2$: $z>\mkern-13.5mu<(fx_{1}\wedge fx_{2})$ can be rewritten as $f^{\dagger}(z\wedge fx_{1})>\mkern-13.5mu<x_{2}$, which yields $(f^{\dagger}z\wedge f^{\dagger}fx_{1})>\mkern-13.5mu<x_{2}$; this is equivalent to $fx_{1}>\mkern-13.5mu<f(f^{\dagger}z\wedge x_{2})$, which implies $x_{1}>\mkern-13.5mu<(f^{\dagger}z\wedge x_{2})$ by assumption; in other words, $f^{\dagger}z>\mkern-13.5mu<(x_{1}\wedge x_{2})$, that is, $z>\mkern-13.5mu<f(x_{1}\wedge x_{2})$.

$2\Rightarrow 3$: $y>\mkern-13.5mu<f^{\dagger}fx$ iff $fy>\mkern-13.5mu<fx$ iff $(fy\wedge fx)>\mkern-13.5mu<1$ iff $f(y\wedge x)>\mkern-13.5mu<1$ iff $(y\wedge x)>\mkern-13.5mu<f^{\dagger}1$, and hence $(y\wedge x)>\mkern-13.5mu<1$, that is, $y>\mkern-13.5mu<x$.

$3\Rightarrow 1$: if $fx_{1}>\mkern-13.5mu<fx_{2}$, then $x_{1}>\mkern-13.5mu<f^{\dagger}fx_{2}$ ($\leq x_{2}$), and hence $x_{1}>\mkern-13.5mu<x_{2}$.

$4\Rightarrow 5$: since $\mathrm{Pos}(x)$ is $x>\mkern-13.5mu<x$, and $\mathrm{Pos}(fx)$ is $fx>\mkern-13.5mu<fx$.

$5\Rightarrow 6$: $z>\mkern-13.5mu<1$ iff $\mathrm{Pos}(z)$, which implies $\mathrm{Pos}(fz)$; this is equivalent to $fz>\mkern-13.5mu<1$, that is, $z>\mkern-13.5mu<f^{\dagger}1$.

$6\Rightarrow 7$: $z>\mkern-13.5mu<x$ iff $(z\wedge x)>\mkern-13.5mu<1$ iff $(z\wedge x)>\mkern-13.5mu<f^{\dagger}1$ iff $f(z\wedge x)>\mkern-13.5mu<1$; the last implies $(fz\wedge fx)>\mkern-13.5mu<1$, which is equivalent to $fz>\mkern-13.5mu<fx$ and hence to $z>\mkern-13.5mu<f^{\dagger}fx$.

$7\Rightarrow 4$: if $x_{1}>\mkern-13.5mu<x_{2}$ ($\leq f^{\dagger}fx_{2}$), then $x_{1}>\mkern-13.5mu<f^{\dagger}fx_{2}$, that is, $fx_{1}>\mkern-13.5mu<fx_{2}$. ∎

4. The category OA of overlap algebras

The identity function $id:L\rightarrow L$ on an o-algebra $L$ is symmetrizable with $id^{\dagger}=id$. For $L$, $M$, $N$ o-algebras, if $f:L\rightarrow M$ and $g:M\rightarrow N$ are symmetrizable, then $g\circ f$ is symmetrizable too and

[TABLE]

since $g(f(x))>\mkern-13.5mu<z\Leftrightarrow f(x)>\mkern-13.5mu<g^{\dagger}(z)\Leftrightarrow x>\mkern-13.5mu<f^{\dagger}(g^{\dagger}(z))$. So o-algebras and symmetrizable functions form a category OA. We will sometimes refer to arrows in OA as overlap-morphisms or o-morphisms.

The category OA is a dagger category, that is, a category $\mathcal{C}$ equipped with an endofunctor $(\_)^{\dagger}:\mathcal{C}^{op}\rightarrow\mathcal{C}$ which is the identity on objects and an involution on arrows.

Proposition \thethm.

Let $\mathrm{Pow}:\mathbf{Rel}^{op}\rightarrow\mathbf{OA}$ be the functor that associates to every relation $R\subseteq X\times Y$ its inverse image $\mathrm{Pow}(R)=R^{-1}:\mathrm{Pow}(Y)\to\mathrm{Pow}(X)$. Then $\mathrm{Pow}$ is a full and faithful functor. Moreover, $\mathrm{Pow}(R^{\dagger})=(\mathrm{Pow}(R))^{\dagger}$.

Proof.

The map $\mathrm{Pow}(R)$ is symmetrizable by equation (13), and $(\mathrm{Pow}(R))^{\dagger}=\mathrm{Pow}(R^{\dagger})$. Lemma 3 shows that $\mathrm{Pow}$ is a functor.

Given $f:\mathrm{Pow}(Y)\to\mathrm{Pow}(X)$, let $R\subseteq X\times Y$ be the relation defined as $xRy\Leftrightarrow x\in f(\{y\})$. Then $x\in R^{-1}(D)$ iff $x\in f(\{y\})$ for some $y\in D$ iff $x\in\bigcup_{y\in D}f(\{y\})$ = $f(\bigcup_{y\in D}\{y\})$ = $f(D)$. This shows that $\mathrm{Pow}$ is full. And $\mathrm{Pow}$ is clearly faithful, for if $R,S\subseteq X\times Y$ are such that $R^{-1}=S^{-1}$, then $xRy\Leftrightarrow x\in R^{-1}(\{y\})\Leftrightarrow x\in S^{-1}(\{y\})\Leftrightarrow xSy$. ∎

4.1. Iso-, mono- and epi-morphisms in OA

Proposition \thethm.

A bijective function $f:L\to M$ is an isomorphism in OA if and only if it is an order-isomorphism. In that case $f^{\dagger}=f^{-1}$ (isomorphisms in OA are “unitary”).

Proof.

One direction is trivial because all arrows in OA are monotone functions. Conversely, let $f$ be an order-isomorphism; we claim that $f$ is symmetrizable and $f^{\dagger}=f^{-1}$. As $f$ and $f^{-1}$ preserve binary meets, items 3 and 4 of propositions 3.1 hold; it remains to be shown that $\mathrm{Pos}(f(x))$ implies $\mathrm{Pos}(x)$, and similarly for $f^{-1}$. This follows from the fact that $f$ and $f^{-1}$ preserve joins. Indeed, by (8), we have $f(x)$ = $\bigvee\{f(z)\ |\ \mathrm{Pos}(z)\land(z\leq x)\}$. So if $\mathrm{Pos}(f(x))$ holds, then $\mathrm{Pos}(f(z))$ holds for some $z\leq x$ with $\mathrm{Pos}(z)$. In particular, also $\mathrm{Pos}(x)$ holds. ∎

So $L$ and $M$ are isomorphic in OA if and only if they are isomorphic as posets. As a corollary, a join-preserving bijection between o-algebras is always symmetrizable888In this case, $f$ is an order-isomorphism because $f^{-1}$ preserves joins as well, for $f^{-1}(\bigvee_{i}y_{i})$ = $f^{-1}(\bigvee_{i}ff^{-1}y_{i})$ = $f^{-1}f(\bigvee_{i}f^{-1}y_{i})$ = $\bigvee_{i}f^{-1}y_{i}$. (compare with Remark 3.1).

Remark \thethm.

If $f$ is an isomorphism in OA, then $fx_{1}>\mkern-13.5mu<fx_{2}\Leftrightarrow x_{1}>\mkern-13.5mu<x_{2}$ holds true by Proposition 3.1.

Proposition \thethm.

Let $m:L\rightarrow M$ be an arrow in OA. Then $m$ is a monomorphism if and only if $m$ is injective.

Proof.

If $m$ is an injective function, then it is trivially a monomorphism.

Conversely, assume $m(a)=m(b)$ with $a,b\in L$. Let $f_{a}(x)$ and $f_{b}(x)$ be the truth values of $x>\mkern-13.5mu<a$ and $x>\mkern-13.5mu<b$, respectively. In view of Remark 3.1, $f_{a}$ and $f_{b}$ are two o-morphisms from $L$ to $\Omega$. Now $f_{a}m^{\dagger}y$ = $(m^{\dagger}y>\mkern-13.5mu<a)$ = $(y>\mkern-13.5mu<ma)$ = $(y>\mkern-13.5mu<mb)$ = $(m^{\dagger}y>\mkern-13.5mu<b)$ = $f_{b}m^{\dagger}y$. So $f_{a}\circ m^{\dagger}$ = $f_{b}\circ m^{\dagger}$, and hence $m\circ f_{a}^{\dagger}$ = $m\circ f_{b}^{\dagger}$. Since $m$ is mono, we get $f_{a}^{\dagger}$ = $f_{b}^{\dagger}$; therefore $f_{a}$ = $f_{b}$, that is, $a=b$ (by density). ∎

Note that a join-preserving map $f:L\rightarrow M$ between posets is injective if and only if $\forall_{f}\circ f=id_{L}$ (apply the triangular identity $f\circ\forall_{f}\circ f=f$). Similarly, $f$ is surjective if and only if $f\circ\forall_{f}=id_{M}$.

Proposition \thethm.

Let $f:L\rightarrow M$ be an arrow in OA; then

1. (1)

$f$* is an epimorhism if and only if $f^{\dagger}$ is a monomorphism;* 2. (2)

if $f$ is surjective, then $f$ is an epimorphism; 3. (3)

classically, if $f$ is an epimorphism, then $f$ is surjective.

Proof.

Item 1 holds in any dagger category; 2 is trivial.

Let $f$ be epi, and assume LEM. Then $f^{\dagger}$ is injective, and $f^{\dagger}(y)$ = $-\forall_{f}(-y)$. Therefore also $\forall_{f}$ is injective, for $\forall_{f}y_{1}$ = $\forall_{f}y_{2}$ iff $-f^{\dagger}(-y_{1})$ = $-f^{\dagger}(-y_{2})$ iff $f^{\dagger}(-y_{1})$ = $f^{\dagger}(-y_{2})$ iff $-y_{1}$ = $-y_{2}$ iff $y_{1}$ = $y_{2}$. But $\forall_{f}\circ f\circ\forall_{f}$ = $\forall_{f}$ (triangular identity); hence $f(\forall_{f}y)$ = $y$ for all $y\in M$; so $f$ is surjective. ∎

It is possible to construct a Brouwerian counterexample to the fact that epic implies surjective. Let us consider a topological space $(X,\tau)$ in which the closure operator cl is the identity id (see section 3.1). Let $f:\mathrm{Pow}(\tau)\rightarrow\mathrm{Pow}(X)$ be the map $\{A_{i}\}_{i\in I}\mapsto\cup_{i\in I}A_{i}$; it is symmetrizable and $f^{\dagger}(Y)$ = $\{A\in\tau|Y>\mkern-13.5mu<A\}$.999This is a consequence of proposition 3.1. Here is a direct proof: $f(\{A_{i}\}_{i\in I})>\mkern-13.5mu<Y$ iff $(\bigcup_{i\in I}A_{i})>\mkern-13.5mu<Y$ iff $(\exists i\in I)(A_{i}>\mkern-13.5mu<Y)$ iff $(\exists i\in I)(A_{i}\in f^{\dagger}(Y))$ iff $\{A_{i}\}_{i\in I}>\mkern-13.5mu<f^{\dagger}(Y)$. Now $f^{\dagger}$ is injective, because $f^{\dagger}(Y_{1})$ = $f^{\dagger}(Y_{2})$ iff $(\forall A\in\tau)(Y_{1}>\mkern-13.5mu<A\Leftrightarrow Y_{2}>\mkern-13.5mu<A)$ iff $\mathrm{cl}Y_{1}=\mathrm{cl}Y_{2}$ iff $Y_{1}=Y_{2}$. In other words, $f^{\dagger}$ is monic and so $f$ is epic. However, if $f$ were surjective, then every $Y\subseteq X$ would be open. In view of this, if the implication “$f$ epi $\Rightarrow$ $f$ surjective” were true, then also “$\textit{cl}=\textit{id}\Rightarrow\textit{int}=\textit{id}$” would be true, which is an intuitionistic “taboo” (see footnote 6 on page 6).

Proposition \thethm.

If $m$ is a mono in OA, then the following hold identically:

1. (1)

if $x_{1}>\mkern-13.5mu<x_{2}$, then $mx_{1}>\mkern-13.5mu<mx_{2}$; 2. (2)

if $\mathrm{Pos}(x)$, then $\mathrm{Pos}(mx)$; 3. (3)

$m^{\dagger}1=1$; 4. (4)

$x\leq m^{\dagger}mx$.

Symmetrically, If $e$ is an epi in OA, then the following hold identically:

1. (1)

if $y_{1}>\mkern-13.5mu<y_{2}$, then $e^{\dagger}y_{1}>\mkern-13.5mu<e^{\dagger}y_{2}$; 2. (2)

if $\mathrm{Pos}(y)$, then $\mathrm{Pos}(e^{\dagger}y)$; 3. (3)

$e1=1$; 4. (4)

$y\leq ee^{\dagger}y$.

Proof.

Recall from Proposition 3.1 that $mx\wedge y\leq m(x\wedge m^{\dagger}y)$ for all $x$ and $y$. In particular, $m1\leq mm^{\dagger}1$ and hence $m1=mm^{\dagger}1$. If $m$ is a mono, that is, it is injective, then $m^{\dagger}1=1$, which is item 6 of Proposition 3.1. The second part follows by applying the same argument to $e^{\dagger}$. ∎

4.2. Limits and co-limits in OA

Limits and colimits in a dagger category are mutually closely related: an object $C$ together with arrows $\alpha_{i}:A_{i}\to C$ is the colimit of a diagram $f_{i,j}^{k}:A_{i}\to A_{j}$ if and only if the same $C$ together with ${\alpha_{i}}^{\dagger}:C\to A_{i}$ is the limit of the diagram $(f_{i,j}^{k})^{\dagger}:A_{j}\to A_{i}$.

Lemma \thethm.

Let $\{L_{i}\}_{i\in I}$ be a family of o-algebras. Then the set-theoretic product $\Pi_{i\in I}L_{i}$ is an o-algebra with respect to pointwise joins and meets, and $\mathrm{Pos}(f)$ holds in $\Pi_{i\in I}L_{i}$ if and only if $\mathrm{Pos}(f_{i})$ holds in some $L_{i}$.

Proof.

Let us check (11), the other properties being clear. Given $f$ and $g$, assume $\mathrm{Pos}(h\wedge f)\Rightarrow\mathrm{Pos}(h\wedge g)$ for all $h$. For any given $k\in I$ and $z\in L_{k}$, let us define $h$ as $h_{i}=\bigvee\{x\in L_{i}\ |\ (i=k)\land(x=z)\}$. By assumption we then have $\mathrm{Pos}(z\wedge f_{k})\Rightarrow\mathrm{Pos}(z\wedge g_{k})$, for all $k\in I$ and for all $z\in L_{k}$. So $f_{k}\leq g_{k}$ by (11) in $L_{k}$, for all $k\in I$; therefore $f\leq g$. ∎

Proposition \thethm.

The category $\mathbf{OA}$ has arbitrary products (and coproducts).

Proof.

We claim that $\Pi_{i\in I}L_{i}$, as defined in the previous lemma, is the product of the family of o-algebras $\{L_{i}\}_{i\in I}$. Let $\pi_{k}$ be the $k$-th projection, and define ${\pi_{k}}^{\dagger}(z)$ to be the function $i\mapsto\bigvee\{x\in L_{i}\ |\ (i=k)\land(x=z)\}$. Then $f>\mkern-13.5mu<{\pi_{k}}^{\dagger}(z)$ iff $f_{i}>\mkern-13.5mu<\bigvee\{x\in L_{i}\ |\ (i=k)\land(x=z)\}$ for some $i\in I$ iff $f_{k}>\mkern-13.5mu<z$ iff $\pi_{k}(f)>\mkern-13.5mu<z$. Therefore the set-theoretic projections are o-moprhisms.

Let $\{g_{i}:M\to L_{i}\}_{i\in I}$ be a family of morphisms in OA. We claim that there exists a unique morphism $h:M\to\Pi_{i\in I}L_{i}$ such that $\pi_{i}\circ h$ = $f_{i}$ for all $i$. The only possible candidate for $h$ is the mapping $x\mapsto h(x)$ with $h(x)_{i}=g_{i}(x)$. Let us check that it is symmetrizable with $h^{\dagger}(f)$ = $\bigvee_{i\in I}{g_{i}}^{\dagger}(f_{i})$. We have that $h(x)>\mkern-13.5mu<f$ $\Leftrightarrow$ $h(x)_{i}>\mkern-13.5mu<f_{i}$ for some $i\in I$ $\Leftrightarrow$ $g_{i}(x)>\mkern-13.5mu<f_{i}$ for some $i\in I$ $\Leftrightarrow$ $x>\mkern-13.5mu<{g_{i}}^{\dagger}(f_{i})$ for some $i\in I$ $\Leftrightarrow x>\mkern-13.5mu<\bigvee_{i\in I}{g_{i}}^{\dagger}(f_{i})$ $\Leftrightarrow$ $x>\mkern-13.5mu<h^{\dagger}(f)$. ∎

Note that $\mathrm{Pow}(\emptyset)$ is a zero object (both initial and terminal), because given an arbitrary o-algebra $L$, there exists a unique morphism $f:\mathrm{Pow}(\emptyset)\rightarrow L$, namely, $f(\emptyset)=0$ ($f$ has to preserve joins); and $f$ is the symmetric of the unique function $g:L\to\mathrm{Pow}(\emptyset)$, namely, the constant function with value $\emptyset$ (both $\emptyset>\mkern-13.5mu<x$ and $\emptyset>\mkern-13.5mu<gx$ are always false).

The category OA is not complete.

A category $\mathcal{C}$ is complete if it has all (small) limits. It is well-known that a category with all (small) products is complete if and only if it has equalizers. We are going to show that OA does not have equalizers, in general, hence it is not complete. This fact is independent from LEM, that is, OA is not complete even classically, as we now see.

Recall that, classically, OA is the category of complete Boolean algebras and join-preserving maps. Let us consider the complete Boolean algebras $\Omega=\mathrm{Pow}(1)\cong 2=\{0,1\}$ and $L=\{0,a,-a,1\}\cong\mathrm{Pow}(2)$. Let $f,g:L\to 2$ be two maps defined by $f(0)=g(0)=0$, $f(1)=g(1)=1$, $f(a)=g(a)=1$, $f(-a)=0$ and $g(-a)=1$. Clearly both $f$ and $g$ preserves joins. We claim that there is no equalizer of $f$ and $g$. By way of contradiction let us assume that $e:E\to L$ is the equalizer of $f$ and $g$. In particular $e$ is mono, that is, injective; and $-a$ is not in the image of $e$. Therefore, up to isomorphism we have only two possibilities for $E$, namely, $E=1=\mathrm{Pow}(\emptyset)$, and $E=2$. In particular, the image of $e$ contains at most two elements. Now consider the function $t:L\to L$ define by $t(0)=0$, $t(a)=a$, $t(1)=1=t(-a)$. It is easy to check that $t$ preserves joins and that $f\circ t=g\circ t$. So there must exist (a unique) $h:L\rightarrow E$ such that $e\circ h=t$. This is impossible because the image of $t$ contains three elements.

Remark \thethm.

The argument above shows a case in which a weak equalizer exists ($t:L\to L$ is a weak equalizer of $f$ and $g$ because any other $h:X\to L$ with $fh=gh$ factors through $t$, actually $h=th$). And weak equalizers always exist in Rel. So it is natural to ask whether OA has weak equalizers as well: this is an open problem.

The functor $\mathrm{Pow}:\mathbf{Rel}^{op}\rightarrow\mathbf{OA}$ preserves (co)products. Indeed, it is well-known that (co)products in $\mathbf{Rel}$ are given by disjoint unions; and the powerset of a disjoint union $\Sigma_{i\in I}X_{i}$ is the set-theoretic product of the powersets of the $X_{i}$’s, that is, $\mathrm{Pow}(\Sigma_{i\in I}X_{i})$ = $\Pi_{i\in I}\mathrm{Pow}(X_{i})$.

5. Overlap-frames and overlap-locales

From now on, we restrict our attention to o-morphisms $f$ that preserve finite meets (note that $f^{\dagger}$ need not preserve finite meets). Let OFrm be the corresponding subcategory of OA. So OFrm is also a subcategory of the category Frm of frames, hence the name. Note that the functor $\mathrm{Pow}$ restricts to a fucntor $\mathbf{Set}^{op}\to\mathbf{OFrm}$ because $R^{-1}$ preserves finite intersections if and only if $R$ is a function.

Lemma \thethm.

Let $f:L\rightarrow M$ be a morphism in OA; then the following are equivalent:

1. (1)

$f$* preserves finite meets;* 2. (2)

$f^{\dagger}\dashv f$.

Proof.

By Proposition 3.1, $f$ preserves binary meets iff $f^{\dagger}fx\leq x$, and $f1=1$ iff $y\leq ff^{\dagger}y$. ∎

A frame homomorphism $f$ is open [7, 4] if it has a left adjoint $\exists_{f}$ which satisfies Frobenius reciprocity condition $\exists_{f}(f(x)\wedge y)=x\wedge\exists_{f}(y)$. Equivalently, $f$ is open if it preserves the Heyting implication and arbitrary meets. For instance, the unique frame homomorphism $!:\Omega\to L$ is open if and only if the frame $L$ is overt (in which case $\exists_{!}=\mathrm{Pos}$).

All arrows $f$ in OFrm are open with $\exists_{f}=f^{\dagger}$; actually the following, more general, result holds.

Proposition \thethm.

Let $f:L\to M$ be a function between o-algebras. Then the following are equivalent:

1. (1)

$f$* is symmetrizable and preserves finite meets;* 2. (2)

$f$* is an open frame homomorphism;* 3. (3)

$f$* preserves all joins and meets, and the Heyting implication.*

Proof.

$(1\Rightarrow 2)$: $z>\mkern-13.5mu<f^{\dagger}(fx\wedge y)$ iff $fz>\mkern-13.5mu<fx\wedge y$ iff $fz\wedge fx>\mkern-13.5mu<y$ iff $f(z\wedge x)>\mkern-13.5mu<y$ iff $z\wedge x>\mkern-13.5mu<f^{\dagger}y$ iff $z>\mkern-13.5mu<x\wedge f^{\dagger}y$.

$(2\Rightarrow 3)$: well-known.

$(3\Rightarrow 1)$: $fx>\mkern-13.5mu<y$ iff $\mathrm{Pos}_{M}(fx\wedge y)$ iff101010$\mathrm{Pos}_{M}$ = $\mathrm{Pos}_{L}\circ\exists_{f}$ because $!_{M}$ = $f\circ!_{L}$. $\mathrm{Pos}_{L}\exists_{f}(fx\wedge y)$ iff $\mathrm{Pos}_{L}(x\wedge\exists_{f}y)$ iff $x>\mkern-13.5mu<\exists_{f}y$. ∎

So OFrm is the category of o-algebras and open frame homomorphisms. Classically, OFrm is just the category cBa of complete Boolean algebras.

5.1. Subobjects, equalizers and completeness of OFrm

Proposition 4.1 holds for OFrm too, because the morphisms $f_{a}^{\dagger}$ and $f_{b}^{\dagger}$ which appear in that proof preserve finite meets. Therefore, every monomorphism $m$ in OFrm is injective; by triangular identity, this is equivalent to the equation $m^{\dagger}\circ m=id$; and this happens precisely $x_{1}>\mkern-13.5mu<x_{2}$ $\Leftrightarrow$ $mx_{1}>\mkern-13.5mu<mx_{2}$ for all $x_{1}$, $,x_{2}$ (see Propositions 3.1 and 4.1).

Let $f:L\rightarrow M$ be any arrow in OFrm. Then the set-theoretic image $f[L]$ = $\{f(x)\ |\ x\in L\}$ is a sub-frame of $M$, and it is an o-algebra where $fx_{1}>\mkern-13.5mu<_{f[L]}fx_{2}$ is defined as $x_{1}>\mkern-13.5mu<_{L}x_{2}$. Note that the symmetric of the inclusion $\textit{i}:f[L]\rightarrow M$ is given by $i^{\dagger}(y)=ff^{\dagger}(y)$ because

$ifx>\mkern-13.5mu<_{M}y\Leftrightarrow fx>\mkern-13.5mu<_{M}y\Leftrightarrow x>\mkern-13.5mu<_{L}f^{\dagger}y\Leftrightarrow fx>\mkern-13.5mu<_{f[L]}ff^{\dagger}y$.

Clearly if $m$ is monic, then $m[L]$ is isomorphic to $L$.

Proposition \thethm.

Let $M$ be an o-algebra and let $N\subseteq M$. Then the following are equivalent:

1. (1)

$N$* = $m[L]$ for some mono $m:L\to M$ in OFrm;* 2. (2)

$N$* is closed under all joins and meets, and the Heyting implication.*

Proof.

$(1\Rightarrow 2)$: easy, since an open frame homomorphism $m$ preserve all joins and meets, and the implication.

$(2\Rightarrow 1)$: by assumption, the inclusion map $\textit{i}:N\rightarrow M$ is an open frame homomorphism, and $\exists_{i}\circ i$ = $id_{N}$ because $i$ is injective. We claim that $N$ is an o-algebra, with respect to (the restriction of) the positivity predicate of $M$. The only thing that needs to be checked is (11). Given $x,y\in N$, assume $\mathrm{Pos}(z\wedge x)\Rightarrow\mathrm{Pos}(z\wedge y)$ for all $z\in N$; we must show that $x\leq y$. By (11) in $M$, it is enough to check that $\mathrm{Pos}(t\wedge x)\Rightarrow\mathrm{Pos}(t\wedge y)$ for all $t\in L$. If $\mathrm{Pos}(t\wedge x)$, then also $\mathrm{Pos}(\exists_{i}t\wedge x)$ because $\exists_{i}\vdash i$ and $t\leq i\exists_{i}t$. By assumption we get $\mathrm{Pos}(\exists_{i}t\wedge y)$, and hence $\mathrm{Pos}(\exists_{i}(t\wedge y))$ by Frobenius reciprocity. Since $\exists_{i}:M\to N$ is a join preserving function between overt frames (see footnote 7 on page 7), we obtain $\mathrm{Pos}(t\wedge y)$. ∎

From a classical point of view, of course, $N$ is a subobject of $M$ if and only if $N$ is a sub-cBa of $M$.

Proposition \thethm.

The category OFrm is complete.

Proof.

The construction of products and equalizers is straightforward. Indeed, if $\{L_{i}\}_{i\in I}$ is a family of o-algebra, then the product $\Pi_{i\in I}L_{i}$ in OA works as a product in OFrm as well (projections $\pi_{i}$’s preserve finite meets). And if $f,g:L\to M$ are two parallel arrows in OFrm, then $E=\{x\in L\ |\ fx=gx\}$, together with the inclusion $e:E\to L$, is the equalizer of $f$ and $g$. ∎

In general $\mathbf{OFrm}$ does not have co-products, even classically, because $\mathbf{cBa}$ does not have co-products, in general, as it is well-known. Indeed, this is a consequence of the Gaifman-Hales-Solovay Theorem [11] that there is no free complete boolean algebra on countably many generators.

5.2. Sublocales of overlap algebras

Let $\mathbf{Loc}$ = $\mathbf{Frm}^{op}$ be the category of locales (see [5] and [9] for a comprehensive treatment of locale theory). A sublocale of $L$ is a regular subobjects in Loc, that is, a quotient of $L$ in $\mathbf{Frm}$. It is well known that sublocales of $L$ have, up to isomorphism, the form $L_{j}$ = ${\{jx\ |\ x\in L\}}$ where $j$ is a nucleus, that is, a function $j:L\rightarrow L$ such that

1. (1)

$x\leq j(x)=j(j(x))$ for all $x\in L$, and 2. (2)

$j(x\wedge y)=j(x)\wedge j(y)$ for all $x,y\in L$.

By definition, an open sublocale is given by a nucleus of the form $j(x)=a\to x$, for $a\in L$, where $\to$ is the Heyting implication in $L$. It is well known [7] that a sublocale $m:L_{j}\to L$ is open if and only if the corresponding frame epimorphism $m^{*}:L\to L_{j}$, with $m^{*}(x)=j(x)$, is open. Moreover, $\exists_{m^{*}}(jx)=a\wedge x$ and $a=\exists_{m^{*}}(1)$.

A sublocale $L_{j}$ is Boolean, that is, it is a complete Boolean algebra if and only if $j$ is of the form $j(x)=(x\to a)\to a$ for some $a\in L$. If $L$ itself is Boolean, then every sublocale $L_{j}$ of $L$ is Boolean, because $j(x)=(x\to j(0))\to j(0)$ holds identically in that case. What happens if we replace complete Boolean algebras with overlap algebras?

Proposition \thethm.

Every open sublocale of an overlap algebra is an overlap algebra.

Proof.

Given $m:L_{j}\rightarrow L$ with $L$ an o-algebra and $m$ open, we claim that $L_{j}$ is an o-algebra with respect to the positivity predicate $\mathrm{Pos}_{L_{j}}=\mathrm{Pos}_{L}\circ\exists_{m^{*}}$.

[TABLE]

In order to prove that $L_{j}$ is an o-algebra we must check that (11) holds for $L_{j}$, namely

$\forall z.\left[\mathrm{Pos}_{L_{j}}(jz\wedge jx)\Rightarrow\mathrm{Pos}_{L_{j}}(jz\wedge jy)\right]\Longrightarrow jx\leq jy\ .$

Now $\mathrm{Pos}_{L_{j}}(jz\wedge jx)$ can be rewritten as $\mathrm{Pos}_{L}\exists_{m^{*}}(m^{*}z\wedge jx)$, and hence as $\mathrm{Pos}_{L}(z\wedge\exists_{m^{*}}jx)$; similarly for $y$ in place of $x$. So the antecedent becomes $\forall z.[(z>\mkern-13.5mu<\exists_{m^{*}}jx)\Rightarrow(z>\mkern-13.5mu<\exists_{m^{*}}jy)]$, that is, $\exists_{m^{*}}jx\leq\exists_{m^{*}}jy$. This is equivalent to $jx\leq m^{*}\exists_{m^{*}}jy$ = $m^{*}\exists_{m^{*}}m^{*}y$ = $m^{*}y$ = $jy$. ∎

Discrete locales, that is, powersets regarded as locales, are overlap algebras (and they are Boolean if and only if LEM holds). More generally, we have the following.

Lemma \thethm.

Every overt sublocale of a discrete locale is open (as a sublocale).

Proof.

Let $j$ be a nucleus on $\mathrm{Pow}(X)$ such that the corresponding sublocale is overt with positivity predicate $\mathrm{Pos}$. Let $P$ be $\{x\in X\ |\ \mathrm{Pos}(j\{x\})\}$. We claim that $jU=P\to U$. Indeed, if $x\in jU$, then $j\{x\}=j(\{x\}\cap U)$; if also $x\in P$, then $\mathrm{Pos}(j(\{x\}\cap U))$, and hence $\{x\}\cap U$ is inhabited, that is, $x\in U$. Conversely, if $x\in P\to U$, then $\mathrm{Pos}(j\{x\})\Rightarrow(x\in U)$; so $\mathrm{Pos}(j\{x\})\Rightarrow(j\{x\}\subseteq jU)$; by overtness, $j\{x\}\subseteq jU$, that is, $x\in jU$. ∎

Corollary \thethm.

Overt sublocales of discrete locales are overlap algebras.

Proof.

By the previous proposition and lemma. ∎

Proposition \thethm.

*For $L$ a locale, there is a bijection between sublocales of $L$ which are overlap algebras and join-preserving maps $L\to\Omega$. *

Proof.

Given an o-algebra $L_{j}$, put $\varphi(x)=\mathrm{Pos}(jx)=(jx>\mkern-13.5mu<jx)$. Then $\varphi(\bigvee_{i}x_{i})$ = $\mathrm{Pos}(j(\bigvee_{i}x_{i}))$ = $\mathrm{Pos}(\bigvee^{L_{j}}_{i}jx_{i})$ = $\exists i.\mathrm{Pos}(jx_{i})$ = $\exists i.\varphi(x_{i})$.

Conversely, given $\varphi:L\to\Omega$, put $jy$ = $\bigvee\{x\in L\ |\ \forall z.[\varphi(z\wedge x)\Rightarrow\varphi(z\wedge y)]\}$. It is not difficult to check that $\varphi(x\wedge jy)$ iff $\varphi(x\wedge y)$, and that $x\leq jy$ iff $\varphi(z\wedge x)\Rightarrow\varphi(z\wedge y)$ for all $z$. Therefore $j$ is a nucleus, and $L_{j}$ is an o-algebra with $jx>\mkern-13.5mu<jy$ if $\varphi(x\wedge y)$. ∎

Some remarks on predicativity

In predicative foundations powersets are treated essentially as classes; actually, complete (semi)lattices are typically partially ordered classes rather than posets. As a consequence, the requirement (11) in the very definition of an overlap algebra appears problematic, as it may contain a universal quantification over a class.

This problem can be often overcome by restricting one’s attention to set-based overlap algebras. A base $S$ for a suplattice (complete join-semilattice) $(L,\leq)$ is a set-indexed family of generators: $p=\bigvee\{a\in S|a\leq p\}$ for every $p$ in $L$. Of course, every o-algebra is set-based impredicatively.

For a set-based o-algebra condition (11) can be replaced by the following

$(\forall a\in S)(\mathrm{Pos}(a\wedge x)\Rightarrow\mathrm{Pos}(a\wedge y))\Longrightarrow x\leq y$

where the universal quantifier ranges over a set now.

Much of the results about OA presented here remain valid for the category of set-based o-algebras within a predicative framework.