---
tag: CD9Y7YP4EJ
kind: statement
role: theorem
name: Esakia duality
msc: ["06D20", "06D50", "03G10"]
uses: [NG943XNQWH, 996BWM6ZQ7, SA22SEC75K, K7A04ZBD92]
about: [NG943XNQWH, 996BWM6ZQ7]
sources:
  - url: https://en.wikipedia.org/wiki/Esakia_duality
same_as:
  wikidata: Q5396694
  wikipedia: Esakia duality
---

## Statement

Let $f \colon X \to Y$ be a continuous order-preserving map between [[Esakia spaces|996BWM6ZQ7]].
Call $f$ an *Esakia morphism* if for all $x \in X$ and $y \in Y$ with $f(x) \le y$ there is $z \in X$ with $x \le z$ and $f(z) = y$.
Let $\mathbf{HA}$ be the category of [[Heyting algebras|NG943XNQWH]] with homomorphisms that preserve $0$, $1$, $\wedge$, $\vee$ and $\to$.
Let $\mathbf{Esa}$ be the category of Esakia spaces with Esakia morphisms.
Then $\mathbf{HA}$ is dually equivalent to $\mathbf{Esa}$, that is, $\mathbf{HA}$ is [[equivalent|K7A04ZBD92]] to the opposite category of $\mathbf{Esa}$.

1. A Heyting algebra $H$ goes to the set $X_H$ of prime filters of $H$, ordered by inclusion.
Its topology is generated by the sets $\set{P : a \in P}$ and $\set{P : a \notin P}$ for $a \in H$.
2. An Esakia space $X$ goes to the Heyting algebra of its clopen up-sets, with $U \to V = X \setminus {\downarrow}(U \setminus V)$.
3. The map $a \mapsto \set{P \in X_H : a \in P}$ is an isomorphism from $H$ onto the clopen up-sets of $X_H$.

## Remarks

The theorem refines [[Priestley duality|SA22SEC75K]] between bounded distributive lattices and Priestley spaces.
A Heyting algebra is in particular a bounded distributive lattice, and the extra structure of the implication matches exactly the condition that ${\downarrow} C$ is clopen for clopen $C$.
A lattice homomorphism between Heyting algebras preserves $\to$ exactly when its dual map satisfies the lifting condition above.
For a finite Heyting algebra the topology is discrete, and the theorem says that finite Heyting algebras are the algebras of up-sets of finite posets.

## Explanations

### L1 human

Every Heyting algebra can be rebuilt from a space of points with an order and a topology.
Algebra questions about Heyting algebras then turn into geometric questions about these spaces, and back.
Since Heyting algebras model intuitionistic logic, the theorem links the algebraic and the relational pictures of that logic.

### L2 human

The points of the dual space are the prime filters, which play the role of possible worlds in [[Kripke semantics|NGHWZ9Y7ZV]].
The duality turns subalgebras into images of Esakia morphisms and homomorphic images into closed up-sets, which makes it a working tool in the study of intermediate logics.
It is one member of the family of Stone-type dualities, next to [[Stone duality|B9T33D5MJK]] for Boolean algebras and [[Priestley duality|SA22SEC75K]] for distributive lattices.