Extremally disconnected locale

A locale is extremally disconnected when the closure of every open is open. Equivalently its regular open elements are complemented, or double negation preserves binary joins, or its Booleanization of a locale is a flat sublocale.

For a compact regular locale $X$, put $B=\mathcal{O}(X{)}_{\neg \neg }$ and $\mathcal{O}(\gamma X)=\mathrm{Idl}(B)$. This locale is extremally disconnected. Its natural surjection to $X$ has inverse imageThe Joyal extension lemma gives the frame homomorphism; its injectivity follows by recovering $a$ as the join of the regular opens in this ideal.