Locales, sublocales II: sieves

Last time, I promised you we would explore another way of defining sublocales.  We shall again use the naive approach that consists in imagining how we would encode subspaces of a T₀ topological space X by looking at open subsets only, and certainly not at points.

Hence imagine we know of a T₀ topological space X through its lattice Ω of opens, and consider a subset A of X.  I would like to say the most I can say about A when I only have access to the open subsets U of X, not its points.  I can say whether U intersects A, and I can say whether the complement of U intersects A.

Crescents, formal crescents

I can say something more, in fact.  Consider two open subsets U and V of X.  Their difference U — V is a so-called crescent.  (This is graphical: imagine U is the moon, and V is the shadow of the earth; then U — V is the visible part of the moon — a crescent.)  We may now test, for each crescent, whether it intersects A.  This gives us more information than just testing whether U alone, or the complement of V alone, intersects A.

I will encode A as the collection of pairs (U, V) of open sets such that U — V intersects A.

We now have to describe this formally, using a frame Ω (supposedly the lattice of open subsets of X) only.  Let me write u, v, …, for the elements of Ω, to make a parallel with real opens U, V, …, while stressing that we are now working in a general frame.

Call a pair (u, v) of elements of Ω a formal crescent.  By analogy with actual crescents, we say that (u, v) is empty if and only if u ≤ v.  Indeed, for actual crescents, U — V is empty if and only if U ⊆ V.

Again with analogy with actual crescents, we compare formal crescents by: (u, v) ⊑ (u’, v’) if and only if u ≤ v ∨ u’ and u ∧ v’ ≤ v.  (∧ is binary inf, and ∨ is binary sup.)  That may not ring a bell, but you may check that, for actual crescents, U — V ⊆ U’ — V’ if and only if U is included in V union U’ and the intersection of U and V’ is included in V.

The relation ⊑ is a preorder, but in general not an ordering.  That is, the equivalence relation ≣ defined by (u, v) ≣ (u’, v’) if and only if (u, v) ⊑ (u’, v’)  and (u’, v’) ⊑ (u, v), is not the equality relation in general.  One may quotient formal crescents by ≣ and obtain a good locale-theoretic notion of crescent, but we won’t need to do that.

Sieves

Now look at the set E of (actual) crescents U — V that intersect A.  It has the following properties:

1. All the crescents in E are non-empty.
2. E is upwards-closed: if U — V is a crescent in E, then any larger crescent is also in E.
3. E is refinement-closed: if U — V is a crescent in E, and U’ is any open subset, then the intersection of (U — V) with U’ or with the complement of U’ is in E.  (Given a point in the intersection of U — V with A, it must be in U’ or in the complement of U’.)
4. E is accessible: if U — V is a crescent in E, and if U is the union of a family U_i of opens, i in I, then U_i — V is in E for some i in I.  (A point in U must be in some U_i.)

Accordingly, call a sieve S on a frame Ω any set of formal crescents such that:

1. No empty formal crescent is in S.
2. S is upwards-closed: if (u, v) is a formal crescent in S, and if (u, v) ⊑ (u’, v’), then (u’, v’) is in S.
3. S is refinement-closed: if (u, v) is in S, then for every u’ in Ω, (u ∧ u’, v) or (u, v ∨ u’) is in S.
4. S is accessible: if (u, v) is in S and u = ⋁_{i ∈ I} u_i then (u_i, v) is in S for some i in I.

Upward closure (condition 2) in particular implies that if (u, v) is a formal crescent in S, then any formal crescent (u’, v’) that is equivalent to (u, v) in the sense that (u, v) ≣ (u’, v’) is also in S.  This is why we will never need to quotient our formal crescents: every sieve S contains all the formal crescents that intuitively denote the same crescent as one already in S.

The poset of sieves

We order sieves by inclusion.  This is natural: if A and B are two subsets of X, and if A is included in B, then all the crescents that intersect A also intersect B.  I doubt that the converse would hold (even assuming that X is T₀), since that would imply that any two subsets that intersect the same crescents are equal.

Let C(Ω) denote the poset of all sieves on the frame Ω.  It is an easy exercise to verify that any union of sieves is a sieve.  It follows that C(Ω) is a complete lattice.

