Revisiting Stone duality for bitopological spaces: II. sequent theories, 2-sublocales, and (simple) biframes

What a summer! Yuxu Chen, Hui Kou and Zhenchao Lyu cracked three open problems in domain theory: 1. the domain of discs in the plane is an FS-domain that is not an RB-domain, hence FS≠RB, something I talked about in the July 2026 post; 2. the probabilistic powerdomain of a finite poset P is an RB-domain if and only if P is a tree (see https://arxiv.org/abs/2607.02231v1), and 3. there is a Cartesian-closed category of continuous dcpos that is closed under the (sub)probabilistic powerdomain monad, finally solving an old question (see https://arxiv.org/abs/2608.03073v2). I am planning to talk about these subjects in the forthcoming months. In the meantime, I had already prepared something about Stone dualities for bitopological spaces. Let me tell you a little secret: I usually take rather long holidays from mid-July to mid-August, roughly. Since I always plan to have something ready to post on August 20th, I tend to spend some time during my holidays preparing the August post. For a few years now, this post has tended to become way too long over time (and I also tend to spend a few hours every day of my holidays preparing it); hence I eventually split it in several parts, which then become the September and October posts, typically. This is fortunate, in a sense: the final days of August, and the months of September and October are the busiest time of the year for me, and I almost always end up having no time to prepare any blog post during that period. All this to say that I have already prepared posts for the next few months, and that it is likely that I will only talk about Shen, Kou and Lyu’s amazing discoveries later this academic year.

And now for something completely different, as John Cleese would say.

Tomáš Jakl wrote to me about my proposal of 2-frames (in the June 2026 post), and asked me whether it would solve some issues that d-frames have.  Notably, it seems that it is hard in general to define a notion analogous to that of sublocales [2] in the theory of frames and locales; sublocales are the point free analogue of the notion of subspace, and are also an essential tool in define locales from generators and relations.

I will start addressing this in this post, or rather in a series of posts starting with this one: I have too much to say in one post. The first of these posts will seem to wander around and not go in any specific direction: I originally wrote this while I was discovering what the right notions should be, and I decided to keep it that way. Ordinarily, when you write a paper in mathematics, you discard every piece of your erratic journey towards the truth, and only keep the final result. But I feel the journey is interesting in its own right here, and will help understand that there is a progression from d-frames, through 2-frames (with a slight modification, which are Anna Laura Suarez’ finitary biframes [5]), until we reach a notion that I think is natural, which I will call simple biframes, are are really Banaschewski, Brümmer and Hardie’s notion of biframes [3, 4] in disguise.

Before we start, the slight modification of 2-frames I am mentioning is that the cut rules (cut+) and (cut–) should be changed to:

  • (cut+) if u+; u– ⊢ v+ ⋁ w; v– and u+ ⋀ w; u– ⊢ v+; v– then u+; u– ⊢ v+; v– and
  • (cut–) if u+; u– ⊢ v+; v– ⋁ w and u+; u– ⋀ w ⊢ v+; v– then u+; u– ⊢ v+; v–.

But we will have time to return to this.

My initial direction of research was that I should imitate the specific form of reasoning I used in introducing sieves, an equivalent presentation of locales (see the May 2016 post), in order to find the appropriate notion of 2-locales.  In the process, I discovered that the notion of sieve could be presented slightly differently, as what I will call sequent theories. (This has some connections with theories in geometric logic, too, but I will not go in this direction.)

Back to sieves

In May 2016, I defined a sieve on a frame Ω as 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 ui, then (ui, v) is in S for some i in I.

A formal crescent is simply a pair (u, v) of two elements of Ω.  It is empty if and only if u≤v.  The ordering ⊑ is defined by (u, v) ⊑ (u’, v’) if and only if u ≤ v ∨ u’ and u ∧ v’ ≤ v.  The intuition is that, if Ω is the lattice OX of open subsets of a topological space X, then a formal crescent is notation for an actual crescent u–v: then u–v is empty if and only if u is less than or equal to (included) in v, and (u, v) ⊑ (u’, v’) if and only if u–v ⊆ u’–v’. The axioms above are a list of properties satisfied by the set of (formal) crescents that intersect a given, fixed subset of a topological space. In May 2016, I showed that the notion of sieve was equivalent to the notion of a sublocale (hence also to the notion of nucleus) in locale theory.

What I will call a sequent theory is simply the complement of a sieve.  Explicitly, and slightly modifying the axioms along the way,

Definition A.  A sequent theory on a frame Ω is a binary relation ⊢ on Ω (a subset of Ω × Ω) such that:

  1. (The axiom rule (ax)) For every u ∈ Ω, u ⊢ u.
  2. (The cut rule (cut)) For all u, v, w ∈ Ω, if u ⊢ v ⋁ w and u ⋀ w ⊢ v then u ⊢ v; we will say that w is what we cut on.
  3. For every v ∈ Ω, the set _ ⊢ v ≝ {u ∈ Ω | u ⊢ v} is an ideal (a non-empty downwards-closed set, closed under directed suprema; non-emptiness is automatic, because of the axiom rule).
  4. For every u ∈ Ω, the set u ⊢ _≝ {v ∈ Ω | u ⊢ v} is upwards-closed (and non-empty, by the axiom rule).

I claim that sequent theories and sieves (hence also sublocales, nuclei, etc.) are the same thing, up to an obvious encoding. This encoding consists in taking complements.

Lemma B.  The complement of every sieve is a sequent theory.

Proof.  Let S be a sieve, and ⊢ be its complement.  In other words, we define u ⊢ v as (u, v) ∉ S.

  1. The axiom rule follows from the fact that (u, u) is an empty formal crescent, hence cannot be in S.
  2. The cut rule is a rephrasing of the fact that S is refinement-closed, up to contraposition.  Explicitly, if u ⊢ v fails, namely if (u, v) ∈ S, then by refinement closure (u ∧ w, v) or (u, v ∨ w) is in S, namely u ⋀ w ⊢ v fails or u ⊢ v ⋁ w fails.
  3. Let us fix v ∈ Ω.  For every element u of _ ⊢ v, for every u’ ≤ u, we claim that u’ is in _ ⊢ v, too.  Otherwise, (u’, v) is in S.  But (u’, v) ⊑ (u, v), so (u, v) is in S, which contradicts u ⊢ v.  We have just shown that _ ⊢ v is downwards-closed.
    Finally, let (ui)i ∈ I be a family of elements of _ ⊢ v, and let u be its supremum in Ω. We wish to show that if (ui)i∈ I is directed, then u is also in _ ⊢ v, but we will not need directedness for that.  For the purpose of contradiction, let is assume that u is not in _ ⊢ v.  Hence (u, v) is in S, and since S is accessible, some (ui, v) is in S, too.  But that would mean that ui ⊢ v, which is impossible.
  4. Let us fix u ∈ Ω.  For every element v of u ⊢ _, for every v’ ≥ v, we claim that v’ is in u ⊢ _, too.  Otherwise, (u, v’) is in S.  But (u, v’) ⊑ (u, v), so (u, v) is in S, which contradicts u ⊢ v.  We have just shown that u ⊢ _ is upwards-closed.   ☐

We will see that, conversely, the complement of a sequent theory is always a sieve.  We first need to make a few remarks on sequent theories.

Lemma C.  Given a sequent theory  ⊢ on a frame Ω, the following hold:

  1. ≤ is included in ⊢, namely: for all u, v ∈ Ω, if u ≤ v then u ⊢ v.
  2. For all u, v, w ∈ Ω, if u ⊢ v then u ⋀ w ⊢ v ⋀ w.
  3. For all u, v, w ∈ Ω, if u ⊢ v then u ⋁ w ⊢ v ⋁ w.
  4. For all u, v, w ∈ Ω, u ⊢ v ⋀ w if and only if u ⊢ v and u ⊢ w.
  5. For all u, v, w ∈ Ω, u ⋁ v ⊢ w if and only if u ⊢ w and v ⊢ w.

Proof.  1. By (ax), v ⊢ v, then u ⊢ v since _ ⊢ v is downwards-closed.

2. From u ⊢ v and u ⋀ w ≤ u, we obtain that u ⋀ w ⊢ v.  We rewrite the v on the right as (v ⋀ w) ⋁ v, so (u ⋀ w) ⊢ (v ⋀ w) ⋁ v.  We also have (u ⋀ w) ⋀ v ⊢ (v ⋀ w) because (u ⋀ w) ⋀ v = u ⋀ (v ⋀ w) ≤ (v ⋀ w), and using item 1.  Applying (cut) to (u ⋀ w) ⊢ (v ⋀ w) ⋁ v and to (u ⋀ w) ⋀ v ⊢ (v ⋀ w), and cutting on v, we obtain u ⋀ w ⊢ v ⋀ w.

3. We proceed similarly.  We cut between (u ⋁ w)⊢ (v ⋁ w) ⋁ u and (u ⋁ w) ⋀ u ⊢ (v ⋁ w) on u.  The first statement (u⋁ w)⊢ (v ⋁ w) ⋁ u is by item 1, since (u ⋁ w) ≤ (v ⋁ w) ⋁ u.  The second one, (u ⋁ w) ⋀ u ⊢ (v ⋁ w), simplifies to u ⊢ (v ⋁ w), which follows from u ⊢ v and the fact that u ⊢ _ is upwards-closed.

4.  If u ⊢ v ⋀ w then u ⊢ v and u ⊢ w since u ⊢ _ is upwards-closed.  Conversely, let us assume that u ⊢ v and u ⊢ w.  We rewrite u ⊢ v as u ⊢ (v ⋀ w) ⋁ v and we cut it against u ⋀ v ⊢ (v ⋀ w) (which we obtain by item 2 from u ⊢ w) on v.  The result is the desired u ⊢ v ⋀ w.

5. If u ⋁ v ⊢ w, then u ⊢ w and v ⊢ w since _ ⊢ w is downwards-closed.  Conversely, let us assume that u ⊢ w and v ⊢ w.  From u ⊢ w and using item 3, we obtain (u ⋁ v) ⊢ v ⋁ w.  We cut it against (u ⋁ v) ⋀ v ⊢ w (equivalently, v ⊢ w) on v and we obtain the desired statement u ⋁ v ⊢ w.  ☐

Remark C.1.  It is easy to see that ≤ is a sequent theory.  By Lemma C, item 1, ≤ is the smallest sequent theory.

Remark C.2.  By Lemma C, item 5, _ ⊢ w is not just an ideal, it is also closed under binary suprema.  In particular, it is closed under arbitrary suprema, which we can always write as directed suprema of finite suprema.  It immediately follows that given any w ∈ Ω, there is a largest element u ∈ Ω such that u ⊢ w.  We write this element u as ν⊢(w).  Yes, I am hinting at the fact that ν⊢ is a nucleus.

Lemma D.  The complement of a sequent theory is a sieve.

Proof.  Let ⊢ be a sequent theory on a frame Ω, and let S be its complement, namely the set of formal crescents (u, v) such that u ⊬ v.

  1. Given any empty formal crescent (u, v), by definition u ≤ v.  By Lemma C, item 1, u ⊢ v, so (u, v) is not in S.
  2. We wish to show that S is upwards-closed.  Let (u, v) be a formal crescent in S, so u ⊬ v, and let us assume another formal crescent (u’, v’) such that (u, v) ⊑ (u’, v’), in other words u ≤ v ∨ u’ and u ∧ v’ ≤ v.  We claim that (u’, v’) is in S.  We reason by contradiction, and we assume that it is not, namely that u’ ⊢ v’.  From u ≤ v ∨ u’ and using Lemma C, item 1, u ⊢ v ∨ u’.  We cut this against u ⋀ u’ ⊢ v on u’ to obtain u ⊢ v, which is impossible; the statement u ⋀ u’ ⊢ v is obtained as follows: from u’ ⊢ v’, using Lemma C, item 2, we obtain u ⋀ u’ ⊢ v ⋀ v’, and then u ⋀ u’ ⊢ v since u ⋀ u’ ⊢ _ is upwards-closed.
  3. Refinement closure is a rephrasing of the (cut) rule.  We wish to show that for every formal crescent (u, v) in S, for every u’ in Ω, (u ∧ u’, v) or (u, v ∨ u’) is in S.  The contrapositive is: if u ∧ u’ ⊢ v and u ⊢ v ∨ u’ then u ⊢ v, which is the (cut) rule.
  4. Finally, we wish to show that S is accessible, namely that if (u, v) is in S and u = ⋁i ∈ I ui, then (ui, v) is in S for some i in I.  The contrapositive is: if ui ⊢ v for every i ∈ I, then u ⊢ v, and this holds by Remark C.2. ☐

Following up on Remark C.2, ν⊢ is a nucleus, namely a monotonic map that preserves binary infima, such that id ≤ ν⊢  and ν⊢  o ν⊢ ≤ ν⊢ (hence ν⊢ o ν⊢ = ν⊢).  Indeed, ν⊢ is defined as mapping every w ∈ Ω to the largest u ∈ Ω such that u ⊢ w; equivalently, the largest u ≥ w such that u ⊢ w.  In the May 2016 post, we had defined a function νS from any sieve S as mapping every w ∈ Ω to the largest u ∈ Ω such that (u, w) ∉ S, and we had shown that νS is a nucleus.  Taking the complement of ⊢ for S, we see that ν⊢=νS, so ν⊢ is a nucleus.

Conversely, we had seen that given any nucleus ν, we could retrieve the sieve it comes from by letting S be the set of formal crescents (u, v) such that u ≰ ν(v).  Hence we retrieve the sequent theory ⊢ from any given nucleus ν by letting u ⊢ v if and only if u ≤ ν(v).

Back to 2-frames

In the June 2026 post, I had defined a 2-frame as a triple (L+, L–, _; _ ⊢ _; _) consisting of two frames L+, L– and a 4-ary relation _; _ ⊢ _; _ (or just ⊢) with a list of ten properties (!).  I have announced at the beginning of this post that I would change the (cut+) and (cut–) rules.  I will also write ⊢2 for the 4-ary relation, in order to distinguish it visually from a sequent theory ⊢.  Here is our modified definition. I am pretty much convinced that the tight 2-frames are exactly Anna Laura Suarez’ finitary biframes [5, Section 3]. (Thanks to Tomáš Jakl for mentioning this paper to me!) I will not verify this formally, but everything points to this conclusion.

Definition E. A 2-frame is a triple (L+, L–, _; _ ⊢2 _; _) consisting of two frames L+, L– and a 2-sequent theory, namely a 4-ary relation _; _ ⊢2 _; _ (⊢2 for short) such that:

  • the binary relation _; u– ⊢2 _; v– is a sequent theory on L+ for all u–, v– in L–;
  • the binary relation u+; _ ⊢2 v+; _ is a sequent theory on L– for all u+, v+ in L+..

It is tight if and only if, in addition:

  • _; ⊤ ⊢2 _; ⊥ is ≤, the smallest sequent theory on L+;
  • ⊤; _ ⊢2 ⊥; _ is ≤, the smallest sequent theory on L–.

The latter two conditions were numbered 7 and 8 in the June 2026 post, and I have made them optional: some 2-frames will be tight, some will not.  The first two conditions sum up all the remaining conditions (modulo our change to the cut rules).

In the same post, I made the remark that I did not need any of the axioms to build a dual adjunction between bitopological spaces and 2-frames, and that I only needed (axiom+) and (axiom–) in order to build the free 2-frame.  (The (axiom+) and (axiom–) properties are Lemma C, item 1, applied to the sequent theories _; u– ⊢2 _; v– and u+; _ ⊢2 v+; _.) Therefore, all the theorems proved there still hold with the new definition.  Let me recapitulate them here.

Theorem E.  There is an adjunction 2O ⊣ 2pt between biTop and 2Frmop.  Its unit is defined at every bitopological space X as ηX : X → 2pt 2OX, ηX(x) ≝ (η+X(x), η–X(x)) where η+X(x) ≝ {U+ ∈ O+X | x ∈ U+} and η–X(x) ≝ {U– ∈ O–X | x ∈ U–}.

Here O+X is the collection of open subsets of X with its first topology, and O–X is its collection of open subsets with the second topology.

Remark E.1.  Additionally, for every bitopological space X, 2OX is tight.

Let S+X be the sobrification of X with respect to its first topology, consisting of the irreducible closed subsets of X in its first topology.  We define S–X similarly.

The 2-sobrification 2SX ≅ 2pt 2OX of a bitopological space X is the collection of pairs (C+, C–) ∈ S+X × S–X such that for all U+ ∈ O+X and U– ∈ O+X, if U+ intersects C+ and U– intersects C–, then U+ ⋂ U– intersects C+ ⋂ C–.  This is a bitopological space with the following two topologies:

  • O+ 2SX consists of the sets ♢+ U+ ≝ {(C+, C–) ∈ 2SX | C+ intersects U+}, where U+ ranges over O+X;
  • O– 2SX consists of the sets ♢– U– ≝ {(C+, C–) ∈ 2SX | C– intersects U–}, where U– ranges over O–X.

Proposition F.  For a bitopological space X, the following are equivalent:

  1. ηX : X → 2SX is bijective;
  2. ηX : X → 2SX is an isomorphism in biTop;
  3. X is 2-sober, namely every irreducible pair is equal to (↓+x, ↓–x) for a unique point x of X.An irreducible pair is a pair (C+, C–) ∈ S+X × S–X such that:
    • (a) C+ and C– intersect,
    • (b) and for every pair of sets U+ ∈ O+X and U– ∈ O–X, if U+ intersects C+ and U–intersects C–, then U+ ⋂ U– intersects C+ ⋂ C–.
  4. X is pairwise T0 (namely, the intersection of the specialization preorderings ≤+ and ≤– of O+X and O–X respectively is a partial ordering, i.e., it is antisymmetric) and every irreducible pair is equal to (↓+x, ↓–x) for some point x of X.

Theorem G.  For every 2-frame L ≝ (L+, L–, ⊢), 2pt L is 2-sober. The 2O ⊣ 2pt adjunction is idempotent, so the monad 2S is idempotent on biTop.

Finally, we can build the free 2-frame over pairs of disjoint sets G+ and G–.  For every set G, let FG be the set of downwards-closed subsets of Pfinop(G), where Pfin(G) is the collection of finite subsets of G ordered by inclusion, and Pfinop(G) is the same set ordered by reverse inclusion.  Hence FG is the set of upwards-closed subsets of Pfin(G).

Theorem H.  For every pair of disjoint sets G+ and G–, there is a free 2-frame 2F(G+, G–) on (G+, G–), and this is (FG+, FG–, ⊩2) where D+; D– ⊩2 D’+; D’– if and only if D+ ⊆ D’+ or D–⊆ D’–.  Explicitly, there is a pair of functions iG+ : G+ → FG+ and iG– : G– → FG–, and for every 2-frame L ≝ (L+, L–, ⊢2), every pair of functions f+ : G+ → L+ and f– : G– → L– extends to a unique 2-frame homomorphism (f!+, f!–) : 2F(G+, G–) → L, where extending means that f!+ o iG+ = f+ and f!–o iG– = f–.

Remark H.1.  2F(G+, G–) is always tight.  Hence it is also the free tight 2-frame on (G+, G–).

2-sublocales

Let us reason as we did in order to discover the notion of sieves in the May 2016 post.  Sieves were meant to be a point free analogue of the notion of subspace, and were eventually equivalent to sublocales, and therefore also to nuclei.  The basic idea behind a sieve was that the best way we could identify a subspace A of a topological space X when we only have access to the open subsets of X, not to its points, was to look at the crescents U–V that intersect A.  A crescent is simply the difference between two open subsets U and V of X.  A syntax for such crescents is what we called formal crescents, which are just pairs (U, V) of two open subsets of X.  And then we discovered that the collection of formal crescents (U, V) such that U–V intersects A is a sieve.  With Lemmata B and D in this post, the collection of formal crescents (U, V) such that U–V is disjoint from A is a sequent theory.

With bitopological spaces, it is natural to look at 2-crescents, which are differences (U+ ⋂ U–) – (V+ ∪ V–), where U+and V+ are open subsets of X in its first topology, and  U+ and V+ are open subsets of X in its first topology.  Note also that a 2-crescent is simply the intersection of U+, U–, the complement of V+, and the complement of V–.

A formal 2-crescent is then simply the corresponding 4-tuple (U+, U–, V+, V–).  We say that is is empty if and only if the corresponding 2-crescent is empty; equivalently, if U+; U– ⊢2  V+; V–, where ⊢2 is the 2-sequent theory of 2OX.  Let E be the set of formal 2-crescents whose corresponding 2-crescents intersect A.  Then:

  1. No formal 2-crescent in E is empty.
  2. E is upwards-closed with respect to ⊑2, where ⊑2 encodes inclusion of 2-crescents on formal 2-crescents (explicitly, (U+, U–, V+, V–) ⊑2 (U’+, U’–, V’+, V’–) if and only if the four following conditions are satisfied: (a) U+; U– ⊢2  V+ ∪ U’+; V– (b) U+; U– ⊢2  V+; V– ∪ U’– (c) U+ ⋂ V’+; U– ⊢2  V+; V– and (d) U+; U–  ⋂ V’– ⊢2  V+; V–).
  3. E is 2-refinement-closed: for every (U+, U–, V+, V–) ∈ E,
    • for every open subset W+ of X in the first topology, (U+ ⋂ W+, U–, V+, V–) or (U+, U–, V+ ∪ W+, V–) is in E(namely, letting C be the 2-crescent (U+ ⋂ U–) – (V+ ∪ V–), C ⋂ W+ or C – W+ must intersect E);
    • for every open subset W– of X in the second topology, (U+, U– ⋂ W–, V+, V–) or (U+, U–, V+, V– ∪ W–) is in E (namely, letting C be the 2-crescent (U+ ⋂ U–) – (V+ ∪ V–), C ⋂ W– or C – W– must intersect E).
  4. E is 2-accessible: for every (U+, U–, V+, V–) ∈ E,
    • if U+ is the union of a family of open subsets (Ui+)i ∈ I of X in the first topology, then (Ui+, U–, V+, V–) ∈ Efor some i ∈ I;
    • if U– is the union of a family of open subsets (Ui–)i ∈ I of X in the second topology, then (U+, Ui–, V+, V–) ∈ E for some i ∈ I.

Let us simplify.

Proposition I. The above conditions 1–4 are equivalent to:

  • A. for every formal crescent (U–, V–) on X with its second topology, the collection E(U–, V–) of formal crescents (U+, V+) on X with its first topology such that (U+, U–, V+, V–) ∈ E is a sieve;
  • B. for every formal crescent (U+, V+) on X with its first topology, the collection E(U+, V+) of formal crescents (U–, V–) on X with its second topology such that (U+, U–, V+, V–) ∈ E is a sieve;
  • C. the implication U+; U– ⊢2  V+; V– ⇒ (U+, U–, V+, V–) ∉ E holds, for every formal 2-crescent (U+, U–, V+, V–).

Proof.  Let us assume that conditions 1–4 hold.  We first show that condition A holds, namely that E(U–, V–) is a sieve.

  • The crescents (U+, V+) in E(U–, V–) are non-empty: otherwise U+ – V+ would be empty, so the smaller set (U+⋂ U–) – (V+ ∪ V–) would be empty as well, contradicting condition 1.
  • If (U+, V+) in E(U–, V–) and U+–V+ is included in U’+–V’+, then (U+ ⋂ U–) – (V+ ∪ V–) is included in (U’+ ⋂ U–) – (V’+ ∪ V–).  (U+, V+) in E(U–, V–) means that (U+, U–, V+, V–) ∈ E, and by condition 2 it follows that (U’+, U–, V’+, V–) is also in E, namely that (U’+, V’+) is in E(U–, V–).  Therefore E(U–, V–) is upwards-closed.
  • If (U+, V+) in E(U–, V–), then (U+, U–, V+, V–) ∈ E, and condition 3 tells us that for every open subset W+ of X in the first topology, (U+ ⋂ W+, U–, V+, V–) or (U+, U–, V+ ∪ W+, V–) is in E.  In other words, (U+ ⋂ W+, V+) or (U+, V+ ∪ W+) is in E(U–, V–), showing that E(U–, V–) is refinement-closed.
  • If (U+, V+) in E(U–, V–) and U+ is the union of a family of open subsets (Ui+)i ∈ I of X in the first topology, then (U+, U–, V+, V–) ∈ E, and by condition 4, (Ui+, U–, V+, V–) ∈ E for some i ∈ I.  Therefore (Ui+, V+) in E(U–, V–), showing that E(U–, V–) is accessible.

Second, the fact that condition B holds is similar.  Condition C is obvious, since U+; U– ⊢2  V+; V– is equivalent to the emptiness of (U+, U–, V+, V–), and no empty formal 2-crescent is in E by condition 1.

Conversely, let us assume that conditions A, B and C hold.  We have just observed that condition A is a rephrasing of condition 1, so condition 1 holds.  Condition 3 is a rephrasing of the fact that all the sets E(U–, V–) and E(U+, V+) are refinement-closed, and condition 4 is a rephrasing of the fact that all the sets E(U–, V–) and E(U+, V+) are accessible.

It remains to show condition 2, namely that if (U+, U–, V+, V–) ⊑2 (U’+, U’–, V’+, V’–) and if (U+, U–, V+, V–) ∈ E, then (U’+, U’–, V’+, V’–) ∈ E.  This is pretty technical.  By assumption:

(a) U+; U– ⊢2  V+ ∪ U’+; V–      (b) U+; U– ⊢2  V+; V– ∪ U’–
(c) U+ ⋂ V’+; U– ⊢2  V+; V– and (d) U+; U– ⋂ V’– ⊢2  V+; V–.

We proceed in five steps.  The first first are rather similar, and use (a), (c), (b) and (d) respectively.

  • We have (U+, U–, V+, V–) ∈ E, and E(U–, V–) is a sieve, so (U+ ⋂ U’+, U–, V+, V–) or (U+, U–, V+ ∪ U’+, V–) is in E by refinement-closure.  By (a) and condition C, (U+, U–, V+ ∪ U’+, V–) cannot be in E.  Therefore (U+ ⋂ U’+, U–, V+, V–) ∈ E.
  • Since (U+ ⋂ U’+, U–, V+, V–) ∈ E and E(U–, V–) is a sieve, (U+ ⋂ U’+ ⋂ V’+, U–, V+, V–) or (U+ ⋂ U’+, U–, V+ ∪ V’+, V–) is in E by refinement-closure.  Since (U+ ⋂ U’+ ⋂ V’+) – V+ is included in (U’+ ⋂ V’+) – V+, and since E(U–, V–) is upwards-closed, the first case would imply (U’+ ⋂ V’+, U–, V+, V–) ∈ E; and this is impossible by (c) and condition C.  Therefore (U+ ⋂ U’+, U–, V+ ∪ V’+, V–) ∈ E.
  • Since (U+ ⋂ U’+, U–, V+ ∪ V’+, V–) ∈ E and E(U+ ⋂ U’+, V+ ∪ V’+) is a sieve, (U+ ⋂ U’+, U– ⋂ U’–, V+ ∪ V’+, V–) or (U+ ⋂ U’+, U–, V+ ∪ V’+, V–∪ U’–) is in E by refinement-closure.  Since (U+ ⋂ U’+) – (V+ ∪ V’+) is included in U+ – V+ and E(U– ∪ U’–, V–) is upwards-closed, the second case would imply (U+, U–, V+, V–∪ U’–) ∈ E, which is impossible by (b) and condition C.  Therefore (U+ ⋂ U’+, U– ⋂ U’–, V+ ∪ V’+, V–) ∈ E.
  • Since (U+ ⋂ U’+, U– ⋂ U’–, V+ ∪ V’+, V–) ∈ E and E(U+ ⋂ U’+, V+ ∪ V’+) is a sieve, (U+ ⋂ U’+, U– ⋂ U’– ⋂ V’–, V+ ∪ V’+, V–) or (U+ ⋂ U’+, U– ⋂ U’–, V+ ∪ V’+, V– ∪ V’–) is in E by refinement-closure.  Since (U+ ⋂ U’+) – (V+ ∪ V’+) is included in U+ – V+ and E(U– ⋂ U’– ⋂ V’–, V–) is upwards-closed, the first case would imply (U+, U– ⋂ U’– ⋂ V’–, V+, V–) ∈ E; then, since (U– ⋂ U’– ⋂ V’–) – V– is included in (U– ⋂ V’–) – V– and E(U+, V+) is upwards-closed, we would obtain that (U+, U– ⋂ V’–, V+, V–) ∈ E, which is impossible by (d) and condition C.  It follows that (U+ ⋂ U’+, U– ⋂ U’–, V+ ∪ V’+, V– ∪ V’–) ∈ E.
  • Finally, (U+ ⋂ U’+) – (V+ ∪ V’+) is included in U’+ – V’+ and E(U– ⋂ U’–, V– ∪ V’–) is upwards-closed, so (U’+, U– ⋂ U’–, V’+, V– ∪ V’–) ∈ E; and (U– ⋂ U’–) – (V– ∪ V’–) is included in U’– – V’– and E(U’+, V’+) is upwards-closed, so (U’+,U’–, V’+, V’–) ∈ E. ☐

By Proposition I, and by the fact that complements of sieves coincide with sequent theories (Lemmas B and D), we are led to the fact that a 2-sublocale—the 2-frame analogue of a subspace of a bitopological space— of a 2-frame (L+, L–, _; _ ⊢2 _; _) should simply be a 2-sequent theory ⊩2 (conditions A and B of Proposition I) such that ⊢2 ⊆ ⊩2.

One can then define free 2-frames specified by generators and relations, answering Tomáš Jakl’s initial question (well, at least partially; his question was a lot longer, and I will not prove that they are free in any sense):

  • We start from the generators: two disjoint sets G+ and G–.
  • We form the free 2-frame 2F(G+, G–) = (FG+, FG–, ⊩2) (see Theorem H).
  • We now consider a set of relations, which will simply be formal statements « D+; D– ⊢2 D’+; D’–», for various elements D+, D’+ of FG+, and D–, D’– of FG–.
  • We form the smallest 2-sequent theory ⊢2 such that D+; D– ⊢2 D’+; D’– for every formal statement « D+; D– ⊢2D’+; D’–» in the given set of relations.
  • Our final 2-frame specified by generators and relations is (FG+, FG–, ⊢2).

We note that ⊢2 is defined as the smallest 2-sequent theory containing a specific set of 4-sequents, and this makes sense since any intersection of 2-sequent theories is a 2-sequent theory.  We also note that every 2-sequent theory must contain ⊩2: if D+; D– ⊩2 D’+; D’– then D+ ⊆ D’+ or D–⊆ D’–; if D+ ⊆ D’+ then D+; D– ⊢2 D’+; D’– by the fact that _; D– ⊢2 _; D’– is a sequent theory, and therefore _; D– ⊢2 D’+; D’– is and ideal, and is in particular downwards-closed; similarly if D–⊆ D’–.

Therefore our free 2-frame generated by generators and relations is a 2-sublocale of the free 2-frame 2F(G+, G–) defined by generators and no relation.

Simple biframes

It would seem like we have now reached a satisfactory theory of 2-frames, with an adjunction 2O ⊣ 2pt, with a notion of 2-sublocales, with a way of presenting 2-frames by generators and relations. Let me recall that, unless I have made a mistake, what I call (tight) 2-frames here are Suarez’ finitary biframes [5].

However, this theory lacks in other respects. Once you obtain a 2-sublocale of a 2-frame (L+, L–, ⊢2), in the form of a 2-sequent theory ⊩2 containing ⊢2, what 2-frame does it define? The obvious answer is (L+, L–, ⊩2), but look at it this way. Consider the inconsistent relation for ⊩2, namely the relation that relates all possible 4-tuples. The topological intuition is that this is the relation 2-sequent theory associated with an empty subspace. In Top, the empty space is the initial object. One would then expect the 2-sublocale (L+, L–, ⊩2) to be a terminal object, but it is not. There are in general way too many elements in L+ and in L–. The problem is that one should consider tight 2-sublocales instead, as with Suarez’ assembly of a finitary biframe [5, Section 4].

Another weakness, or so I thought initially, is as follows. Given two elements (v+, v–) ∈ L+ × L–, the set {(u+, u–) ∈ L+ × L– | u+; u– ⊢2 v+; v–} is a C-ideal. A C-ideal is a downwards-closed subset L+ × L– that is closed under directed suprema on each coordinate, the other coordinate being fixed. The C-ideals are elements of the coproduct L++L– of the two frames L+ and L–; this coproduct can be described, up to isomorphism, as the frame of the Galois connections between L+ and L–, as I did in the book. Just like sequent theories are equivalent to sieves, hence to sublocales and to nuclei, this leaves the impression that 2-sequent theories might be equivalent to nuclei on L++L–, but this does not work out. You have to replace C-ideals by finitary C-ideals, namely C-ideals obtained as finite unions of rectangles. (I will tell you what a rectangle is below.) This is the sublocale analogue of Suarez’ finitary congruences [5, Lemma 3.1 and previous text].

Let us return to our bitopological intuition that, when L+ = O+X and L– = O–X for some bitopological space X, the 2-sequent theory ⊢2 of 2OX is given by U+; U– ⊢2 V+; V– if and only if U+ ⋂ U– ⊆ V+ ∪ V–, for all U+, V+ ∈ O+X and U–, V– ∈ O–X; and that every subspace A yields a sub-2-sequent theory ⊩2 by letting U+; U– ⊩2 V+; V– if and only if (U+ ⋂ U–) – (V+ ∪ V–) is disjoint from A.

Let us consider the patch topology on X, namely the coarsest topology that contains both O+X and O–X. Its elements can all be written as ∪i ∈ I (U+i ⋂ U–i), where U+i ∈ O+X and U–i ∈ O–X. Let us call such sets patch-open. The elementary patch-open subsets of X those where we can take I finite. By distributing intersections over unions, every elementary patch-open subset of X can be written as ∩j ∈ J (V+j ∪ V–j), where V+j ∈ O+X and V–j ∈ O–X, and J is finite. (This does not work for non-elementary patch-open subsets of X, as you should note.) Now ∪i ∈ I (U+i ⋂ U–i) ⊆ ∩j ∈ J (V+j ∪ V–j) if and only if for every i ∈ I, for every j ∈ J, U+i ⋂ U–i ⊆ V+j ∪ V–j, where the latter inclusion is expressible using ⊢2. Similarly, we can express the fact that the crescent (∪i ∈ I (U+i ⋂ U–i)) – (∩j ∈ J (V+j ∪ V–j)) is disjoint from A by requiring that for every i ∈ I, for every j ∈ J, (U+i ⋂ U–i) – (V+j ∪ V–j) is disjoint from A, and we can write the latter disjointness condition using ⊩2. However this all works for differences of a patch-open subset ∪i ∈ I (U+i ⋂ U–i) and an elementary patch-open subset ∩j ∈ J (V+j ∪ V–j), with J finite. This is what 2-sequent theories model.

What 2-sequent theories lack is the possibility of reasoning with arbitrary patch-open subsets. Here is our final fix. On the localic side, we will encode patch-open subsets by elements of L++L–. When L+ = O+X and L– = O–X for some bitopological space, we will take the semantics of a C-ideal I ∈ L++L– to be ⟦I⟧ ≝ ∪(U+, U–) ∈ I (U+ ⋂ U–). Instead of considering 2-sequent theories, we will simply consider sequent theories on L++L–, or equivalently nuclei on L++L–, or equivalently sublocales of L++L–. This will be Definition J below.

At this point, we need to set a few things straight about coproducts L++L– of frames. Since they are coproducts, we have the following:

  • for all u+ ∈ L+ and u– ∈ L–, there is a C-ideal u+ × u– ≝ ↓(u+, u–); this is the rectangle defined by u+ and u–;
  • there are canonical injections ι+ : L+ → L++L– and ι– : L– → L++L–, defined by ι+ (u+) ≝ u+ × ⊤ and ι– (u–) ≝ ⊤ × u–; those are frame homomorphisms, and are mono in the category Frm of frames, in other words they are injective frame homomorphisms;
  • (the universal property of coproducts) for all frame homomorphisms φ+ : L+ → Ω and φ– : L– → Ω, there is a unique frame homomorphism ⟨ φ+, φ– ⟩ : L++L– → Ω such that ⟨ φ+, φ– ⟩ o ι+ = φ+ and ⟨ φ+, φ– ⟩ o ι– = φ–; the homomorphism ⟨ φ+, φ– ⟩ maps every C-ideal I to ∨(u+, u–) ∈ I (φ+ (u+) ∧ φ– (u–));
  • in particular, for all frame homomorphisms φ+ : L+ → L’+ and φ– : L– → L’+, we can form the frame homomorphism φ++φ– : L++L– → L++L–, defined as ⟨ ι+ o φ+, ι– o φ– ⟩, or (slightly more) explicitly by: (φ++φ–) (I) ≝ ∨(u+, u–) ∈ I (φ+ (u+) × φ– (u–)), where ∨ denotes supremum in L++L–.

We arrive at our final notion. Soon enough, we will see that this is very much related to Banaschewski, Brümmer and Hardie’s notion of biframe [3, 4], so I will call them simple biframes. It will also be convenient to reason on a relaxed notion, which I will call simple lax biframes. A simple lax biframe is a triple (L+, L–, ⊢) where L+ and L– are frames and ⊢ is a sequent theory on L++L–. A simple biframe is a simple lax biframe that is tight, in the sense that for all u+, u’+ ∈ L+ and u–, u’– ∈ L–, u+ × ⊤ ⊢ u’+ × ⊤ implies (hence is equivalent to) u+ ≤ u’+, and ⊤ × u– ⊢ ⊤ × u’– implies (hence is equivalent to) u– ≤ u’–.

A morphism φ : (L+, L–, ⊢) → (L’+, L’–, ⊢’) of simple (lax or tight) biframes is a pair of frame homomorphisms φ+ : L+ → L’+ and φ– : L– → L’– such that φ++φ– preserves sequent theories, namely: for all C-ideals I and J on L++L–, if I ⊢ J then (φ++φ–) (I) ⊢’ (φ++φ–) (J).

It will be more practical to use nuclei instead of sequent theories, so here is the actual definition we will use.

Definition J. A simple lax biframe is a triple (L+, L–, ν) where:

  • L+ and L– are frames;
  • ν is a nucleus on L++L–.

It is tight if and only if for all u+, u’+ ∈ L+ and u–, u’– ∈ L–, u+ × ⊤ ⊆ ν (u’+ × ⊤) implies (hence is equivalent to) u– ≤ u’– and ⊤ × u– ⊆ ν (⊤ × u’–) implies (hence is equivalent to) u– ≤ u’–. A simple biframe is a simple lax biframe that is tight.

A morphism φ : (L+, L–, ν) → (L’+, L’–, ν’) of simple (lax or tight) biframes is a pair of frame homomorphisms φ+ : L+ → L’+ and φ– : L– → L’– such that for every C-ideal I on L++L–, (φ++φ–) (ν (I)) ⊆ ν’ ((φ++φ–) (I)).

Together, these define a category laxbiFrm of lax simple biframes (resp. biFrm of simple biframes). Oh, why not laxsimplebiFrm and simplebiFrm? Isn’t there a risk of confusion with a category of biframes, in the sense of [3, 4]? There is a confusion, but I claim that is not a risk at all: simple biframes and biframes are… essentially the same thing, as we will now see.

Simple biframes are biframes

A biframe is a triple (L+, L–, L0) of frames such that L+ and L– are subframes of L0, which generate L0, in the sense that every element of L0 is a supremum of binary infima u+ ∧ u– with u+ ∈ L+ and u– ∈ L– [3, 4]. We will understand “subframe” as meaning “subframe up to frame isomorphism”. Explicitly, we will take the latter definition to mean that (L+, L–, L0) is a triple of frames, there are two monos i+ : L+ → L0 and i– : L– → L0 in Frm (injective frame homomorphisms) such that every element of L0 is a supremum of binary infima i+ (u+) ∧ i– (u–) with u+ ∈ L+ and u– ∈ L–.

In order to see that simple biframes are biframes, we first need to say how nuclei create frames. We will then apply this to nuclei on L++L–.

Let me recall from the May 2016 post that nuclei on a frame Ω and sublocales of Ω are two faces of the same coin. Given a nucleus ν on Ω we obtain a sublocale as the set of fixed points of ν, or equivalently as its image Im ν. (Every element ν(u) of Im ν is a fixed point because ν (ν (u)) = ν (u), and conversely every fixed point of ν is trivially in Im ν.) We equip Im ν with the restriction of the ordering ≤ on Ω, and we wish to show that Im ν is a frame with this ordering.

There is pitfall here: in Im ν, infima will be computed as in the surrounding frame Ω, but suprema will not.

  • We start with infima. Let (ui)i ∈ I be a family of elements of Im ν, and let u ≝ ∧i ∈ I ui be their infimum in Ω. We need to show that u is a fixed point of ν, and then it will automatically be the infimum of (ui)i ∈ I in Im ν. We already know that u ≤ ν (u). In the reverse direction, since ν is monotonic and u ≤ ui for every i ∈ I, we have ν (u) ≤ ∧i ∈ I ν (ui), and the latter is equal to ∧i ∈ I ui = u since every ui is a fixed point of ν.
  • Let (ui)i ∈ I be a family of elements of Im ν. I claim that their supremum in Im ν is u ≝ ν (∨i ∈ I ui). This element u is clearly in Im ν, and above every ui. It remains to show that it is the least upper bound of (ui)i ∈ I in Im ν. Let v be any upper bound of that family in Im ν. In particular, v = ν (v), and ∨i ∈ I ui ≤ v. Since ν is monotonic, we obtain that v = ν (v) is larger than or equal to ν (∨i ∈ I ui) = u.
  • In order to see that Im ν is a frame, we wish to show that (arbitrary) suprema distribute over binary infima. That is, and writing (temporarily) ⊔ for supremum in Im ν, we wish to show that v ∧ ⊔i ∈ I ui = ⊔i ∈ I (v ∧ ui), for all elements v and ui of Im ν. Using the definition of suprema, as given above, this means that our goal is to show that v ∧ ν (∨i ∈ I ui) = ν (∨i ∈ I (v ∧ ui)). Since v is a fixed point of ν and ν commutes with binary infima, the left-hand side is equal to ν (v ∧ ∨i ∈ I ui), hence to ν (∨i ∈ I (v ∧ ui)), since Ω is a frame.

Let us return to simple biframes (L+, L–, ν). We let L0 ≝ Im ν. We have just seen that this is a frame, which happens to be a sublocale of L++L–. There are two maps i+ : L+ → L0 and i– : L– → L0, defined by i+ (u+) ≝ ν (u+ × ⊤) and i– (u–) ≝ ν (⊤ × u–). Then, dealing with i+ only, since the case of i– is similar:

  • i+ takes its values in Im ν, and is clearly monotonic.
  • The function i+ preserves finite infima: given finitely many elements u+1, …, u–n, i+, i+ (u–1 ∧ … ∧ u+n) = ν ((u–1 ∧ … ∧ u–n) × ⊤) = ν ((u–1 × ⊤) ⋂ … ⋂ (u+n × ⊤)) = ν (u–1 × ⊤) ⋂ … ⋂ ν (u+n × ⊤) (since ν preserves finite infima) = i+ (u–1) ⋂ … ⋂ i+ (u–n).
  • The function i+ preserves arbitrary suprema. We recall that suprema in L0 are given by taking suprema in the surrounding frame L++L– and then applying ν. Let (ui)i ∈ I be a family of elements of L+, with supremum u. The supremum of the family (i+ (ui))i ∈ I is ν (∨i ∈ I (ui × ⊤)), and we wish to show that this is equal to i+ (u) = ν (u × ⊤). It suffices to show that the supremum ∨i ∈ I (ui × ⊤), taken in L++L–, is u × ⊤. The latter is clearly an upper bound, and we have to show that it is least. Let J be another upper bound, namely a C-ideal such that ui × ⊤ ⊆ J for every i ∈ I, namely such that (ui, ⊤) ∈ J for every i ∈ I. Since J is a C-ideal, hence is closed under suprema taken on one component, the other component being constant, J must also contain (u, ⊤); so (u × ⊤) ⊆ J.
  • Hence i+ is a frame homomorphism, and we claim that it is injective. It suffices to show that i+ (u+) ⊆ i+ (v+) implies u+ ≤ v+. (Then swap u+ and v+ in order to obtain the other inequality.) We assume that i+ (u+) ⊆ i+ (v+), namely that ν (u+ × ⊤) ⊆ ν (v+ × ⊤). In particular, (u+ × ⊤) ⊆ ν (v+ × ⊤). Since the simple biframe (L+, L–, ν) is tight, it follows that u+ ≤ v+.

Finally, we claim that every element I of L0 is a supremum of binary infima i+ (u+) ∧ i– (u–) with u+ ∈ L+ and u– ∈ L–. Since I is a C-ideal, I is the union, and also the supremum in L++L–, of the rectangles u+ × u– where (u+, u–) ranges over I: in notation, I = ∨(u+, u–) ∈ I (u+ × u–). Since I is in L0 = Im ν, I is a fixed point of ν, so I = ν (∨(u+, u–) ∈ I (u+ × u–)). Each rectangle u+ × u– is smaller than or equal to ν (u+ × u–) = ν ((u+ × ⊤) ⋂ (⊤ × u–)) = ν (u+ × ⊤) ⋂ ν (⊤ × u–) = i+ (u+) ∧ i– (u–). Therefore I ⊆ ν (∨(u+, u–) ∈ I (i+ (u+) ∧ i– (u–))). The latter is the supremum (in L0!) of the terms i+ (u+) ∧ i– (u–). The reverse inequality is easy: every term i+ (u+) ∧ i– (u–) = ν (u+ × u–) is included in ν (I) = I, so their supremum (in L0) is also included in I. Therefore I is the supremum (in L0) of the binary infima i+ (u+) ∧ i– (u–), where (u+, u–) ranges over I.

We have proved the following (“every simple biframe is a biframe”).

Proposition K. For every simple biframe (L+, L–, ν), there is an associated biframe (L+, L–, L0) where L0 ≝ Im ν, L+ embeds in L0 through the injective frame homomorphism u+ ↦ ν (u+ × ⊤) and L– embeds in L0 through the injective frame homomorphism u– ↦ ν (⊤ × u–).

This raises the question: is every biframe actually a simple biframe? You have guessed it: yes.

Biframes are simple biframes

Let (L+, L–, L0) be a biframe. Hence there are two monos i+ : L+ → L0 and i– : L– → L0 in Frm (injective frame homomorphisms) such that L+ and L– generate L0, namely such that every element of L0 is a supremum of binary infima i+ (u+) ∧ i– (u–) with u+ ∈ L+ and u– ∈ L–.

By the universality property of coproducts, there is a unique frame homomorphism ⟨ i+, i– ⟩ : L++L– → L0 such that ⟨ i+, i– ⟩ o ι+ = i+ and ⟨ i–, i– ⟩ o ι– = i–, where ι+ : L+ → L++L– and ι– : L– → L++L– are the canonical injections. (We recall that ι+ (u+) ≝ u+ × ⊤ and ι– (u–) ≝ ⊤ × u–.) We have ⟨ i+, i– ⟩ (I) = ∨(u+, u–) ∈ I (i+ (u+) ∧ i– (u–)) for every C-ideal I ∈ L++L–. Note that suprema are taken in L0 here. Since L+ and L– generate L0, we also realize that ⟨ i+, i– ⟩ is surjective.

Let f ≝ ⟨ i+, i– ⟩. Just as with any other frame homomorphism, and in general with any sup-preserving map, f has a right adjoint f*, namely the unique monotonic map f* : L0 → L++L– such that f o f* ≤ id and f* o f ≥ id: explicitly, f* (u) is defined as ∨ {I ∈ L++L– | f (I) ≤ u} for every u ∈ L0. Additionally, f is surjective, and in that case, we see that, in fact, f o f* = id.

Such a right adjoint, whose left adjoint preserves finite infima, is usually called a localic map, and its image is a sublocale of its codomain. We build the associated nucleus explicitly: ν ≝ f* o f.

  • The map ν is monotonic, because it is obtained as the composition of two monotonic maps.
  • Since f* o f ≥ id, we have I ⊆ ν (I) for every C-ideal I.
  • We have ν o ν = (f* o f) o (f* o f) = f* o (f o f*) o f = f* o f = ν.
  • Finally, we claim that ν preserves binary infima, namely that ν (I1 ⋂ I2) = ν (I1) ⋂ ν (I2) for all C-ideals I1 and I2. This follows from the fact that f preserves binary infima, since it is a frame homomorphism, and that f* preserves all infima, as all right adjoints do.

Proposition L. For every biframe (L+, L–, L0) (with injective frame homomorphisms i+ : L+ → L0 and i– : L– → L0), there is a simple biframe (L+, L–, ν), where ν ≝ f* o f, f ≝ ⟨ i+, i– ⟩, f* is the right adjoint of f. Additionally, f* defines a frame isomorphism of L0 onto Im ν, whose inverse is the restriction of f to Im ν.

Proof. We have already proved that (L+, L–, ν) is a simple lax biframe. We claim that it is tight.

We will need to observe that a mono in Frm, in other words, an injective frame homomorphism i, must reflect the ordering, namely that i (u) ≤ i (u’) must imply u ≤ u’. Indeed, from i (u) ≤ i) (u’), we deduce i (u) = i (u’) ∧ i (u), hence i (u) = i (u’ ∧ u), and injectivity gives us u = u’ ∧ u, whence u ≤ u’.

