Given a preorder $(X, \preccurlyeq)$ one can define a Heyting algebra $(P_{\preccurlyeq}(X), \cap, \cup, \rightarrow, X, \emptyset)$, where $P_{\preccurlyeq}(X) = \{ A \subseteq X \mid \forall x, y: x \in A \text{ and } x \preccurlyeq y \text{ implies } y \in A \}$ and $A \rightarrow B = \{ c \mid \forall d \succcurlyeq c: d \in A \text{ implies } d \in B \}$. In fact, all Heyting algebras occur as a subalgebra of such a set-based algebra by a Stone-type representation theorem, and it can be seen that this is how the Kripke semantics of intuitionistic logic works.
I'm interested in the structure of prime filters on these preorder-generated Heyting algebras. In particular, an answer to the following question: given $x \in X$, if $F$ is the prime filter $\{ A \in P_{\preccurlyeq}(X) \mid x \in A \}$ and $F \subseteq G$, what can we say about $G$?
- Is $G$ itself principal? Ie. does there exist $y \in X$ such that $G = \{ A \in P_{\preccurlyeq}(X) \mid y \in A \}$?
- If so, do we obtain $x \preccurlyeq y$?
- If not, is there a concrete counterexample?
This seems like it should be straightforward to me but I'm struggling to give an answer one way or another. It's obviously true in the finite case (as all prime filters are principal then) but I'm struggling to think of a proof or an infinite counterexample. My feeling is the presence of $\uparrow x \in F \subseteq G$ should allow me to find an appropriate $y$ or a contradiction but I've been unable to make much headway. Any insights would be appreciated!
(the context here, for people more interested, is understanding how much of Esakia's duality for Heyting algebras is contained in just the presentation of the semantics of intuitionistic logic. That is, can we give a dual adjunction that restricts to a dual equivalence when topology is considered, just like in the case for Boolean algebras? The existence of such a $y$ is the requirement for the components of one of the natural transformations to be a p-morphism.)
Let $X = \left\{-\frac{1}{n}:n\geq 1\right\}$ with the usual order.
This is a poset, so it's a pre-ordered set as well.
Its lattice of upsets, which is the construction you use to generate the (lattice) Heyting Algebra, is, up to isomorphism, $\{0\}\cup\left\{\frac{1}{n}:n\geq 1\right\}$ (where $0$ corresponds to $\varnothing$, which is an upset too).
In this lattice (and Heyting Algebra), every proper filter is prime and all but one is principal, where the non-principal filter is $G=\left\{\frac{1}{n}:n\geq 1\right\}$.
Since for every element $a \in X$, the principal filter generated by the upset generated by $a$ is prime and is contained in $G$ which is not principal, your conjecture doesn't hold.