So suprema are simple: they are just unions.  It is a general fact that all infima also exist: the inf of a family of sieves is the sup of its set of lower bounds.  However, this is less concrete, and hardly usable.  We had the same issue with the complete lattice of sublocales, where suprema are simply unions, but infima are more complicated.

Let me show that sieves and sublocales form isomorphic lattices.  It will be easier to go through frame congruences, and nuclei, though.

Given a subset A of a space X, imagine two opens U and V of X that have different intersections with A.  There is a point of A that is in U but not in V, or in V but not in U.  That is, U — V or V — U intersects A.  The converse direction is easy, too.  We obtain that U and V are in the frame congruence associated with A (i.e., U ⋂ A = V ⋂ A) if and only if the crescents U — V and V — U are both outside the sieve associated with A (i.e., they do not intersect A).  When U is included in V, this condition simplifies to: U is equivalent to V if and only if V — U is outside the sieve associated with A.  In particular, the largest open subset that has the same intersection as U with A is the union of all the open subsets V ⊇ U such that V — U is outside the sieve associated with A.

Accordingly, on the localic side, given a sieve S in C(Ω), let ν_S be the function that maps every u in Ω to the union of all the elements v ≥ u such that (v, u) is not in S.

Lemma. For every sieve S, ν_S is a nucleus.

Proof. We start by checking that ν_S is monotonic.  Assume u ≤ u’.  For every v ≥ u such that (v, u) is not in S, I claim that (v ∨ u’, u’) is not in S either.  Indeed, we can check that (v ∨ u’, u’) ⊑ (v, u), and this then follows from the fact that S is upwards-closed.  By taking suprema, ν_S(u) ∨ u’ ≤ ν_S(u‘).  This actually shows both monotonicity and the inequality u’ ≤ ν_S(u‘) at once.

To show that it is a closure operator, namely ν_S o ν_S = ν_S, we need to check that ν_S(u) is the largest v ≥ u such that (v, u) is not in S, i.e., that the supremum of those v‘s is attained.  This amounts to showing that (ν_S(u), u) is not in S.  If it were in S, since S is accessible and ν_S(u) is the supremum of all elements v ≥ u such that (v, u) is not in S, one of those v‘s would be such that (v, u) in S.  That would be absurd.

It remains to show that ν_S preserves binary infima.  The inequality ν_S(u ∧ v) ≤ ν_S(u) ∧ ν_S(v) follows from monotonicity.  In the converse direction, we know that ν_S(u) ≥ u, ν_S(v) ≥ v, (ν_S(u), u) is not in S, and (ν_S(v), v) is not in S.  We shall prove that (ν_S(u) ∧ ν_S(v), u ∧ v) is not in S, which will imply ν_S(u ∧ v) ≥ ν_S(u) ∧ ν_S(v).  Assume on the contrary that (ν_S(u) ∧ ν_S(v), u ∧ v) is in S.

By refinement-closure, ((ν_S(u) ∧ ν_S(v)) ∧ u, u ∧ v) or (ν_S(u) ∧ ν_S(v), (u ∧ v) ∨ u) is in S.  In other words, simplifying all expressions, (u ∧ ν_S(v), u ∧ v) or (ν_S(u) ∧ ν_S(v), u) is in S.  The second case is impossible since (ν_S(u) ∧ ν_S(v), u) ≤ (ν_S(u), u), which is not in S, because S is upwards-closed.  Hence (u ∧ ν_S(v), u ∧ v) is in S.

By refinement-closure again, ((u ∧ ν_S(v)) ∧ v, u ∧ v) or (u ∧ ν_S(v), (u ∧ v) ∨ v) is in S.  Simplifying, (u ∧ v, u ∧ v) or (u ∧ ν_S(v), v) is in S. The first case is impossible since no empty formal crescent is in S, and the second case is impossible since (u ∧ ν_S(v), v) ≤ (ν_S(v), v), which is not in S.

This concludes our argument that (ν_S(u) ∧ ν_S(v), u ∧ v) is not in S, hence also the whole proof. ☐

The mapping S ⟼ ν_S is easily seen to be antitonic.