Let us assume that u+ × ⊤ ⊆ ν (u’+ × ⊤). (We only deal with plus signs, the case of minus signs is similar.) In other words, ι+ (u+) ⊆ ν (ι+ (u’+)). Since ν o ι+ = f* o f o ι+ = f* o ⟨ i+, i– ⟩ o ι+ = f* o i+, it follows that ι+ (u+) ⊆ f* (i+ (u+)). Since f* is right adjoint to f, the latter inclusion is equivalent to f (ι+ (u+) ≤ i+ (u+). But f o ι+ = ⟨ i+, i– ⟩ o ι+ = i+, so i+ (u+) ≤ i+ (u+). Since i+ is a mono in Frm, it reflects the ordering, so u+ ≤ u+. Therefore (L+, L–, ν) is tight.

Finally, we show that f* restricts to a frame isomorphism between L0 and Im ν. In order to see that it takes its values in Im ν it suffices to show that f* (u) is a fixed point of ν for every u ∈ L0. But ν o f* = f* o f o f* is equal to f*. This is a general fact of adjoint pairs of maps: we have f* o f o f* ≤ f* because f o f* ≤ id and f* is monotonic, and f* o f o f* ≥ f* because f* o f ≥ id. The inverse of f* : L0 → Im ν is then the appropriate restriction of f. We already know that f o f* = id, and we observe that the restriction of f* o f to Im ν is also the identity map, since f* o f o ν = ν o ν = ν. ☐

In order to complete our argument, we show that the two constructions of Propositions K and L are inverse of each other.

  • Starting from a biframe (L+, L–, L0) (with injective frame homomorphims i+ : L+ → L0 and i– : L– → L0), we build a simple biframe (L+, L–, ν) as in Proposition L: ν = f* o f, f = ⟨ i+, i– ⟩ : L++L– → L0, f* is the right adjoint of f. We get back a biframe (L+, L–, L’0) by Proposition K, with L’0 = Im ν. The second part of Proposition L tells us that f* is a frame isomorphism of L0 onto Im ν. Hence L0 and L’0 are isomorphic.
    In addition, f* maps every element of the form i+(u+) to ν (u+ × ⊤) and every element of the form i–(u–) to ν (⊤ × u–): for the first claim, we simply observe that f (ν (u+ × ⊤)) = (f o f* o f) (u+ × ⊤) = f (u+ × ⊤) (because f o f* o f = f, as with every adjoint pair) = f (ι+ (u+)) = (⟨ i+, i– ⟩ o ι+) (u+) = i+(u+); similarly for the second claim. We will see (in a later post) that this means that f* is a homomorphism of biframes, hence an isomorphism of biframes, in the sense of Banaschewski, Brümmer and Hardie [3, 4]… but I haven’t introduced homomorphism of biframes yet.
  • Starting from a simple biframe (L+, L–, ν), we form the biframe (L+, L–, L0) of Proposition K: so L0 = Im ν, L+ embeds in L0 through the injective frame homomorphism i+ : u+ ↦ ν (u+ × ⊤) and L– embeds in L0 through the injective frame homomorphism i– : u– ↦ ν (⊤ × u–). We get back a simple biframe (L+, L–, ν’) by using Proposition L, where ν’ ≝ f* o f, f ≝ ⟨ i+, i– ⟩, f* is the right adjoint of f. We claim that ν’ = ν.
    • We compute f: f is the unique frame homomorphism from L++L– to L0 such that f o ι+ = i+ and f o ι– = i–, namely such that f (u+ × ⊤) = ν (u+ × ⊤) for every u+ ∈ L+ and f (⊤ × u–) = ν (⊤ × u–) for every u– ∈ L–: uniqueness tells us that f = ν (more precisely, f is ν, after replacing its codomain by its image Im ν = L0).
    • The right adjoint f* to f = ν is defined by f* (J) = ∨ {I ∈ L++L– | f (I) ≤ J} = ∨ {I ∈ L++L– | ν (I) ≤ J} for every J ∈ L0 = Im ν. Every I ∈ L++L– such that ν (I) ≤ J must be such that I ⊆ J, and J itself is such that ν (J) ≤ J, since J ∈ Im ν. Therefore f* (J) = J, and hence f* is simply the inclusion of L0 in L++L–.
    • It follows that ν’ = f* o f = ν.

That is it for this month. We have gone through a long and winding path, starting from d-frames, through 2-frames (Suarez’ finitary frames), and we finally rediscovered Banaschewski, Brümmer and Hardie’s biframes.

  1. Tomáš Jakl. d-Frames as algebraic duals of bitopological spaces, Ph.D. thesis, Charles University and University of Birmingham, 2018.
  2. Jorge Picado and Aleš Pultr. Frames and locales — topology without points. Birkhäuser, 2010.
  3. Bernhard Banaschewski, Guillaume C. L. Brümmer and Keith A. Hardie. Biframes and bispaces. Paper read at the Symposium on Categorical Algebra and Topology University of Cape Town, 29 June—3 July 1981. Quaestiones Mathematicae Volume 6, 1983 – Issue 1-3, pages 13—25.
  4. Bernhard Banaschewski and Guillaume C. L. Brümmer. Stably continuous frames. In Mathematical Proceedings of the Cambridge Philosophical Society 104(1):7–19, Cambridge University Press, 1988.
  5. Anna Laura Suarez. The category of finitary biframes as the category of pointfree bispaces. Journal of Pure and Applied Algebra 226:106783, 2022.

— Jean Goubault-Larrecq (August 20th, 2026)

jgl-2011