Locales, sublocales III: the frame of nuclei

My goal today is to describe two elegant proofs of the fact that nuclei form a frame. There are many proofs of that.

The main difficulty is that, while meets (infima) of nuclei are taken pointwise, joins (suprema) are much harder to describe.  That is certainly an obstacle if one ever tries to prove that binary meets distribute over joins.  A similar difficulty occurs with sublocales.

I will present a short proof due to Picado and Pultr, using sublocales. I will also present an entirely different proof due to M. H. Escardó, which works on nuclei. The latter will make use of a fixed point theorem we have already seen on this site! Read the full post.