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.\u00a0 That is certainly an obstacle if one ever tries to prove that binary meets distribute over joins.<\/p>\n
In 2003, Mart\u00edn H. Escard\u00f3<\/span><\/span><\/a> gave an elegant description of joins of nuclei, which he claims is historically the sixth way of computing them [1]. This comes with useful induction principles, which make proving the frame distributivity law a cinch. Interestingly enough, this makes a crucial use of his slight extension of Pataraia’s version of the Bourbaki-Witt fixed point theorem we have seen in the June 2013 post<\/a>.<\/p>\n Perhaps the shortest self-contained proof of the frame property can be found in Picado and Pultr’s book [2]. Look for Theorem 3.2.1 there. They use sublocales instead of nuclei, and we start with it.<\/p>\n Recall that a sublocale of a frame \u03a9 is a subset L<\/em> of \u03a9 that is closed under arbitrary infima (taken in \u03a9), and under residuation on the left<\/em>, i.e., \u03c9 \u27f9 x<\/em> is in L<\/em> for every x<\/em> in L<\/em> and every \u03c9 in \u03a9.<\/p>\n Recall that \u27f9 is residuation: a<\/em> \u27f9 b<\/em> is the largest c<\/em> such that a<\/em> \u2227 c<\/em> \u2264 b<\/em>.\u00a0 For logically minded people, it is useful to think of \u2227 as logical and, and \u27f9 as logical implication, and \u2264 as being the relation of logical entailment\u2014but one should be careful to reason intuitionistically.<\/p>\n The lattice of sublocales is isomorphic to the opposite<\/em> of the lattice of nuclei, so our task is to show that the lattice of sublocales form a co<\/em>frame, not a frame.\u00a0 In other words, we want to show that arbitrary meets distribute over binary joins.<\/p>\n Meets of sublocales are easy.\u00a0 Every intersection of sublocales is a sublocale, so meets of sublocales are computed as intersections.\u00a0 Fine.<\/p>\n The union of two sublocales is not a sublocale in general, but there is an easy way of describing their join: L<\/em>1<\/sub> \u2228 L<\/em>2<\/sub> is the set of elements of the form u<\/em>1<\/sub> \u2227 u<\/em>2<\/sub> where u<\/em>1<\/sub> ranges over L<\/em>1<\/sub> and u<\/em>2<\/sub> ranges over L<\/em>2<\/sub>.\u00a0 (The \u2227 sign is infimum in \u03a9, while the \u2228 sign here one is supremum in the lattice of sublocales.)<\/p>\n Let us check that.\u00a0 Let L<\/em> be the set of elements of the form u<\/em>1<\/sub> \u2227 u<\/em>2<\/sub> built as above.\u00a0 Any intersection of elements of this form is again of this form, and for every \u03c9 in \u03a9, \u03c9 \u27f9 u<\/em>1<\/sub> \u2227 u<\/em>2<\/sub> is in L<\/em>, since\u00a0\u03c9 \u27f9 u<\/em>1<\/sub> \u2227 u<\/em>2<\/sub> is equal to (\u03c9 \u27f9 u<\/em>1<\/sub>) \u2227 (\u03c9 \u27f9\u00a0u<\/em>2<\/sub>).\u00a0 (Exercise!\u00a0 Using the definition of \u27f9, show that those two elements have exactly the same set of lower bounds, hence they are equal.)\u00a0 It follows that L<\/em> is a sublocale.<\/p>\n It contains both L<\/em>1<\/sub> and L<\/em>2<\/sub>: for every u<\/em>1<\/sub> in L<\/em>1<\/sub>, u<\/em>1<\/sub> = u<\/em>1<\/sub> \u2227 \u22a4 is in L<\/em> since \u22a4 is in L<\/em>2<\/sub> (as the intersection of the empty family).\u00a0 Similarly for L<\/em>2<\/sub>. It follows that L<\/em> contains L<\/em>1<\/sub> \u2228 L<\/em>2<\/sub>.\u00a0 Conversely, any sublocale that contains both L<\/em>1<\/sub> and L<\/em>2<\/sub> must contain all intersections u<\/em>1<\/sub> \u2227 u<\/em>2<\/sub> with u<\/em>1<\/sub> in L<\/em>1<\/sub> and u<\/em>2<\/sub> in L<\/em>2<\/sub>. So it must contain L<\/em>, and we are done.<\/p>\n A similar formula applies that yields the supremum of an arbitrary family of sublocales, but we don’t care here.<\/p>\n We now wish to show that for all sublocales L<\/em>, and Li<\/sub><\/em>, i<\/em> in I<\/em>, L<\/em>\u00a0\u2228 \u2229i \u2208 I<\/sub><\/em> Li<\/sub><\/em> = \u2229i \u2208 I<\/sub><\/em> (L<\/em> \u2228 Li<\/sub><\/em>).\u00a0 By monotonicity arguments, the left-hand side is included in the right-hand side.\u00a0 The difficult inclusion is from right to left.\u00a0 Let x<\/em> be an element of the right-hand side.\u00a0 For every i<\/em> in I<\/em>, we can write x<\/em> as a meet ui<\/sub><\/em> \u2227 vi<\/sub><\/em> of an element ui<\/sub><\/em> of L<\/em> with an element vi<\/sub><\/em> of\u00a0Li<\/sub><\/em>.<\/p>\n We would like to exhibit x<\/em> as the meet of a single<\/em> element of L<\/em> with an element that is in every Li<\/sub><\/em>.\u00a0 That seems hard to achieve, since there is no reason to believe that the elements ui<\/sub><\/em> are all equal, or that the elements vi<\/sub><\/em> are all equal.<\/p>\n But that can be repaired.\u00a0 Let u<\/em> be the infimum of the elements ui<\/sub><\/em>, i<\/em> in I<\/em>.\u00a0 Certainly, x<\/em> = infi \u2208 I<\/sub><\/em> (ui<\/sub><\/em> \u2227 vi<\/sub><\/em>) = infi \u2208 I<\/sub><\/em> ui<\/sub><\/em> \u2227 infi \u2208 I<\/sub><\/em>\u00a0vi<\/sub><\/em> = u<\/em> \u2227 infi \u2208 I<\/sub><\/em>\u00a0vi<\/sub><\/em>.\u00a0 For each i<\/em>, the latter is less than or equal to u <\/em>\u2227 vi<\/sub><\/em>, which is itself less than or equal to ui<\/sub><\/em> \u2227 vi<\/sub><\/em> = x<\/em>.\u00a0 This circular list of inequalities shows that x<\/em> is in fact equal to u<\/em> \u2227 vi<\/sub><\/em>.\u00a0 That solves one of our problems: we can replace the possibly distinct values ui<\/sub><\/em> by the same value u<\/em>.\u00a0 Since it is obtained as an infimum of elements of L<\/em>, u<\/em> is itself in L<\/em>.<\/p>\n We still have our second problem: the values vi<\/sub><\/em> may all be different, and we would like to replace them by a common value v<\/em>, which additionally should be in \u2229i \u2208 I<\/sub><\/em> Li<\/sub><\/em>.\u00a0 Here comes the trick, which is apparently due to Dana S. Scott (according to P. Johnstone, cited by Picado and Pultr).<\/p>\n We have seen that x<\/em> = u<\/em> \u2227 vi<\/sub><\/em> for every i<\/em> in I<\/em>.\u00a0 We claim that this entails that the values\u00a0u<\/em> \u27f9 vi<\/sub><\/em> are all equal.\u00a0 We shall then take v<\/em> to be this common value.\u00a0 (If I<\/em> is non-empty.\u00a0 Otherwise, we can take any v<\/em> we wish.)<\/p>\n Let us check this.\u00a0 Take two indices i<\/em>, j<\/em> in I<\/em>.\u00a0 We know that u<\/em> \u2227 vi<\/sub><\/em> = u<\/em> \u2227 vj<\/sub><\/em>. We check easily that, in a frame, a<\/em> \u2227 (a<\/em> \u27f9 b<\/em>) = a<\/em> \u2227 b<\/em>.\u00a0 So u<\/em> \u2227 (u<\/em> \u27f9 vi<\/sub><\/em>) = u<\/em> \u2227 vi <\/sub><\/em>= u<\/em> \u2227 vj<\/sub><\/em> = u<\/em> \u2227 (u<\/em> \u27f9 vj<\/sub><\/em>).\u00a0 In particular, u<\/em> \u2227 (u<\/em> \u27f9 vi<\/sub><\/em>) \u2264 (u<\/em> \u27f9 vj<\/sub><\/em>), so (u<\/em> \u27f9 vi<\/sub><\/em>) \u2264 u \u27f9 <\/em>(u<\/em> \u27f9 vj<\/sub><\/em><\/em>) = <\/em>(u<\/em> \u27f9 vThe Picado-Pultr proof<\/h2>\n