Solution (source code)

= Solution

For a <Boolean algebra> $B$, write $\downarrow b$ for its principal <lattice ideal>. The <ideal frame of a Boolean algebra> has intersections as meets and ideals generated by unions as joins. The <pseudocomplement> of an ideal $I$ is
$$
I^*=\{b\in B:\ b\wedge i=0\text{ for every }i\in I\}.
$$
In particular $(\downarrow b)^*=\downarrow\neg b$, so every principal ideal is complemented and regular.

If $B$ is complete, put $s=\bigvee_B I$. Then $I^*=\downarrow\neg s$ and $I^{**}=\downarrow s$. Thus all regular ideals are principal and complemented, so the corresponding <locale> is extremally disconnected.

Conversely, if the <ideal frame of a Boolean algebra> is extremally disconnected, each $I^{**}$ is complemented. Any complemented ideal is principal: if $J\vee K=B$ and $J\cap K=\{0\}$, the fact that their generated <join> contains $1$ supplies $b\in J,c\in K$ with $b\vee c=1$. Then $b\wedge c=0$, so $c=\neg b$; every $j\in J$ is disjoint from $c$ and therefore $j\leq b$. Thus $J=\downarrow b$. Write $I^{**}=\downarrow s$. Since $I\subseteq I^{**}$, $s$ bounds $I$. If $t$ is another upper bound, $I\subseteq\downarrow t$ implies $I^{**}\subseteq(\downarrow t)^{**}=\downarrow t$, so $s\leq t$. An arbitrary subset has the same upper bounds as the <lattice ideal> it generates, so every subset of $B$ has a supremum. Hence
$$
\boxed{\operatorname{Idl}(B)\text{ is extremally disconnected}\iff B\text{ is complete}.}
$$

Now put $A=\mathcal O(X)$ and $B=A_{\neg\neg}$. This is a <complete Boolean algebra>, with arbitrary Boolean joins $\neg\neg\bigvee_A b_i$, so the preceding result makes $\gamma X$ extremally disconnected. We construct its map to $X$ using the permitted <Joyal extension lemma>.

The map $\sigma:\operatorname{Idl}(B)\to B$, $I\mapsto\bigvee_B I$, is a <frame homomorphism>, with <right adjoint> $b\mapsto\downarrow b$. Thus $k(I)=\downarrow\bigvee_B I$ is a <nucleus on a frame> whose fixed <frame> is $B$. It preserves finite joins: both $k(I\vee J)$ and $k(I)\vee k(J)$ equal $\downarrow(\bigvee_B I\vee_B\bigvee_B J)$, and $k(0)=0$. Consequently the <locale> with <frame> $B$ is a <flat sublocale> of $\gamma X$. It is also the <Booleanization of a locale> $X$, so it has its inclusion map to $X$.

The <Joyal extension lemma> says that a map from a <flat sublocale> to a <compact locale> that is a <regular locale> extends uniquely to the ambient <locale>. Apply it to this inclusion. Its <frame> formula gives
$$
\boxed{g^*(a)=\bigvee_{u\prec a}^{\operatorname{Idl}(B)}\downarrow(\neg\neg u),\qquad g:\gamma X\to X,}
$$
where $u\prec a$ is the <well-inside relation> $\neg u\vee a=1$. This also proves directly that the map is surjective. Indeed $u\prec a$ implies $\neg\neg u\leq a$: <meet> $\neg u\vee a=1$ with $\neg\neg u$. Every member of the ideal $g^*(a)$ is therefore at most $a$ in $A$, since a finite Boolean <join> of its generators is below $\neg\neg(u_1\vee\cdots\vee u_n)\leq a$; the last inequality follows because $u_1\vee\cdots\vee u_n\prec a$. Regularity gives
$$
a=\bigvee_{u\prec a}u=\bigvee_{u\prec a}\neg\neg u=\bigvee_A\{b\in B:b\in g^*(a)\}.
$$
Thus $a$ can be recovered from $g^*(a)$, so $g^*$ is injective. A <locale> map with injective inverse-image <frame homomorphism> is a <surjection>. We have obtained \b[an extremally disconnected $\gamma X$ and a <surjection> $\gamma X\to X$].