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: a ⟹ b is the largest c such that a ∧ c ≤ b.  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: L₁ ∨ L₂ is the set of elements of the form u₁ ∧ u₂ where u₁ ranges over L₁ and u₂ ranges over L₂.  (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 u₁ ∧ u₂ built as above.  Any intersection of elements of this form is again of this form, and for every ω in Ω, ω ⟹ u₁ ∧ u₂ is in L, since ω ⟹ u₁ ∧ u₂ is equal to (ω ⟹ u₁) ∧ (ω ⟹ u₂).  (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 L₁ and L₂: for every u₁ in L₁, u₁ = u₁ ∧ ⊤ is in L since ⊤ is in L₂ (as the intersection of the empty family).  Similarly for L₂. It follows that L contains L₁ ∨ L₂.  Conversely, any sublocale that contains both L₁ and L₂ must contain all intersections u₁ ∧ u₂ with u₁ in L₁ and u₂ in L₂. 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 L_i, i in I, L ∨ ∩_{i ∈ I} L_i = ∩_{i ∈ I} (L ∨ L_i).  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 u_i ∧ v_i of an element u_i of L with an element v_i of L_i.

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

But that can be repaired.  Let u be the infimum of the elements u_i, i in I.  Certainly, x = inf_{i ∈ I} (u_i ∧ v_i) = inf_{i ∈ I} u_i ∧ inf_{i ∈ I} v_i = u ∧ inf_{i ∈ I} v_i.  For each i, the latter is less than or equal to u ∧ v_i, which is itself less than or equal to u_i ∧ v_i = x.  This circular list of inequalities shows that x is in fact equal to u ∧ v_i.  That solves one of our problems: we can replace the possibly distinct values u_i 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 v_i may all be different, and we would like to replace them by a common value v, which additionally should be in ∩_{i ∈ I} L_i.  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 = u ∧ v_i for every i in I.  We claim that this entails that the values u ⟹ v_i 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 u ∧ v_i = u ∧ v_j. We check easily that, in a frame, a ∧ (a ⟹ b) = a ∧ b.  So u ∧ (u ⟹ v_i) = u ∧ v_i = u ∧ v_j = u ∧ (u ⟹ v_j).  In particular, u ∧ (u ⟹ v_i) ≤ (u ⟹ v_j), so (u ⟹ v_i) ≤ u ⟹ (u ⟹ v_j) = (u ⟹ v_j).  (We use the definition of residuation, then the fact that, in a frame, a ⟹ (a ⟹ b) = (a ⟹ b).)  The other inequality (u ⟹ v_j) ≤ (u ⟹ v_i) is proved similarly.

Since x = u ∧ v_i, it follows that x = u ∧ (u ⟹ v_i) = u ∧ v.  Moreover, v = (u ⟹ v_i) is in L_i for every i, because L_i is closed under residuation on the left.  So v is in ∩_{i ∈ I} L_i.  Since u is in L, we have exhibited x as an element of L ∨ ∩_{i ∈ I} L_i, 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: ν₁ ∧ ν₂ maps every u to the inf of ν₁(u) and ν₂(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(u ∧ v) = 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 p ⟼ p 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 x₀ 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 p ⟼ p o ν and p ⟼ p 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 S_i, i in I, compute the corresponding sublocales L_i.  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 w ≥ v and w ≱ u.

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

• w ≥ v,
• w ≱ u,
• for every t > w, (t, w) is in ∩_{i ∈ I} S_i.

More generally, ∧_{i ∈ I} S_i is the largest sieve contained in ∩_{i ∈ I} S_i, 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 w ≥ v, w ≱ u, and for every t > w, (t, w) is in A.

Does that help?

— Jean Goubault-Larrecq (June 16th, 2016)

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