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.

In 2003, Martín H. Escardó 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.

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.

The Picado-Pultr proof

Recall that a sublocale of a frame Ω is a subset L of Ω that is closed under arbitrary infima (taken in Ω), and under residuation on the left, i.e., ω ⟹ x is in L for every x in L and every ω in Ω.

Recall that ⟹ is residuation: ab is the largest c such that acb.  For logically minded people, it is useful to think of ∧ as logical and, and ⟹ as logical implication, and ≤ as being the relation of logical entailment—but one should be careful to reason intuitionistically.

The lattice of sublocales is isomorphic to the opposite of the lattice of nuclei, so our task is to show that the lattice of sublocales form a coframe, not a frame.  In other words, we want to show that arbitrary meets distribute over binary joins.

Meets of sublocales are easy.  Every intersection of sublocales is a sublocale, so meets of sublocales are computed as intersections.  Fine.

The union of two sublocales is not a sublocale in general, but there is an easy way of describing their join: L1L2 is the set of elements of the form u1u2 where u1 ranges over L1 and u2 ranges over L2.  (The ∧ sign is infimum in Ω, while the ∨ sign here one is supremum in the lattice of sublocales.)

Let us check that.  Let L be the set of elements of the form u1u2 built as above.  Any intersection of elements of this form is again of this form, and for every ω in Ω, ω ⟹ u1u2 is in L, since ω ⟹ u1u2 is equal to (ω ⟹ u1) ∧ (ω ⟹ u2).  (Exercise!  Using the definition of ⟹, show that those two elements have exactly the same set of lower bounds, hence they are equal.)  It follows that L is a sublocale.

It contains both L1 and L2: for every u1 in L1, u1 = u1 ∧ ⊤ is in L since ⊤ is in L2 (as the intersection of the empty family).  Similarly for L2. It follows that L contains L1L2.  Conversely, any sublocale that contains both L1 and L2 must contain all intersections u1u2 with u1 in L1 and u2 in L2. So it must contain L, and we are done.

A similar formula applies that yields the supremum of an arbitrary family of sublocales, but we don’t care here.

We now wish to show that for all sublocales L, and Li, i in I, L ∨ ∩i ∈ I Li = ∩i ∈ I (LLi).  By monotonicity arguments, the left-hand side is included in the right-hand side.  The difficult inclusion is from right to left.  Let x be an element of the right-hand side.  For every i in I, we can write x as a meet uivi of an element ui of L with an element vi of Li.

We would like to exhibit x as the meet of a single element of L with an element that is in every Li.  That seems hard to achieve, since there is no reason to believe that the elements ui are all equal, or that the elements vi are all equal.

But that can be repaired.  Let u be the infimum of the elements ui, i in I.  Certainly, x = infi ∈ I (uivi) = infi ∈ I ui ∧ infi ∈ I vi = u ∧ infi ∈ I vi.  For each i, the latter is less than or equal to u vi, which is itself less than or equal to uivi = x.  This circular list of inequalities shows that x is in fact equal to uvi.  That solves one of our problems: we can replace the possibly distinct values ui by the same value u.  Since it is obtained as an infimum of elements of L, u is itself in L.

We still have our second problem: the values vi may all be different, and we would like to replace them by a common value v, which additionally should be in ∩i ∈ I Li.  Here comes the trick, which is apparently due to Dana S. Scott (according to P. Johnstone, cited by Picado and Pultr).

We have seen that x = uvi for every i in I.  We claim that this entails that the values uvi are all equal.  We shall then take v to be this common value.  (If I is non-empty.  Otherwise, we can take any v we wish.)

Let us check this.  Take two indices i, j in I.  We know that uvi = uvj. We check easily that, in a frame, a ∧ (ab) = ab.  So u ∧ (uvi) = uvi = uvj = u ∧ (uvj).  In particular, u ∧ (uvi) ≤ (uvj), so (uvi) ≤ u ⟹ (uvj) = (uvj).  (We use the definition of residuation, then the fact that, in a frame, a ⟹ (ab) = (ab).)  The other inequality (uvj) ≤ (uvi) is proved similarly.

Since x = uvi, it follows that x = u ∧ (uvi) = uv.  Moreover, v = (u ⟹ vi) is in Li for every i, because Li is closed under residuation on the left.  So v is in ∩i ∈ I Li.  Since u is in L, we have exhibited x as an element of L ∨ ∩i ∈ I Li, which terminates the proof.

Escardó’s proof

Martín Escardó’s proof works very differently [1].  We look at nuclei instead of sublocales.  Meets are take pointwise: ν1 ∧ ν2 maps every u to the inf of ν1(u) and ν2(u).  But joins are harder to describe.

So we first move to prenuclei.  A prenucleus is just like a nucleus, except it may fail to be idempotent.  In other words, a prenucleus is a monotonic map p : Ω → Ω such that p(u) ≥ u for every u in Ω (p is inflationary), and such that p(uv) = p(u) ∧ p(v) for all u, v in Ω.  We do not require idempotence, i.e., we do not require p(p(u)) = p(u).

The nice thing about prenuclei is that, not only pointwise infima of prenuclei are prenuclei, but also pointwise suprema.  In particular, prenuclei form a frame.

Now imagine you would like to find the smallest nucleus above a given prenucleus p.  We observe that, for a nucleus ν, p≤ν if and only if p o ν = ν.

