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 *co*frame, 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*_{1} ∨ *L*_{2} is the set of elements of the form *u*_{1} ∧ *u*_{2} where *u*_{1} ranges over *L*_{1} and *u*_{2} ranges over *L*_{2}. (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*_{1} ∧ *u*_{2} built as above. Any intersection of elements of this form is again of this form, and for every ω in Ω, ω ⟹ *u*_{1} ∧ *u*_{2} is in *L*, since ω ⟹ *u*_{1} ∧ *u*_{2} is equal to (ω ⟹ *u*_{1}) ∧ (ω ⟹ *u*_{2}). (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*_{1} and *L*_{2}: for every *u*_{1} in *L*_{1}, *u*_{1} = *u*_{1} ∧ ⊤ is in *L* since ⊤ is in *L*_{2} (as the intersection of the empty family). Similarly for *L*_{2}. It follows that *L* contains *L*_{1} ∨ *L*_{2}. Conversely, any sublocale that contains both *L*_{1} and *L*_{2} must contain all intersections *u*_{1} ∧ *u*_{2} with *u*_{1} in *L*_{1} and *u*_{2} in *L*_{2}. 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*). By monotonicity arguments, the left-hand side is included in the right-hand side. The difficult inclusion is from right to left. Let

_{i}*x*be an element of the right-hand side. For every

*i*in

*I*, we can write

*x*as a meet

*u*∧

_{i}*v*of an element

_{i}*u*of

_{i}*L*with an element

*v*of

_{i}*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*are all equal, or that the elements

_{i}*v*are all equal.

_{i}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*) = inf

_{i}

_{i ∈ I}*u*∧ inf

_{i}

_{i ∈ I}*v*=

_{i}*u*∧ inf

_{i ∈ I}*v*. For each

_{i}*i*, the latter is less than or equal to

*u*∧

*v*, which is itself less than or equal to

_{i}*u*∧

_{i}*v*=

_{i}*x*. This circular list of inequalities shows that

*x*is in fact equal to

*u*∧

*v*. That solves one of our problems: we can replace the possibly distinct values

_{i}*u*by the same value

_{i}*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*. Here comes the trick, which is apparently due to Dana S. Scott (according to P. Johnstone, cited by Picado and Pultr).

_{i}We have seen that *x* = *u* ∧ *v _{i}* for every

*i*in

*I*. We claim that this entails that the values

*u*⟹

*v*are all equal. We shall then take

_{i}*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*. We check easily that, in a frame,

_{j}*a*∧ (

*a*⟹

*b*) =

*a*∧

*b*. So

*u*∧ (

*u*⟹

*v*) =

_{i}*u*∧

*v*=

_{i }*u*∧

*v*=

_{j}*u*∧ (

*u*⟹

*v*). In particular,

_{j}*u*∧ (

*u*⟹

*v*) ≤ (

_{i}*u*⟹

*v*), so (

_{j}*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}*) is proved similarly.*

*u*⟹*v*_{i}Since *x* = *u* ∧ *v _{i}*, it follows that

*x*=

*u*∧ (

*u*⟹

*v*) =

_{i}*u*∧

*v*. Moreover,

*v =*(

*u ⟹*) is in

*v*_{i}*L*for every

_{i}*i*, because

*L*is closed under residuation on the left. So

_{i}*v*is in ∩

_{i ∈ I}*L*. Since

_{i}*u*is in

*L*, we have exhibited

*x*as an element of

*L*∨ ∩

_{i ∈ I}*L*, which terminates the proof.

_{i}## 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*(*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 ν

*. 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.*

_{i}Here, this induction principle takes the following form (we take *x*_{0} to be the least prenucleus, namely the identity map):

(Join induction.) To show that a given property

Pof prenuclei holds of the nucleus supremum ∨_{i ∈ I}ν, we much check that:_{i}— (Base case.)

Pholds of the identity map (the least nucleus).— (Induction case.)

P(p) impliesP(po ν) for every_{i}iinIand every prenucleusp, and— (Pointwise suprema.) For every directed family

Dof prenuclei that satisfyP,their pointwise supremum supD(i.e., their supremum in the frame of prenuclei) satisfiesP.

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 ν). That is, we must show that_{i}*ν*∧ ()*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})). By the definition of*u**ν’*,*ν*_{i}*≤ ν’*. It follows that (*ν*∧ ()) (*p*o ν_{i}*u*) ≤*ν’*((*ν’*)) =*u**ν’*(), and that was what we were after.*u* - 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}*∧*

*ν**). The converse inequality is obvious. That’s it!*

*ν*_{i}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

*ν*, in a way that interleaves them all in a fair way. This is easier to understand for the supremum of two nuclei

_{i}*ν*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*. Take the intersection

_{i}*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*, and the above suggests that the largest sieve contained in a set

_{i}*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)

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