Let us find a mapping in the converse direction.  Given a nucleus ν on Ω, let S_ν be the set of formal crescents (u, v) such that u ≰ ν(v).

Lemma.  For every nucleus ν, S_ν is a sieve.

Proof. 1. If (u, v) is an empty formal crescent, then u ≤ v ≤ ν(v), hence it is not in S_ν.

2. Upward closure.  The argument exhibits some subtletly.  Assume (u, v) is in S_ν, and (u, v) ⊑ (u’, v’).  We must show that (u’, v’) is in S_ν.  Otherwise, u’ ≤ ν(v’).  The inequality (u, v) ⊑ (u’, v’) means that u ≤ v ∨ u’ and u ∧ v’ ≤ v.  Now u  = u ∧ u ≤ u ∧ (v ∨ u’) ≤ u ∧ (v ∨ ν(v’)) = (u ∧ v) ∨ (u ∧ ν(v’)), the term u ∧ v is less than or equal to v, the term u ∧ ν(v’) is less than or equal to ν(u) ∧ ν(v’) = ν(u ∧ v’) ≤ ν(v); so u ≤ v ∨ ν(v) = ν(v).  But that contradicts the fact that (u, v) is in S_ν.

3. Refinement closure.  Assume (u, v) is in S_ν, and that for some u’ in Ω, neither (u ∧ u’, v) nor (u, v ∨ u’) is in S_ν.  In other words, u ∧ u’ ≤ ν(v) and u ≤ ν(v ∨ u’).  Again, the argument is slightly subtle.  We have u  = u ∧ u ≤ u ∧ ν(v ∨ u’) ≤ ν(u) ∧ ν(v ∨ u’) = ν(u ∧ (v ∨ u’)) = ν((u ∧ v) ∨ (u ∧ u’)) ≤ ν((u ∧ v) ∨ ν(v)) = ν(ν(v)) [since u ∧ v ≤ ν(v)] = ν(v).  But u ≤ ν(v) contradicts the assumption that (u, v) is in S_ν.

4. Accessibility.  Assume (u, v) is in S_ν, u = ⋁_{i ∈ I} u_i but no (u_i, v) is in S_ν.  In other words, u_i ≤ ν(v) for every i in I.  Clearly, this implies u ≤ ν(v), a contradiction. ☐

The mapping ν ⟼ S_ν is, too, easily seen to be antitonic.

Lemma. The mappings ν ⟼ S_ν and S ⟼ ν_S are inverse of each other.

Proof. Given a nucleus ν, let S = S_ν, and let us compute ν_S: ν_S(u) is the largest v ≥ u such that (v, u) is not in S_ν, i.e., such that v ≤ ν(u).  Clearly, this v is just ν(u), so ν_S=ν.

Conversely, given a sieve S, let ν=ν_S, and let us compute S_ν.  We show that the formal crescents that are not in S are exactly those that are not in S_ν, and this will show S= S_ν.  For every formal crescent (u, v), if (u, v) is not in S, then u would be in the family of elements w ≥ v such that (w, v) is not in S.  The largest element of that family is ν_S(v), so we would obtain u ≤ ν_S(v), hence (u, v) is not in S_ν.  Conversely, if (u, v) is not in S_ν, then u ≤ ν_S(v).  Calling w the element ν_S(v), w is the largest element above v such that (w, v) is not in S by definition, and we know that u ≤ w.  Hence (u, v) ⊑ (w, v).  Since S is upwards-closed, (u, v) is not in S. ☐

Since we know that nuclei form a frame, we immediately obtain:

Theorem. The lattice of sieves is a co-frame, isomorphic to the opposite of the frame of nuclei (hence to the co-frame of sublocales).

Open and closed sieves, crescent sieves

If A is an open subset of the T₀ topological space X, then the crescent U — V intersects A if and only if (U — V) ⋂ A = (U ⋂ A) — V is non-empty.  Note that (U ⋂ A) — V is a crescent in this case.

We can port this observation to the localic side, and define, for each element ω of the frame Ω, the open sieve o(ω) as the set of pairs (u, v) such that (u ∧ ω, v) is non-empty.   I will let you check that this is indeed a sieve.

