Ideal frame of a Boolean algebra (source code)

= Ideal frame of a Boolean algebra
{title2=$\operatorname{Idl}(B)$}

The <lattice ideals> of a <Boolean algebra> form a <frame> under inclusion. Meets are intersections and joins are ideals generated by unions. A complemented ideal is principal: if $I\vee J=B$ and $I\cap J=\{0\}$, choose $b\in I,c\in J$ with $b\vee c=1$; then $c=\neg b$ and $I=\mathord\downarrow b$. This ideal frame defines an <extremally disconnected locale> exactly when $B$ is complete.