I have already asked a similar question at


<https://math.stackexchange.com/questions/470704/can-a-brouwerian-lattice-be-extended-into-a-boolean-algebra>


but have received no answer.
Sorry, I ask a similar question second time, as it is very important for my research.


Is it true that every Brouwerian lattice (=locale =frame) can be order-embedded into a Boolean lattice?


If yes, can we warrant that this embedding preserves joins and finite meets?



Embedding a Brouwerian lattice into a Boolean lattice
$\def\pw{\mathcal P}$The answer to all the questions is yes. Here are some relevant embedding results:


**Proposition 1:** Every partial order $(P,\le)$ can be embedded in the powerset lattice $(\pw(P),\subseteq)$, i.e., an atomic complete Boolean algebra. The embedding can be made to preserve all existing meets, or all existing joins (but not both at the same time).


*Proof:* Map $a\in P$ to $\{b\in P:b\le a\}$ or to $\{b\in P:a\nleq b\}$.


**Proposition 2 ([Dedekind–MacNeille completion](https://en.wikipedia.org/wiki/Dedekind%E2%80%93MacNeille_completion)):** Every partial order $(P,\le)$ can be embedded in a complete lattice $(L,\le)$ in such way that all existing joins and meets are preserved, and $P$ is dense in $L$ in the sense that every element of $L$ is the join of a subset of $P$, and the meet of a subset of $P$. If $P$ is a Heyting or Boolean algebra, then so is $L$, and the embedding preserves (relative) complements.


**[Proposition 3](https://en.wikipedia.org/wiki/Duality_theory_for_distributive_lattices):** Every distributive lattice $(L,\le)$ can be embedded in a powerset algebra so that all existing finite joins and meets are preserved.


*Proof:* Let $X$ be the set of prime filters on $L$, and define $f\colon L\to\pw(X)$ as $f(a)=\{f\in X:a\in F\}$. Here, a filter is an upward closed subset of $L$ which is closed under all existing finite meets, and it is prime if its complement is closed under all existing finite joins. Note that the join of the empty set is the smallest element of the lattice, if it exists, and dually for empty meets.


**Proposition 4:** For every Heyting algebra $(H,\le)$, there is an embedding of $H$ into a complete Boolean algebra (not necessarily atomic) that preserves finite meets and all existing joins (but not necessarily relative complements).


*Proof:* By Proposition 3, we may assume that $H$ is a bounded sublattice of some $\pw(X)$. Let $B$ be the Boolean subalgebra of $\pw(X)$ generated by the elements of $H$, and $\tilde B$ be the Dedekind–MacNeille completion of $B$. It suffices to show that the inclusion $H\subseteq B$ preserves all existing joins.


The key point is that for every $x\in B$, there exists $\hat x\in H$ such that
$$\tag{$\*$} a\le x\iff a\le\hat x$$
for every $a\in H$. This can be shown as follows: by expressing $x$ in the conjunctive normal form, and using the closure of $H$ under finite joins and meets, we can write $x=\bigwedge\_{i<n}(-b\_i\lor c\_i)$ for some $n\in\omega$, $b\_i,c\_i\in H$. Then
$$\begin{align\*}
a\le x&\iff\forall i<n\:a\le-b\_i\lor c\_i\\
&\iff\forall i<n\:a\land b\_i\le c\_i\\
&\iff\forall i<n\:a\le(b\_i\to\_Hc\_i)\\
&\iff a\le\bigwedge\_{i<n}(b\_i\to\_Hc\_i)=:\hat x.
\end{align\*}$$
Now assume that $b\in H$ is the join of $A\subseteq H$. For any $x\in B$, we have
$$\begin{align\*}
b\le x&\iff b\le\hat x\\
&\iff\forall a\in A\:a\le\hat x\\
&\iff\forall a\in A\:a\le x,
\end{align\*}$$
hence $b$ is the join of $A$ in $B$ as well.


I should note that $B$ is sometimes called the wrapping algebra of $H$ in modal logic literature. It is not just a Boolean algebra, it also carries the structure of an S4Grz-modal algebra, which allows to recover $H$ back from $B$.