By similar considerations, we can define the closed sieve c(ω) as the set of pairs (u, v) such that (u, v ∨ ω) is non-empty.  Thinking of ω as open, this represents the complement of ω as a sieve.  Indeed, look back at the topological side.  If A is a closed subset of X, then the crescent U — V intersects the complement of A if and only if the crescent U — (V ⋃ A) is non-empty.

Generalizing the two constructions, given a formal crescent (u₀, v₀), we can define oc (u₀, v₀) as the set of pairs (u, v) such that (u ∧ u₀, v ∨ v₀) is non-empty.  This intuitively encodes the intersects of the open set u₀ and of the complement of the open set v₀.  (That can be checked, too, see below.)

Even more generally, given (u₀, v₀) and a sieve S, define oc (S; u₀, v₀) as the set of pairs (u, v) such that (u ∧ u₀, v ∨ v₀) is in S.  We get back oc (u₀, v₀) by taking 1 for S, where 1 is the largest sieve (= the set of all non-empty formal crescents).  We also obtain o(u₀) as oc (1; u₀, ⊥) and c(v₀) as oc (1; ⊤, v₀).

As an exercise, let me suggest that you check the following (without going through nuclei or sublocales):

1. oc (S; u₀, v₀) is a sieve; in particular o(u₀) and c(v₀) are sieves, too.
2. oc (S; ⋁_{i ∈ I} u_i, v₀) = ⋃_{i ∈ I} oc (S; u_i, v₀).
3. oc (S; u₀, v₀) is monotonic in S and u₀, and antitonic in v₀.
4. oc (S; u₀, v₀) is the inf of S, o(u₀) and c(v₀) in C(Ω).  (Hint: to check that every sieve S‘ that is included in S, o(u₀) and c(v₀) is also included in oc (S; u₀, v₀), take an arbitrary formal crescent (u, v) in S’, and use refinement-closure twice to show that (u ∧ u₀, v), then (u ∧ u₀, v ∨ v₀), is in S’.)
   
5. o commutes with finite infima.
6. o commutes with arbitrary suprema.
7. inf (S, o(u₀)) ⊆ S’ if and only if S ⊆ c(u₀) ⋃ S’.  (Hint: in the ⇒ direction, let (u, v) be in S, use refinement-closure to obtain that (u ∧ u₀, v) or (u, v ∨ u₀) is in S.  In the first case, use item 4 and the assumption to conclude that (u, v) is in S’.  In the second case, observe that no element of S can be empty and conclude that (u, v) is in c(u₀).)
8. inf (S, c(u₀)) ⊆ S’ if and only if S ⊆ o(u₀) ⋃ S’.  (A very similar proof.)
9. o(u₀) and c(u₀) are complements.  (Use 7 and 8.)
10. For every sieve S, for all pairs (u₀, v₀) that are not in S, S ⊆ c(u₀) ⋃ o(v₀).  (Use 7, 8, and the fact that S is upwards-closed.)
11. Conversely, if S ⊆ c(u₀) ⋃ o(v₀) then (u₀, v₀) cannot be in S.
12. Every sieve S is the intersection (hence the infimum) of the complemented sieves c(u₀) ⋃ o(v₀), when (u₀, v₀) ranges over the pairs that are not in S.  (Use 10 and 11.)

This way, you will retrieve something that I had announced last month: every sublocale is an infimum of complemented sublocales, each obtained as binary supremum of an open and a closed sublocale.  In particular, the co-frame of sieves (or sublocales) is zero-dimensional.

Also, items 5 and 6 show that o is a frame homomorphism from Ω to C(Ω).  It is in fact a frame embedding, of Ω into C(Ω), since o(u) ⊆ o(v) is equivalent to u≤v.  (o is monotonic since it preserves finite infima for example.  Conversely, if u≰v then (u, v) is in o(u) but not in o(v).)

I am leaving one question open here.  There are several ways of showing that the lattice of nuclei is a frame, or equivalently that the lattice of sublocales is a co-frame, certain simpler than others.  Is there a simple, direct way of showing that the lattice of sieves is a co-frame?

— Jean Goubault-Larrecq(May 11th, 2016)