Indeed, if p≤ν then for every u in Ω, (p o ν) (u) ≤ ν (ν (u)) = ν (u) since ν is idempotent, and ν (u) ≤ (p o ν) (u) since p is inflationary.  So p o ν = ν.  Conversely, if p o ν = ν, then since ν is inflationary and p is monotonic, p p o ν = ν.

Given a family of nuclei νi, i in I, (or, for that matter, of prenuclei), the least nucleus ν above all of them is therefore the least common fixed point of the functionals pp o νi.  Note that those functionals are themselves monotonic and inflationary, so the Escardó-Pataraia fixed point theorem tells you that this least common fixed point exists.  We knew that already.  What is important is that we have an induction principle: this is the final “Trick” mentioned in the post on Bourbaki-Witt and Dito Pataraia.

Here, this induction principle takes the following form (we take x0 to be the least prenucleus, namely the identity map):

(Join induction.)  To show that a given property P of prenuclei holds of the nucleus supremum ∨i ∈ I νi, we much check that:

— (Base case.) P holds of the identity map (the least nucleus).

— (Induction case.) P(p) implies P(p o νi) for every i in I and every prenucleus p, and

— (Pointwise suprema.) For every directed family D of prenuclei that satisfy P, their pointwise supremum  sup D (i.e., their supremum in the frame of prenuclei) satisfies P.

Now consider the property P defined by: P(p) if and only if ν  p ≤ ν’, where ν‘ is the join of nuclei ∨i ∈ I (ν  νi).

  • Base case.  For p the least prenucleus, this property is obvious, because ν  p is then also the least nucleus, hence below ν’.
  • Induction case.  Assume that P(p) holds, and let us show P(p o νi).  That is, we must show that ν ∧ (p o νi) ≤ ν’.  For every u in Ω, (ν ∧ (p o νi)) (u) = ν(u) ∧ p(νi(u)) ≤ ν(νi(u)) ∧ p(νi(u)) = (ν  p) (νi(u)).  Since P(p) holds, this is less than or equal to ν’(νi(u)).  By the definition of ν’, νi ≤ ν’.  It follows that (ν ∧ (p o νi)) (u) ≤ ν’(ν’(u)) = ν’(u), and that was what we were after.
  • Pointwise suprema.  Let D be a family of prenuclei that all satisfy P, and write sup D for their pointwise supremum.  For every u in Ω, (ν ∧ sup D) (u) = ν(u) ∧ sup {p(u) | u in D} = sup {ν(u) ∧ p(u) | u in D} ≤ ν‘(u).  Note the crucial use of the frame distributivity law in Ω.

We are done: P holds of ∨i ∈ I νi, namely ν ∧ (∨i ∈ I νi)i ∈ I (ν ∧ νi).  The converse inequality is obvious.  That’s it!

Let us ponder a moment on what we have achieved.  The principle of join induction is a rigorous translation of the following idea.  To obtain ∨i ∈ I νi, we build a kind of infinite composition of all the nuclei νi, in a way that interleaves them all in a fair way.  This is easier to understand for the supremum of two nuclei ν and ν‘: to compute (νν‘) (u), compute u, then the larger element ν(u), then ν‘(ν(u)), then ν(ν‘(ν(u))), etc.  Then take the supremum of that chain (which, rigorously, should be extended in the transfinite).  Escardó’s observation is that what this process computes is exactly the common fixed point of the functionals pp o ν and pp o ν‘.  And that extends to arbitrary families of nuclei.

What about sieves?

Can we prove directly that the lattice of sieves is a coframe?  That is one of the questions I asked last time.  Every union of sieves is a sieve, so joins are unions.  However, meets are more complicated.  That problem is exactly the opposite of the problem we had with sublocales.

Since sieves and sublocales are both isomorphic to the opposite of the lattice of nuclei, they form isomorphic lattices.  Of course this gives us an easy proof that the lattice of sieves is a coframe, by reduction to the coframe of sublocales.

In search of a direct proof, we are led to an easy way of characterizing meets in the lattice of sieves.  Given a family of sieves Si, i in I, compute the corresponding sublocales Li.  Take the intersection L of the latter, then transform back L into a sieve S.

The precise correspondence is as follows, something you can check by composing the isomorphisms given in part II of this series.  Given a sieve S, its corresponding sublocale L is the set of all elements w in Ω such that every t > w is such that (t, w) is in S.   Conversely, given a sublocale L, the corresponding sieve is the set of all formal crescents (u, v) such that there is a w in L such that wv and wu.

If you do that, the formula you obtain is the following: ∧i ∈ I Si is the set of all formal crescents (u, v) such that there is a w in Ω such that:

  • wv,
  • wu,
  • for every t > w, (t, w) is in ∩i ∈ I Si.

More generally, ∧i ∈ I Si is the largest sieve contained in ∩i ∈ I Si, and the above suggests that the largest sieve contained in a set A of formal crescents (possibly upwards-closed, not containing any empty crescent) is the set of formal crescents (u, v) such that there is a w in Ω such that wv, wu, and for every t > w, (t, w) is in A.

Does that help?

Jean Goubault-Larrecq (June 16th, 2016)jgl-2011

  1. Martín H. Escardó. Joins in the frame of nuclei. Applied Categorical Structures, , Volume 11, Issue 2, pp 117-124.
  2. Jorge Picado and Aleš Pultr. Frames and locales — topology without points. Birkhäuser, 2010.