---
tags: logic, category theory, stone duality
---
# A Short Introduction to Stone Duality (Intro)
[up](https://hackmd.io/@alexhkurz/S1W8SC0Tc)
## Introduction and a first duality theorem
(draft)
### What is Logic?
We take the view that logic deals with "propositions", that is, things that can be `true` or `false`. [^modeltheory]
[^modeltheory]: Logic is sometimes divided into model theory and proof theory. Proof theory studies mathematical proofs and views a proposition as true if it has a proof. Model theory studies mathematical models that assign to each proposition a truth value (typically `true` or `false`). A proposition is *valid* if it evaluates to `true` in all models. These notes are written from the model-theoretic rather than the proof-theoretic point of view. Venn diagrams are pictures of mathematical models for what is known as "classical propositional logic".
Take Venn diagrams: Given a "domain" $X$ of objects $x$ a proposition is a subset of $X$. In a Venn diagram one identifies a proposition with the subset of objects for which the proposition is `true`. (Think eg of $X$ as the set of all animals and "cat" as a proposition that is true of some animals and not of others.)
More precisely, given a fixed set $X$ (domain, universe), we take a proposition to be a subset $a\subseteq X$. From given propositions one can build new propositions as follows. If $a,b$ are propositions then
- $a\cap b$ is the intersection and read as "$a$ and $b$"
- $a\cup b$ is the union and read as "$a$ or $b$"
- $\neg a$ is the complement $X\setminus a$ and read as "not $a$"
(I should proably insert some [pictures of Venn diagrams](https://en.wikipedia.org/wiki/Venn_diagram#Overview) here.)
This definition of what a proposition is blurs the distinction of a proposition as a linguistic construct (the letter $a$) and its meaning ($a$ as a subset of $X$). Typically, logicians are more careful than this, but for these notes this sloppiness should not lead to major confusions (I hope). In fact, it can be quite convenient. For example, to express that $x$ satsifies the proposition $a$ (sometimes written as $x\Vdash a$) we can simply write $$x\in a,$$
because, under our identification of propositions and sets, $x$ satisifes the proposition $a$ iff[^iff] $x$ is an element of the set $a$.
(For example: When I say that "Leon is a cat" I equally say that "Leon is an element of the set of cats".)
[^iff]: if and only if
I said that these notes will be written in the spirit of category theory (but no category theory is needed to do the exercises). We can see this right from the start. Instead of starting to build a theory of propositional logic for a fixed set $X$, we rather consider how propositions transform under functions $f:X\to Y$. This may seem as a major detour, or even complication. But it is the modern view in many areas of mathematics: Instead of focussing on a given stucture (such as the set $X$ together with its subsets), study these structures together with their structure-preserving maps.
And this is our starting point. The first proposition/exercise below asks you to show that every function $f$ on objects induces a function $f^\ast$ on propositions that preserves the structure of $\cap,\cup,\neg$.
But before we go there, it will be useful to have a notation for the set of all propositions on a given set $X$. We write
$$2^X$$
for the set of subsets of $X$.[^2X]
## Structure preserving maps and duality
In the following, the propositions are exercises. Write out a proof for each the following propositions.
**Proposition:** Given a function $f:X\to Y$ the inverse image function $f^\ast$ preserves unions, intersections and complements. [^inverseimage]
[^inverseimage]: Given $f:X\to Y$, we define $f^\ast(b) = \{x\in X \mid f(x)\in b\}$. Thus the task is to show that $f^\ast(a\cap b) = f^\ast(a)\cap f^\ast(b)$, and similarly for $\cup$ and $\neg$. As a variation, we will also need that $f^\ast$ preserves infinite intersections and unions.
The next aim is to show that the converse also holds, that is, if a function $g:2^Y\to 2^X$ preserves unions and intersections, then it is the the inverse image of some $f:X\to Y$.
In the notation introduced below, $f$ will be the restriction of $g_\exists$ to $X$.
This requires some work and there are different ways to do this. I will guide you through the way I do this, which has been chosen with future generalizations in mind.
As an aside, adjoints (or adjunctions) play a major role in category theory and many areas of mathematics. In the next proposition/exercise, we encounter a special case for the first time.
**Proposition:** If $g:2^Y\to 2^X$ preserves unions and intersections then $g$ has a left adjoint $g_\exists:2^X\to 2^Y$ and a right-adjoint $g_\forall:2^X\to 2^Y$.[^adjoints]
[^adjoints]: By definition, $l$ is left-adjoint to $r$ (and $r$ is right-adjoint to $l$), written as $l\dashv r$, if for all $a,b$
$$l(a)\subseteq b \ \Leftrightarrow\ a \subseteq r(b) \quad (*)$$
The following statements may help with proving the propositions.
$(*)$ implies $a\subseteq r(l(a))$ and $l(r(b))\subseteq b$.
$(*)$ implies that $l$ and $r$ are monotone.
(Footnote: A function $f$ is *monotone* if $a\subseteq a' \ \Rightarrow \ f(a)\subseteq f(a')$.)
Conversely, if $a\subseteq r(l(a))$ and $l(r(b))\subseteq b$ for all $a,b$ and if $l,r$ are monotone, then $(*)$.
Given $r$, the condition $(*)$ determines $l$ uniquely and, vice versa, $(*)$ determines $r$ uniquely given $l$.
(You may take these statements for granted or as further exercises.)
**Remark:** Category theoretic generalisations of this are known as adjoint functor theorems.
Recall that given $g:2^Y\to 2^X$ preserving intersections and unions, we want to find $f:X\to Y$ so that $g$ is the inverse image $f^\ast$. We want to show that we can obtain $f$ from restricting $g_\exists$ to $X$ via $X\to 2^X\stackrel {f^\ast}\to 2^Y$. For this we need that $g_\exists$ maps singletons to singletons. [^singletons]
[^singletons]: A *singleton* is a set that contains exactly one element.
With an eye on later generalisations, we will use an abstract characterisation of singletons, not in terms of elements, but in terms of subsets.
**Definition:** $a\in 2^X$ is an **atom** if for all $S\subseteq 2^X$ we have that $a\subseteq\bigcup S$ implies that there is $a'\in S$ such that $a\subseteq a'$.
If you see this definition for the first time it will probably look strange. So let me give three reasons for setting things up like this.
- This definition follows a format that generalizes to other areas of mathematics. (For example, the definition of compactness in topology is a variation.)
- The definition is phrased in a way so that the proof of the lemma below is easy in the sense that it can be done with purely algebraic reasoning, just using the definition of adjoint and the stated preservation properties.
- The definition can be read as saying that "$\subseteq$" commutes with "there is".[^commuteswiththereis]
[^commuteswiththereis]: The definition that $a$ is an atom can be rewritten as
$$a\subseteq \{ x\in X \mid \textrm{ there is } a'\in S \textrm{ such that } x\in a'\}$$
iff
$$\textrm{there is } a'\in S \textrm{ such that } a\subseteq \{x\in X\mid x\in a'\}$$
**Proposition:** $a\in 2^X$ is an atom iff there is $x\in X$ such that $a=\{x\}$.
For the proof of the lemma, recall that $g$ has a left adjoint since $g$ preserves intersections and use the definition of atom and adjoint.
**Lemma:** Let $g:2^Y\to 2^X$ preserve intersections and unions. Then the left adjoint $g_\exists$ maps atoms to atoms.
The next proposition now is obtained from putting everything together. You may have to go back to the beginning and retrace your steps to see the whole picture.
**Proposition:** Every function $2^Y\to 2^X$ preserving intersections and unions is the inverse image map for a (unique) function $X\to Y$.
We have done now the hard work. But we can "milk our cow" and deduce some stronger results.
**Theorem:** There is a bijection between functions $2^Y\to 2^X$ preserving intersections and unions and functions $X\to Y$.
This theorem is the beginning of duality theory. It has ramifications in many areas of mathematics.
To understand this better, we need to describe the collections $2^X$ of subsets using abstract algebra ... (to be continued)
[^2X]: (I apologise for the length of this explanation, but this notation is ubiquitous in math and quite slick once one got used to it.)
- It is common to identify the two element set $\{0,1\}$ with the number $2$. So when we write $2^X$, the $2$ refers to the set $\{0,1\}$.
- It is common to identify `true` with $1$ and `false` with $0$. So, in fact, $2$ refers to the set of truth values.
- It is common to write $Y^X$ for the set of functions $X\to Y$. So, in fact, $2^X$ refers to the set of functions $X\to 2$.
- It is common to identify a subset $a\subseteq X$ with its *characteristic function* $X\to 2$
$$x \mapsto \left\{
\begin{array}{l}
1 \quad \textrm{ if $x\in a$} \\
0 \quad \textrm{ if $x\notin a$}
\end{array} \right.$$
To summarize, we write $2^X$ for the collection of subsets of $X$, which, equivalently, is the set of functions $X\to 2$.
*The last bullet point, under which we identify a proposition with a subset with a function into truth-values is very important, both from a conceptual point of view and from a technical point of view. So if you are not sure about this, maybe try to prove the propositions/exercises below and then come back to contemplate this point.*