Boolean ultrafilter-power-set adjunction (source code)

= Boolean ultrafilter-power-set adjunction
{c}
{title2=$\operatorname{Ult}\dashv\mathcal P:\mathbf{Set}^{\mathrm{op}}\to\mathbf{Bool}$}

A <Boolean algebra> homomorphism $B\to\mathcal P(A)$ is equivalent to a function assigning to every $a\in A$ an <ultrafilter> on $B$: test membership of $a$ in every image subset. This gives a left adjoint valued in the <opposite category> of sets. Its unit sends an algebra element $b$ to the set of ultrafilters containing $b$. On an infinite power-set algebra this map is not surjective, because the subset consisting of the <principal ultrafilters> cannot arise this way in the presence of a <nonprincipal ultrafilter>.