Revisiting Stone duality for bitopological spaces

In the June 2025 post, I presented a form of Stone duality for bitopological spaces due to Jung and Moshier [1], and refined by Jakl [2]. A bitopological space is a triple (X, τ⁺, τ^–) of a set X with two topologies τ⁺ and τ^–. I will simply write X for a bitopological space, and O⁺X and O^–X for its two topologies.

We built the dual of X as a d-frame, namely as a quadruple (L⁺, L^–, tot, con) where L⁺ and L^– are two frames, and tot and con are two binary relations between elements of L⁺ and elements of L^– satisfying a long list of axioms. The idea is that L⁺ is an abstraction of O⁺X, L^– is an abstraction of O^–X, that (U⁺, U^–) is in tot if and only if U⁺ ∪ U^– = X, and that (U⁺, U^–) is in con if and only if U⁺ ⋂ U^– = ∅.

Introducing 2-frames

This d-frame abstraction of a bitopological space is however unable to state more complex relations between open sets of the two topologies. For example, I don’t think you can express relations of the form U⁺ ⋂ U^– ⊆ V⁺, or U⁺ ⋂ U^– ⊆ V^–, or U⁺ ⊆ V⁺ ∪ V^–, or U^– ⊆ V⁺ ∪ V^– (+ superscripts indicate elements of τ⁺, – superscripts are for elements of τ^–). More generally, one would like to express all sorts of inclusions between unions of intersections of open sets of the two topologies. If you work a bit, you will see that such inclusions can be written as conjunctions of inclusions of the simple form U⁺ ⋂ U^– ⊆ V⁺ ∪ V^–. If V⁺ and V^– are empty, then this inclusion is equivalent to U⁺ ⋂ U^– = ∅, and we retrieve the relation con. If both U⁺ and U^– are equal to X, then the inclusion U⁺ ⋂ U^– ⊆ V⁺ ∪ V^– is equivalent to V⁺ ∪ V^– = X, and this way we retrieve the relation tot.

Such inclusions are now relations of arity 4: they involve four sets U⁺, U^–, V⁺ and V^–, and I will model them on the lattice-theoretic side of the duality to come as sequents U⁺; U^– ⊢ V⁺; V^–.

Definition A. A 2-frame is a triple (L⁺, L^–, _; _ ⊢ _; _) consisting of two frames L⁺, L^– and a 4-ary relation _; _ ⊢ _; _ (or just ⊢) with the following properties, for all u⁺, v⁺, … ∈ L⁺ and u^–, v^–, … ∈ L^–:

1. the set _; u^– ⊢ v⁺; v^– ≝ {u⁺ ∈ L⁺ | u⁺; u^– ⊢ v⁺; v^–} is downwards-closed and closed under arbitrary suprema in L⁺;
2. the set u⁺; _ ⊢ v⁺; v^– ≝ {u^– ∈ L^– | u⁺; u^– ⊢ v⁺; v^–} is downwards-closed and closed under arbitrary suprema in L^–;
3. the set u⁺; u^– ⊢ _; v^– ≝ {v⁺ ∈ L⁺ | u⁺; u^– ⊢ v⁺; v^–} is upwards-closed and closed under finite infima in L⁺;
4. the set u⁺; u^– ⊢ v⁺; _ ≝ {v^– ∈ L^– | u⁺; u^– ⊢ v⁺; v^–} is upwards-closed and closed under finite infima in L^–;
5. (axiom⁺) if u⁺ ≤ v⁺ then u⁺; u^– ⊢ v⁺; v^–;
6. (axiom^–) if u^– ≤ v^– then u⁺; u^– ⊢ v⁺; v^–;
7. if u⁺; ⊤ ⊢ v⁺; ⊥ then u⁺ ≤ v⁺ in L⁺ (whence u⁺; ⊤ ⊢ v⁺; ⊥ if and only if u⁺ ≤ v⁺, using (axiom⁺));
8. if ⊤; u^– ⊢ ⊥; v^– then u^– ≤ v^– in L^– (whence ⊤; u^– ⊢ ⊥; v^– if and only if u^– ≤ v^– in L^–, using (axiom^–));
9. (cut⁺) if u₁⁺; u₁^– ⊢ v₁⁺; v₁^– and u₂⁺; u₂^– ⊢ v₂⁺; v₂^–, and if v₁⁺ ≤ u₂⁺, then u₁⁺; u₁^– ⋀ u₂^– ⊢ v₂⁺; v₁^– ⋁ v₂^–;
10. (cut^–) if u₁⁺; u₁^– ⊢ v₁⁺; v₁^– and u₂⁺; u₂^– ⊢ v₂⁺; v₂^–, and if v₁^– ≤ v₂^–, then u₁⁺ ⋀ u₂⁺; u₁^– ⊢ v₁⁺ ⋁ v₂⁺; v₂^–.

Above, we write ⊤ for the largest element of either frame L⁺ or L^–, ⊥ for its smallest element, ⋁ for supremum, ⋀ for infimum. All axioms come in pairs: 1 with 2, 3 with 4, (axiom⁺) with (axiom^–), 7 with 8, (cut⁺) with (cut^–). One way of remembering how (cut⁺) and (cut^–) work is to:

• take the two sequents u₁⁺; u₁^– ⊢ v₁⁺; v₁^– and u₂⁺; u₂^– ⊢ v₂⁺; v₂^–,
• superpose them by putting all us on the left and all vs on the right, yielding u₁⁺ ⋀ u₂⁺; u₁^– ⋀ u₂^– ⊢ v₁⁺ ⋁ v₂⁺; v₁^– ⋁ v₂^–;
• remove the one pair of elements that are comparable: v₁⁺ and u₂⁺ if v₁⁺ ≤ u₂⁺, v₁^– and v₂^– if v₁^– ≤ v₂^–.

The axioms of Definition A are heavily redundant. The ordering ≤ on L⁺ and on L^– is entirely determined from ⊢, because of property 7 (and (axiom⁺)), or of property 8 (and (axiom^–)). Hence one may also define a 2-frame as two sets L⁺ and L^– with a 4-ary relation ⊢ satisfying some properties. But we feel this would be awkward, and would hide the frame structures on L⁺ and L^–.

If you feel drowned under the number of axioms, be reassured: we are not going to use any of them. They will just happen to be true of all 2-frames that arise from bitopological spaces, through the functor 2O that we will introduce shortly. Why do we include them, then? For the same reason that we include the axiom of frame distributivity in frames: because we hope that it makes the theory nicer in the end; but frame distributivity is not needed in the usual Stone adjunction Top : O ⊣ pt : Frm^op, which is really an adjunction Top : O ⊣ pt : CLatt^op, where CLatt is the category of complete lattices, without any frame distributivity law.

Well, I just lied. In usual Stone duality, frame distributivity is useful for building free frames, to start with. I will end this note on the construction of free 2-frames, and there we will use some of the axioms; but this will be limited to (axiom⁺) and (axiom^–).

The adjunction 2O ⊣ 2pt

Starting from a bitopological space X, we can build a 2-frame 2O X ≝ (O⁺X, O^–X, ⊢_X), where U⁺; U^– ⊢_X V⁺; V^– is defined as U⁺ ⋂ U^– ⊆ V⁺ ∪ V^–. All the properties of Definition A are clearly satisfied, except perhaps (cut⁺) and (cut^–), which require a bit of verification. Let us deal with (cut⁺), since the other one is similar. We assume that:

• U₁⁺; U₁^– ⊢_X V₁⁺; V₁^–, namely U₁⁺ ⋂ U₁^– ⊆ V₁⁺ ∪ V₁^–;
• U₂⁺; U₂^– ⊢_X V₂⁺; V₂^–, namely U₂⁺ ⋂ U₂^– ⊆ V₂⁺ ∪ V₂^–;
• V₁⁺ ⊆ U₂⁺,

and we wish to show that U₁⁺ ⋂ (U₁^– ⋂ U₂^–) ⊆ V₂⁺ ∪ (V₁^– ∪ V₂^–). For every point x in U₁⁺ ⋂ (U₁^– ⋂ U₂^–), x is in U₁⁺ ⋂ U₁^– hence in V₁⁺ ∪ V₁^– by our first assumption. If x is in V₁^–, then it is in the right-hand side V₂⁺ ∪ (V₁^– ∪ V₂^–). Otherwise, x is in V₁⁺, hence in U₂⁺ by our third assumption. But we remember that x is in U₁⁺ ⋂ (U₁^– ⋂ U₂^–), hence in U₂^–; so x is in U₂⁺ ⋂ U₂^–, hence in V₂⁺ ∪ V₂^– by our second assumption; and therefore x is in the right-hand side V₂⁺ ∪ (V₁^– ∪ V₂^–).

There is a category biTop of bitopological spaces, whose morphisms are bicontinuous maps f : (X, τ⁺, τ_^–) → (Y, σ⁺, σ_^–), meaning that f is continuous both for the + and the – topologies.

Definition B. A 2-frame homomorphism f from a 2-frame (L⁺, L^–, ⊢) to a 2-frame (K⁺, K^–, ⊩) is pair of frame homomorphisms φ⁺ : L⁺ → K⁺ and φ^– : L^–→ K^– that preserve sequents, in the sense that:

• u⁺; u^– ⊢ v⁺; v^– entails φ⁺(u⁺); φ^–(u^–) ⊩ φ⁺(v⁺); φ^–(v^–) for all u⁺, v⁺ ∈ L⁺ and u^–, v^– ∈ L^–.

The identity morphisms are pairs of identity maps, composition is done pairwise. This defines a category 2Frm of 2-frames and 2-frame homomorphisms.

We have already defined a function 2O from objects of biTop to objects of 2Frm. For every bicontinuous map f : X → Y, the pair (f^–1, f^–1) defines a 2-frame homomorphism from 2O Y to 2O X: we write 2O f for this morphism; by reversing arrows, we see it as a morphism from 2O X to 2O Y in the opposite cateogry 2Frm^op.

Lemma C. 2O is a functor from biTop to 2Frm^op.

Let us define a functor in the other direction. As with almost every kind of Stone duality, it is natural to define a point of a 2-frame (L⁺, L_^–, ⊢) as a 2-frame homomorphism (x⁺, x^–) from (L⁺, L_^–, ⊢) to 2O (1), where 1 is the bitopological space with just one point * (and the unique possible topologies). 2O (1) is (2, 2, ⊢₁) where 2 is the frame {0, 1} with 0<1 (representing O1, with 0 for the empty open set and 1 for the whole space {*}), and a⁺; a^– ⊢₁ b⁺; b^– if and only if a⁺ ⋀ a^– ≤ b⁺ ⋁ b^–. It will be practical to observe that a⁺; a^– ⊢₁ b⁺; b^– fails in exactly one case: when a⁺=a^–=1 and b⁺=b^–=0.

Given a 2-frame homomorphism (x⁺, x^–) from (L⁺, L_^–, ⊢) to 2O (1), x⁺ and x^– are frame homomorphisms from L⁺ and L^– respectively to 2, and therefore are charateristic maps of some completely prime filters on L⁺ and L^– respectively: the completely prime filter associated with x⁺ is (x⁺)^–1 ({1}), and similarly with x^–. This is a with ordinary Stone duality, as described in Section 8.1 of the book.

Additionally, the fact that (x⁺, x^–) is a 2-frame homomorphism requires that u⁺; u^– ⊢ v⁺; v^– entails x⁺(u⁺); x^–(u^–) ⊢₁ x⁺(v⁺); x^–(v^–) for all u⁺, v⁺ ∈ L⁺ and u^–, v^– ∈ L^–. Equating x⁺ and x^– with their corresponding completely prime filters, this means that u⁺; u^– ⊢ v⁺; v^– implies that it is impossible that u⁺ ∈ x⁺, u^– ∈ x^–, v⁺ ∉ x⁺, v^– ∉ x^–. We arrive at our actual definition of a point in a 2-frame.

Definition D. A point in a 2-frame L ≝ (L⁺, L_^–, ⊢) is a pair (x⁺, x^–) where:

• x⁺ is a completely prime filter of elements of L⁺;
• x^– is a completely prime filter of elements of L^–;
• for all u⁺, v⁺ ∈ L⁺ and u^–, v^– ∈ L^– such that u⁺ ∈ x⁺, u^– ∈ x^–, v⁺ ∉ x⁺ and v^– ∉ x^–, u⁺; u^– ⊬ v⁺; v^–.

Let 2pt L be the set of all points of L = (L⁺, L_^–, ⊢), with the following two topologies:

• O⁺2pt L consists of the sets O⁺_u⁺ ≝ {(x⁺, x^–) ∈ 2pt L | u⁺ ∈ x⁺}, where u⁺ ranges over L⁺;
• O^–2pt L consists of the sets O^–_u^– ≝ {(x⁺, x^–) ∈ 2pt L | u^– ∈ x^–}, where u^– ranges over L^–.

Then 2pt L is a bitopological space. You should not be too surprised by the construction if you compare it with the construction dpt L of the June 2025 post. Similar to Proposition A in that post, we have the following. I have deferred the proof to the Appendix, since you might want to skip over it, especially if you are already familiar with the June 2025 post.

Proposition E. For every bitopological space X, there is a bicontinuous map η_X : X → 2pt 2OX defined by η_X(x) ≝ (η⁺_X(x), η^–_X(x)) where η⁺_X(x) ≝ {U⁺ ∈ O⁺X | x ∈ U⁺} and η^–_X(x) ≝ {U^– ∈ O^–X | x ∈ U^–}).

We have defined 2pt on objects (2-frames), and we can also define 2pt φ : 2pt K → 2pt L for every 2-frame homomorphism φ ≝ (φ⁺, φ^–) : L → K, where L ≝ (L⁺, L_^–, ⊢) and K ≝ (K⁺, K_^–, ⊩), by letting 2pt φ (x⁺, x^–) ≝ ((φ⁺)^–1 (x⁺), (φ^–)^–1 (x^–)) for every point (x⁺, x^–) of K. As with Proposition E, we defer the proof of the following to the appendix.

Proposition F.  2pt is a functor from 2Frm^op to biTop.

Theorem G. For every bitopological space X, for every 2-frame L ≝ (L⁺, L_^–, ⊢), for every bicontinuous map f : X → 2pt L, there is a unique 2-frame homomorphism f^! : L → 2OX such that 2pt f^! o η_X = f. Hence there is an adjunction 2O ⊣ 2pt between biTop and 2Frm^op, with unit η as defined in Proposition E.

2-sobrification

Much like the sobrification SX of a topological space X is a practical, naturally homeomorphic copy of pt O X (see Section 8.2 in the book), we will define the 2-sobrification 2SX of a bitopological space X as a naturally isomorphic copy of 2pt 2O X. As in the June 2025 post, we will write S⁺X for the sobrification of X with its first topology O⁺X and S^–X for the sobrification of X with its second topology O^–X.

The points of S⁺X are the irreducible closed subsets C⁺ of X with the topology O⁺X. Each such C⁺ defines a completely prime filter F⁺, which consists of all U⁺ ∈ O⁺X that intersect C⁺. Conversely, every completely prime filter F⁺ defines an irreducible closed subset C⁺ of X with the topology O⁺X, which is the complement of the union of all the U⁺ ∈ O⁺X that are not in F⁺. The two constructions are inverse of each other. (Similarly with minus signs.)

The points of 2pt 2O X are pairs (F⁺, F^–) where:

• F⁺ is a completely prime filter of elements of O⁺X;
• F^– is a completely prime filter of elements of O^–X;
• for all U⁺, V⁺ ∈ O⁺X and U^–, V^– ∈ O⁺X such that U⁺ ∈ F⁺, U^– ∈ F^–, V⁺ ∉ F⁺ and V^– ∉ F^–, U⁺ ⋂ U^– ⊊ V⁺ ∪ V^–.

Isomorphically, we can then represent the points of 2pt 2O X as pairs (C⁺, C^–) where:

• C⁺ ∈ S⁺X;
• C^– ∈ S^–X;
• for all U⁺, V⁺ ∈ O⁺X and U^–, V^– ∈ O⁺X such that U⁺ intersects C⁺, U^– intersects C^–, V⁺ is disjoint from C⁺ and V^– is disjoint from C^–, U⁺ ⋂ U^– ⊊ V⁺ ∪ V^–.

Taking the complement of C⁺ for V⁺ and the complement of C^– for V^– in the last condition, we obtain that for all U⁺ ∈ O⁺X and U^– ∈ O⁺X, if U⁺ intersects C⁺ and U^– intersects C^–, then U⁺ ⋂ U^– intersects C⁺ ⋂ C^–. Hence we define:

Definition H. The 2-sobrification 2SX 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.

Those are really topologies, not just bases or subbases of a topology, for the same reason as the analogous phenomenon in the definition of sobrifications: ♢⁺ commutes with arbitrary unions, and with finite intersections because every C⁺∈ S⁺X is irreducible, and similarly with ♢^–.

We will leave the fact that 2SX is isomorphic to 2pt 2O X as an exercise. The isomorphism is the bicontinuous map f : 2pt 2O X → 2SX that maps every pair (F⁺, F^–) of completely prime filters satisfying the condition “U⁺ ∈ F⁺, U^– ∈ F^–, V⁺ ∉ F⁺ and V^– ∉ F^– imply U⁺ ⋂ U^– ⊊ V⁺ ∪ V^–” to (C⁺, C^–) where C⁺ is the complement of the union of all the U⁺ that are not in F⁺, and similarly with minus signs. Then f is injective, and in order to show that it is surjective, you need to show that if C⁺ ∈ S⁺X and C^– ∈ S^–X satisfy the condition “U⁺ intersects C⁺ and U^– intersects C^– imply U⁺ ⋂ U^– intersects C⁺ ⋂ C^–“, then it also satisfies the condition “U⁺ intersects C⁺, U^– intersects C^–, V⁺ is disjoint from C⁺ and V^– is disjoint from C^– imply U⁺ ⋂ U^– ⊊ V⁺ ∪ V^–“. Finally, f^–1 maps O⁺_U⁺ to ♢⁺ U⁺ and O^–_U^– to ♢^– U^–, making it an order-isomorphism.

Let me equate 2SX with 2pt 2O X in what follows. In particular, this turns the unit η_X of the adjunction 2O ⊣ 2pt into a map η_X : X → 2SX. Explicitly, for every x ∈ X, η_X (x) = (↓⁺x, ↓^–x), where ↓⁺ is downward closure with respect to the specialization preordering ≤⁺ of O⁺X and ↓^– is downward closure with respect to the specialization preordering ≤^– of O^–X. (Let us check it: the image of x should be (C⁺, C^–), where C⁺ is the complement of the largest set in the complement of η⁺_X(x) ≝ {U⁺ ∈ O⁺X | x ∈ U⁺}, and similarly with C^–. Hence C⁺ is the smallest O⁺X-closed set that contains x, namely its closure, which happens to be its downward closure in the associated specialization preordering ≤⁺. We reason similarly with minus signs.)

Because 2O ⊣ 2pt is an adjunction, 2S is a monad on biTop, and η is its unit.

Proposition I. For every bitopological space X, the map ♢⁺ is an order-isomorphism of O⁺X onto O⁺ 2SX, and the map ♢^– is an order-isomorphism of O^–X onto O^– 2SX.

Once again, the proof is in the appendix, as for the next lemma.

Lemma J. For every bitopological space X, for every U⁺ ∈ O⁺X, (η_X)^–1 (♢⁺U⁺) = U⁺; for every U^– ∈ O^–X, (η_X)^–1 (♢^–U^–) = U^–.

Fact 8.2.24 of the book states that, relative to the O ⊣ pt adjunction, the unit at a space X is bijective if and only if it is a homeomorphism, and that this is equivalent to X being sober. We had a similar phenomenon with d-sobriety in the June 2025 post, and we use the resulting condition as a definition of the analogous notion of 2-sobriety.

Proposition K. 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 (namely, of irreducible closed subsets of X with its first and second topologies respectively) 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 T₀ (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.

Condition (b) differs from the similar condition for d-sober spaces (see the June 2025 post): there, condition (b) required that if U⁺ intersects C⁺ and U^– intersects C^–, then U⁺ and U^– intersect. Condition (a) is redundant: it follows from condition (b) by taking U⁺ and U^– equal to X. We left it to make the parallel with d-sobriety more obvious.

The 2-sobrification monad is idempotent

This is similar to the fact that S or the monad dS of the June 2025 post is idempotent. I will point you to that post for the notion of an idempotent, and I will be content with asserting that this means that the 2-sobrification of any bitopological space is 2-sober. Just like in that post, we have the following, which is, once again, proved in the appendix.

Theorem L. For every 2-frame L ≝ (L⁺, L_^–, ⊢), 2pt L is 2-sober. The 2O ⊣ 2pt adjunction is idempotent, so the monad dS is idempotent on biTop.

Free 2-frames

Given any set G, whose elements are called the generators, there is a free frame FG on G. Intuitively, the elements of FG represent open sets, obtained as arbitrary unions of finite intersections of the generators, seen as subbasic open sets. One way of building the elements of FG is to describe them as formulas, written as (possibly infinite) disjunctions of finite conjunctions of generators. The ordering between formulas is meant to encode the inequalities that have to be true, such as u≤u or u ⋀ v ≤ v, but no other.

Of course, there is a formal definition: FG (if it exists, and we will show that it does) is a frame, there is a function i_G : G → FG, and for every frame L, every function f : G → L extends to a unique frame homomorphism f^! : FG → L, where extending means that f^! o i_G = f. In other words, F is the left adjoint to the forgetful functor from frames to sets, which sends every frame to its underlying set of elements (forgetting about the frame structure) and every frame homomorphism to itself, seen as a mere function.

The free frame FG exists for every set G, see 2.4 in Chapter IV of [3] for example. Let me briefly describe how it is built.

• We first form P_fin(G), the set of finite subsets of G: one should think of an element {g₁, …, g_n} of P_fin(G) as a formula g₁ ⋀ … ⋀ g_n, following our intuition described above. Already, this representation encodes that ⋀ is associative, commutative, idempotent with a unit (the empty set).
  P_fin(G) is naturally ordered by inclusion, but we will instead consider the opposite order P_fin^op(G), whose ordering is reverse inclusion. The point is that the formal conjunction (intersection) g₁ ⋀ … ⋀ g_n is less than or equal to (included in) g’₁ ⋀ … ⋀ g’_m if every g’_j is above some g_i; we don’t want any additional cases, hence we want to make that ‘if’ and ‘if and only if’; and finally, the only case where we can assert that g’_j is above some g_i is when g’_j = g_i. Hence we want to declare g₁ ⋀ … ⋀ g_n less than or equal to g’₁ ⋀ … ⋀ g’_m if and only if {g₁, …, g_n} ⊇ {g’₁, …, g’_m}, whence our use of reverse inclusion.
• Given any poset P, let DP be the set of downwards-closed subsets of P, ordered by inclusion. This is a completely distributive lattice, where infima are intersections and suprema are unions. In particular, it is a frame.
• We define FG as DP_fin^op(G). The intuition is that given any family (p_i)_{i ∈ I} of elements of P_fin(G), seen as formal conjunctions (or formal intersections) of generators, the downwards-closed set ↓{p_i | i ∈ I} encodes the disjunction (or union) of the p_is.
  The map i_G sends every generator g ∈ G to ↓{{g}} = {p ∈ P_fin(G) | g ∈ p}. (Remember that downward closure ↓ is taken with respect to reverse inclusion.)
  We note that every D ∈ DP_fin^op(G) can be written as ∪_{p ∈ D} ⋂_{g ∈ p} i_G(g): for every p ∈ P_fin(G), ⋂_{g ∈ p} i_G(g) = ⋂_{g ∈ p} {p’ ∈ P_fin(G) | g ∈ p’} = {p’ ∈ P_fin(G) | p ⊆ p’}, so ∪_{p ∈ D} ⋂_{g ∈ p} i_G(g) = {p’ ∈ P_fin(G) | p ⊆ p’ for some p ∈ D} = D (since D is downwards-closed with respect to reverse inclusion, hence upwards-closed with respect to ordinary inclusion).
• Given any function f : G → L where L is a frame, if f^! exists then it must map every D ∈ DP_fin^op(G), which we can write as ∪_{p ∈ D} ⋂_{g ∈ p} i_G(g), to ⋁_{p ∈ D} ⋀_{g ∈ p} f(g), and this formula determines f^! uniquely. We define it this way, and we check that f^! is a frame homomorphism, and that f^! o i_G = f, as desired.

In the case of 2-frames, we will build the free 2-frame 2F(G⁺, G^–) on a pair of sets of generators G⁺ and G^–. 2F(G⁺, G^–), if it exists (and it will), is characterized by the following universal property: 2F(G⁺, G^–) should be a 2-frame (Ω⁺, Ω^–, ⊩), there should be a pair of functions i_G⁺ : G⁺ → Ω⁺ and i_G^– : G^– → Ω^–, and for every 2-frame L ≝ (L⁺, L^–, ⊢), every pair of functions f⁺ : G⁺ → L⁺ and f^– : G^– → L^– should extend to a unique 2-frame homomorphism (f^!+, f^!+) : 2F(G⁺, G^–) → L, where extending means that f^!+ o i_G⁺ = f⁺ and f^!– o i_G^– = f^–. In other words, 2F will be left adjoint to the forgetful functor from 2Frm to Set × Set, the category of pairs of sets with pairs of maps between them.

Theorem M. 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^–, ⊩) where D⁺; D^– ⊩ D’⁺; D’^– if and only if D⁺ ⊆ D’⁺ or D^– ⊆ D’^–.

Proof. First, (FG⁺, FG^–, ⊩) is a 2-frame: FG⁺ and FG^– are frames, and it remains to verify the numerous axioms of Definition A. Let us write FG⁺ as Ω⁺ and FG^– as Ω^–, and let us consider arbitrary elements D⁺, D’⁺, etc. of Ω⁺ and D^–, D’^–, etc. of Ω^–.

1. the set _; D^– ⊩ D’⁺; D’^– ≝ {D⁺ ∈ Ω⁺ | D⁺; D^– ⊩ D’⁺; D’^–} is downwards-closed and closed under arbitrary suprema in L⁺: indeed, this set is equal to Ω⁺ if D^– ⊆ D’^–, and to the downward-closure of D’⁺ otherwise;
2. the set D⁺; _ ⊩ D’⁺; D’^– ≝ {D^– ∈ Ω^– | D⁺; D^– ⊩ D’⁺; D’^–} is downwards-closed and closed under arbitrary suprema in L^–: similar;
3. the set D⁺; D^– ⊩ _; D’^– ≝ {D’⁺ ∈ Ω⁺ | D⁺; D^– ⊩ D’⁺; D’^–} is upwards-closed and closed under finite infima in L⁺: this is equal to Ω⁺ if D^– ⊆ D’^–, and to the upward-closure of D⁺ otherwise;
4. the set D⁺; D^– ⊩ D’⁺; _ ≝ {D’^– ∈ Ω^– | D⁺; D^– ⊩ D’⁺; D’^–} is upwards-closed and closed under finite infima in L^–: similar:
5. (axiom⁺) if D⁺ ⊆ D’⁺ then D⁺; D^– ⊩ D’⁺; D’^–: obvious; in fact, ⊩ is the smallest relation satisfying (axiom⁺) and (axiom^–);
6. (axiom^–) if D^– ⊆ D‘^– then D⁺; D^– ⊩ D’⁺; D’^–: obvious;
7. if D⁺; ⊤ ⊩ D’⁺; ⊥ then D⁺ ⊆ D’⁺: because ⊤ = Ω^– is not included in ⊥ = ∅;
8. if ⊤; D^– ⊩ ⊥; D’^– then D^– ⊆ D’^–: because ⊤ = Ω⁺ is not included in ⊥ = ∅;
9. (cut⁺) if D₁⁺; D₁^– ⊩ D’₁⁺; D’₁^– and D₂⁺; D₂^– ⊩ D’₂⁺; D’₂^–, and if D’₁⁺ ⊆ D₂⁺, then D₁⁺; D₁^– ⋂ D₂^– ⊩ D’₂⁺; D’₁^– ∪ D’₂^–: this requires a case analysis:
   • if D₁⁺ ⊆ D’₁⁺ and D₂⁺ ⊆ D’₂⁺, then D₁⁺ ⊆ D’₁⁺ ⊆ D₂⁺ ⊆ D’₂⁺;
   • if D₁^– ⊆ D’₁^– then D₁^– ⋂ D₂^– ⊆ D’₁^– ∪ D’₂^–;
   • if D₂^– ⊆ D’₂^– then D₁^– ⋂ D₂^– ⊆ D’₁^– ∪ D’₂^–;
10. (cut^–) if D₁⁺; D₁^– ⊩ D’₁⁺; D’₁^– and D₂⁺; D₂^– ⊩ D’₂⁺; D’₂^–, and if D’₁^– ⊆ D’₂^–, then D₁⁺ ⋂ D₂⁺; D₁^– ⊩ D’₁⁺ ∪ D’₂⁺; D’₂^–: similar.

Second, the maps i_G⁺ and i_G^– are already defined, from the theory of free frames: i_G⁺(g⁺) = {p⁺ ∈ P_fin(G⁺) | g⁺ ∈ p⁺} and i_G^–(g^–) = {p^– ∈ P_fin(G^–) | g^– ∈ p^–}.

Let L ≝ (L⁺, L^–, ⊢) be a 2-frame, and let f⁺ : G⁺ → L⁺ and f^– : G^– → L^– be two functions. There are unique frame homomorphisms f^!+ : FG⁺ → L⁺ and f^!– : FG^– → L^– that extend f⁺ and f^–, in the sense that f^!+ o i_G⁺ = f⁺ and f^!– o i_G^– = f^–. It remains to show that (f^!+, f^!+) is a 2-frame homomorphism, namely that D⁺; D^– ⊩ D’⁺; D’^– entails f^!+(D⁺); f^!–(D^–) ⊢ f^!+(D’⁺); f^!–(D’^–) for all D⁺, D⁺ ∈ Ω⁺ and D’^–, D’^– ∈ Ω^–. The assumption D⁺; D^– ⊩ D’⁺; D’^– means that D⁺ ⊆ D’⁺ or D^– ⊆ D’^–.

• If D⁺ ⊆ D’⁺ then f^!+(D⁺) ≤ f^!+(D’⁺) in L⁺, since f^!+ is a frame homomorphism and is in particular monotonic. By property (axiom⁺) of L⁺, f^!+(D⁺); f^!–(D^–) ⊢ f^!+(D’⁺); f^!–(D’^–).
• If D^– ⊆ D’^–, we reason similarly, using (axiom^–). ☐

My secret plan

You might have wondered why I have decided to introduce yet another Stone duality for bitopological spaces. I had already presented d-frames [1, 2], and there are also Banaschewski and Brümmer’s biframes [3], which I have not talked about. Are 2-frames an improvement?

Well, I certainly feel they have a more streamlined presentation than d-frames. What I have in the back of my mind, though, is a plan to revisit a proposal I made earlier of a Stone duality for preordered topological spaces (see the January 2026 post): this one was based on an analogue of d-frames, which I called ad-frames, but conversations with Nesta van der Schaaf convinced me that there were important relations that one could not express with ad-frames, typically of the form U⁺ ⋂ U^– ⊆ V⁺, or U⁺ ⋂ U^– ⊆ V^– (now with the + sets open and the – sets upwards-closed with respect to the given preordering). If you are brave enough, you should be able to realize that we obtain a Stone duality for preordered topological spaces by replaying everything in this post, replacing frames on the – side by completely distributive lattices and frame homomorphisms on the same side by complete lattice homomorphisms, as well as completely prime filters by completely prime complete filters, and so on; and everything will work as smoothly. I will talk about this next time.

You may also have noticed that I am starting to self-plagiarize. A lot of what I wrote this month was copied from previous posts on ad-frames, modifying what had to be modified. This allowed me to write this post a bit faster than other posts (two and half days over a week-end, compared to 3 to 5 days for other posts). That is definitely not commendable conduct far as publications are concerned, but first, this blog is not meant to be a scientific publication (although it may come close), and second, it is more and more difficult for me to find new things to say and to find the time to explain them.

I have already said something of this ilk earlier. Almost two years ago, I said that I would “start slowing down a bit”. I am more busy than ever, and it feels more and more of a miracle that I can post something new each month. You can see my strategy of self-plagiarism as a disguised attempt to slow down. This doubles down as a good way of forcing me to think about the scientific questions I have with Nesta van der Schaaf: I woud not have made any progress on these question without an urge to say something on this blog!

1. Achim Jung and M. Andrew Moshier. A Hofmann-Mislove theorem for bitopological spaces.  Electronic Notes in Theoretical Computer Science 173:159-175, 2007. Available from https://achimjungbham.github.io/pub/papers/HM-journal.pdf
2. Tomáš Jakl. d-Frames as algebraic duals of bitopological spaces, Ph.D. thesis, Charles University and University of Birmingham, 2018.
3. Jorge Picado and Aleš Pultr. Frames and locales — topology without points. Birkhäuser, 2010.
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.

Appendix

Proof of Proposition E. (Reminder: given a bitopological space X, we claim that η_X : X → 2pt 2OX defined by η_X(x) ≝ (η⁺_X(x), η^–_X(x)) where η⁺_X(x) ≝ {U⁺ ∈ O⁺X | x ∈ U⁺} and η^–_X(x) ≝ {U^– ∈ O^–X | x ∈ U^–} is well-defined and bicontinuous).

We must first show that η_X(x), as it is defined, is a point of the 2-frame 2OX. Just like with the O ⊣ pt adjunctionof Section 8.1 of the book, η⁺_X(x) and η^–_X(x) are completely prime filters of O⁺X and of O^–X respectively. Now let us consider U⁺, V⁺ ∈ O⁺X and U^–, V^– ∈ O^–X such that U⁺ ∈ η⁺_X(x), U^– ∈ η^–_X(x), V⁺ ∉ η⁺_X(x) and V^– ∉ η^–_X(x); we wish to show that U⁺; U^– ⊬_X V⁺; V^–. Our four assumptions are that x ∈ U⁺, x ∈ U^–, x ∉ V⁺ and x ∉ V^–. Therefore x is in U⁺ ∩ U^– but not in V⁺ ∪ V^–.  This shows that U⁺ ∩ U^– is not included in V⁺ ∪ V^–, namely that U⁺; U^– ⊬_X V⁺; V^–, as desired.

Next, we must show that η_X is bicontinuous, namely that η_X is continuous from X with the O⁺X topology to 2pt 2OX with the O⁺2pt 2OX topology, and similarly with minus signs. For every U⁺ ∈ O⁺X, the inverse image of O⁺_U⁺ by η_X is the collection of points x ∈ X such that η_X(x) = (η⁺_X(x), η^–_X(x)) is in O⁺_U⁺ = {(x⁺, x^–) ∈ 2pt L | U⁺ ∈ x⁺}, namely such that U⁺ ∈ η⁺_X(x), equivalently such that x ∈ U⁺; so that is the set U⁺. We reason similarly with minus signs. ☐

Proof of Proposition F. (Reminder: this says that 2pt is a functor from 2Frm^op to biTop.)

We recall that for every 2-frame homomorphism φ ≝ (φ⁺, φ^–) : L → K, where L ≝ (L⁺, L_^–, ⊢) and K ≝ (K⁺, K_^–, ⊩), we define 2pt φ (x⁺, x^–) as ((φ⁺)^–1 (x⁺), (φ^–)^–1 (x^–)) for every point (x⁺, x^–) of K.

We first verify that 2pt φ maps points (x⁺, x^–) of K of points of L. The sets (φ⁺)^–1 (x⁺) and (φ^–)^–1 (x^–) are completely prime filters, as in the case of the O ⊣ pt adjunction of Section 8.1 of the book. We need to show that for all u⁺, v⁺ ∈ L⁺ and u^–, v^– ∈ L^– such that u⁺ ∈ (φ⁺)^–1 (x⁺), u^– ∈ (φ^–)^–1 (x^–), v⁺ ∉ (φ⁺)^–1 (x⁺) and v^– ∉ (φ^–)^–1 (x^–), u⁺; u^– ⊬ v⁺; v^–. Our four assumptions are that φ⁺(u⁺) ∈ x⁺, φ^–(u^–) ∈ x^–, φ⁺(v⁺) ∉ x⁺ and φ^–(v^–) ∉ x^–. Since (x⁺, x^–) is a point of K, φ⁺(u⁺); φ^–(u^–) ⊮ φ⁺(v⁺); φ^–(v^–). Now φ = (φ⁺, φ^–) is a 2-frame homomorphism, hence preserves the 4-ary sequent relation: if we had u⁺; u^– ⊢ v⁺; v^–, it would follow that φ⁺(u⁺); φ^–(u^–) ⊩ φ⁺(v⁺); φ^–(v^–). Hence u⁺; u^– ⊬ v⁺; v^–, as desired.

Next, we need to show that 2pt φ is bicontinuous. For every v⁺ ∈ L⁺, the inverse image of O⁺_v⁺ = {(y⁺, y^–) ∈ 2pt L | v⁺ ∈ y⁺} by 2pt φ is the collection of points (x⁺, x^–) of K such that v⁺ ∈ (φ⁺)^–1 (x⁺), namely such that φ⁺ (v⁺) ∈ x⁺; that is O⁺_{φ⁺ (v⁺)}. Similarly with minus signs.

Finally, the fact that dpt maps identity morphisms to identity maps and preserves composition is easy. ☐

Proof of Theorem G. (Reminder: given a bitopological space X, a 2-frame L ≝ (L⁺, L_^–, ⊢), and a bicontinuous map f : X → 2pt L, we claim that there is a unique 2-frame homomorphism f^! : L → 2OX such that 2pt f^! o η_X = f.)

For every x ∈ X, f (x) is a point of L, which is a pair that we will write as (f⁺ (x), f^–(x)); f⁺ (x) is a point (a completely prime filter) of L⁺, and f^– (x) is a point (a completely prime filter) of L^–.

The proof proceeds almost exactly as with O ⊣ pt (see Theorem 8.1.26 in the book). If f^!exists, and writing it as the pair of two frame homomorphisms f^!+ and f^!–, then for every x ∈ X, f (x) must be equal to 2pt f^! (η_X (x)) = ((f^!+)^–1 (η⁺_X(x)), (f^!–)^–1 (η^–_X(x))) = ({v⁺ ∈ L⁺ | x ∈ f^!+(v⁺)}, {v^– ∈ L^– | x ∈ f^!– (v^–)}). Looking at the first components, f⁺ (x) = {v⁺ ∈ L⁺ | x ∈ f^!+ (v⁺)} for every x ∈ X; so, for every x ∈ X, for every v⁺ ∈ L⁺, v⁺ ∈ f⁺ (x) if and only if x ∈ f^!+ (v⁺); therefore, for every v⁺ ∈ L⁺, f^!+ (v⁺) must be equal to {x ∈ X | v⁺ ∈ f⁺ (x)}. Similarly, for every v^– ∈ L^–, f^!– (v^–) must be equal to {x ∈ X | v^– ∈ f^– (x)}. This shows that f^!+ and f^!– are determined uniquely, hence also f^!.

We now define f^!+ (v⁺) as {x ∈ X | v⁺ ∈ f⁺ (x)} for every v⁺ ∈ L⁺ and f^!– (v^–) as {x ∈ X | v^– ∈ f^–(x)} for every v^– ∈ L^–, as we are forced to. Since v⁺ ∈ f⁺ (x) if and only if f (x) ∈ O⁺_v⁺ if and only if x ∈ f^–1 (O⁺_v⁺), and since f is bicontinuous, f^!+ (v⁺) = f^–1 (O⁺_v⁺) is in O⁺X; similarly, f^!– (v^–) = f^–1 (O^–_v^–) is in O^–X. Let us verify that the two maps f^!+ and f^!– are frame homomorphisms. We deal with the case of f^!+ only; let us recall that O⁺_v⁺ ≝ {(y⁺, y^–) ∈ 2pt L | v⁺ ∈ y⁺}:

• If v⁺ = ⊤, then O⁺_v⁺ = {(y⁺, y^–) ∈ 2pt L | ⊤ ∈ y⁺} is the whole of 2pt L, since ⊤ belongs to every completely prime filter y⁺; then f^!+ (v⁺) = f^–1 (dpt L) is the whole of X, which is the top element of O⁺X.
• Binary infima. For all v⁺, v’⁺ ∈ L⁺, the elements of O⁺_v⁺ ⋂ O⁺_v’⁺ are the points (y⁺, y^–) of L such that both v⁺ and v’⁺ are in y⁺; since y⁺ is a filter, that is equivalent to the fact that v⁺ ⋀ v’⁺ is in y⁺. In other words, the elements of O⁺_v⁺ ⋂ O⁺_v’⁺ are the same as those of O⁺_{v⁺ ⋀ v’⁺}. Then f^!+ (v⁺ ⋀ v’⁺) = f^–1 (O⁺_{v⁺ ⋀ v’⁺}) = f^–1 (O⁺_v⁺ ⋂ O⁺_v’⁺) = f^–1 (O⁺_v⁺) ⋂ f^–1 (O⁺_v’⁺) is the infimum of f^!+ (v⁺) and of f^!+ (v’⁺).
• Arbitrary suprema. Let (v_i⁺)_i ∈ I be an arbitrary family in L⁺, with supremum v⁺. The elements of O⁺_v⁺ are the points (y⁺, y^–) of L such that v⁺ ∈ y⁺. If so, then some v_i⁺ is in y⁺, because y⁺ is completely prime; conversely, if some v_i⁺ is in y⁺, then v⁺ is, too, since y⁺ is upwards-closed. Hence the elements of O⁺_v⁺ are the points (y⁺, y^–) of L such that v_i⁺ is in y⁺ for some i ∈ I. In other words, O⁺_v⁺ = ∪_i ∈ I O⁺_vi⁺. Then f^!+ (v⁺) = f^–1 (O⁺_v⁺) = f^–1(∪_i ∈ I O⁺_vi⁺) = ∪_i ∈ I f^–1 (O⁺_vi⁺) = ∪_i ∈ I f^!+ (v_i⁺), showing that f^!+ preserves suprema.

We can now define f^! as the pair of frame homomorphisms f^!+ and f^!–. Let us check that f^!preserves the 4-ary sequent relation. Let u⁺; u^– ⊢ v⁺; v^– in L. We wish to show that f^!+(u⁺); f^!–(u^–) ⊢_X f^!+(v⁺); f^!–(v^–), namely that f^!+(u⁺) ⋂ f^!–(u^–) ⊆ f^!+(v⁺) ∪ f^!–(v^–). If that were not the case, there would be a point x in X that is in f^!+(u⁺), in f^!–(u^–), but not in f^!+(v⁺) and not in f^!–(v^–). Hence u⁺ ∈ f⁺ (x), u^– ∈ f^– (x), v⁺ ∉ f⁺ (x) and v^– ∉ f^– (x). Since (f⁺ (x), f^– (x)) = f (x) is a point of L, the latter would entail that u⁺; u^– ⊬ v⁺; v^–, and we have reached a contradiction.

Finally, for every x ∈ X, 2pt f^! (η_X (x)) = ((f^!+)^–1 (η⁺_X(x)), (f^!–)^–1 (η^–_X(x))) = ({v⁺ ∈ L⁺ | x ∈ f^!+(v⁺)}, {v^– ∈ L^– | x ∈ f^!– (v^–)}) (by definition of η_X) = ({v⁺ ∈ L⁺ | v⁺ ∈ f⁺ (x)}, {v^– ∈ L^– | v^– ∈ f^–(x)}) (by definition of f^!) = (f⁺ (x),  f^– (x)) = f (x). ☐

Proof of Proposition I. (Namely, the map ♢⁺ is an order-isomorphism of O⁺X onto O⁺ 2SX, and the map ♢^– is an order-isomorphism of O^–X onto O^– 2SX.)

♢⁺ is surjective by definition of O⁺ 2SX: every element of O⁺ 2SX is of the form ♢⁺ U⁺ for some U⁺ ∈ O⁺X, see Definition H. If U⁺ ⊆ V⁺, then every point (C⁺, C^–) ∈ 2SX such that U⁺ intersects C⁺ is also such that V⁺ intersects C⁺, so ♢⁺ is monotonic. It remains to show that ♢⁺ is order-reflecting, namely that ♢⁺U⁺ ⊆ ♢⁺V⁺ implies U⁺ ⊆ V⁺, where U⁺ and V⁺ are arbitrary elements of O⁺X.

Since ♢⁺U⁺ ⊆ ♢⁺V⁺, every point (C⁺, C^–) ∈ 2SX such that U⁺ intersects C⁺ is also such that V⁺ intersects C⁺. Let x be any point in U⁺. Then let (C⁺, C^–) ≝ η_X (x) = (↓⁺x, ↓^–x). U⁺ intersects C⁺ (at x), so by assumption V⁺ intersects C⁺ = ↓⁺x. Since V⁺ is upwards-closed with respect to ≤⁺, x must be in V⁺. Since x is arbitrary in U⁺, U⁺ ⊆ V⁺.

Similarly with minus signs. ☐

Proof of Lemma J. (Namely, for every U⁺ ∈ O⁺X, (η_X)^–1 (♢⁺U⁺) = U⁺; for every U^– ∈ O^–X, (η_X)^–1 (♢^–U^–) = U^–.)

Proof. (η_X)^–1 (♢⁺U⁺) is the collection of points x of X such that ↓⁺x intersects U⁺. Since U⁺ is upwards-closed with respect to ≤⁺, the latter condition is equivalent to: x ∈ U⁺. Hence (η_X)^–1 (♢⁺U⁺) = U⁺. We reason similarly in order to show that (η_X)^–1 (♢^–U^–) = U^–. ☐

Proof of Proposition K. (That the following are equivalent:

1. η_X : X → 2SX is bijective;
2. η_X : X → 2SX is an isomorphism in biTop;
3. every irreducible pair is equal to (↓⁺x, ↓^–x) for a unique point x of X. We recall that an irreducible pair is a pair (C⁺, C^–) ∈ S⁺X × S^–X such that: (a) C⁺ and C^– intersect and (b) 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 T₀ and every irreducible pair is equal to (↓⁺x, ↓^–x) for some point x of X.)

Condition 3 is simply a rephrasing of condition 1, hence is trivially equivalent to it.

Clearly, condition 2 implies condition 1. Let us show that condition 1 implies condition 2. We assume that η_X is bijective. Let g be its inverse. We need to show that g is bicontinuous, namely that g is continuous from 2SX with its O⁺ 2SX topology to X with its O⁺X topology, and from 2SX with its O^– 2SX topology to X with its O^–X topology. By Lemma J, for every U⁺ ∈ O⁺X, (η_X)^–1 (♢⁺U⁺) = U⁺; hence g^–1 (U⁺) = ♢⁺U⁺. Similarly, g^–1 (U^–) = ♢^–U^–, proving the claim.

Condition 3 implies condition 4: every irreducible pair is equal to (↓⁺x, ↓^–x) for some point x of X, and it just so happens that this point is unique. Additionally, for every point x of X, (↓⁺x, ↓^–x) = η_X(x) is an irreducible pair, so for every point y of X, if (↓⁺x, ↓^–x) = (↓⁺y, ↓^–y) then x=y. Let ≤ be the intersection of ≤⁺ and ≤^–. If x≤y and y≤x, then x ≤⁺ y, y ≤⁺ x, x ≤^– y and, y ≤^– x, so (↓⁺x, ↓^–x) = (↓⁺y, ↓^–y) and therefore x=y. It follows that X is pairwise T₀.

Conversely, condition 4 implies condition 3. Every irreducible pair is equal to (↓⁺x, ↓^–x) for some point x of X, and if there were another one (↓⁺y, ↓^–y), then we would have x ≤⁺ y, y ≤⁺ x, x ≤^– y and, y ≤^– x, so x≤y and y≤x, and therefore x=y since X is pairwise T₀. Therefore (↓⁺x, ↓^–x) = (↓⁺y, ↓^–y). ☐

Proof of Theorem L. (This says that for every 2-frame L ≝ (L⁺, L_^–, ⊢), 2pt L is 2-sober.)

Let X ≝ 2pt L. Its first topology O⁺2pt L consists of the sets O⁺_u⁺ ≝ {(x⁺, x^–) ∈ 2pt L | u⁺ ∈ x⁺}, where u⁺ ranges over L⁺. We claim that the specialization preordering ≤⁺ of X with its first topology is given by (x⁺, x^–) ≤⁺ (y⁺, y^–) if and only if x⁺ ⊆ y⁺. Indeed, (x⁺, x^–) ≤⁺ (y⁺, y^–) if and only if for every u⁺ ∈ L⁺, if (x⁺, x^–) ∈ O⁺_u⁺ then (y⁺, y^–) ∈ O⁺_u⁺; but (x⁺, x^–) ∈ O⁺_u⁺ is equivalent to u⁺ ∈ x⁺ and (y⁺, y^–) ∈ O⁺_u⁺ is equivalent to u⁺ ∈ y⁺, so (x⁺, x^–) ≤⁺ (y⁺, y^–) if and only if every u⁺ ∈ L⁺ that is in x⁺ is in y⁺.

Similarly, the specialization preordering ≤^– of X with its second topology if given by (x⁺, x^–) ≤^– (y⁺, y^–) if and only if x^– ⊆ y^–. The intersection of ≤⁺ and ≤^– is then the product ⊆ × ⊆, which is antisymmetric. Hence X is pairwise T₀.

Using Proposition K, it remains to show that every irreducible pair (C⁺, C^–) ∈ S⁺X × S^–X is of the form (↓⁺z, ↓^–z) for some z ∈ X. Since X = 2pt L, we will need to build z as a pair (z⁺, z^–) satisfying certain properties. Also, since (C⁺, C^–) is an irreducible pair, we know that: C⁺ is irreducible closed with respect to O⁺dpt L, C^– is irreducible closed with respect to O^–dpt L, (a) C⁺ and C^– intersect and (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^–.

We define z⁺ as the union ∪{x⁺ | (x⁺, x^–) ∈ C⁺}, and similarly z^– as the union ∪{y^– | (y⁺, y^–) ∈ C^–}. We notice that those unions make sense: for each (x⁺, x^–) ∈ C⁺, x⁺ is a subset of L⁺ (even a completely prime filter of elements of L⁺), and similarly with minus signs.

Claim L.1. z⁺ is a completely prime filter of elements of L⁺, z^– is a completely prime filter of elements of L^–.

Proof. This is exactly as for Claim J.1 in the June 2025 post, with no change whatsoever.

We only prove the claim about z⁺. The claim about z^– is entirely similar. Since C⁺ is irreducible (and closed, namely an element of S⁺X), it is non-empty, so it contains a point (x⁺, x^–). Since x⁺ is a (completely prime) filter of elements of L⁺, it contains the top element of L⁺. Then x⁺ ⊆ z⁺ by definition of z⁺, so z⁺ also contains the top element of L⁺. Also, z⁺ is a union of (completely prime) filters x⁺, which are all upwards-closed in L⁺, so z⁺ is also upwards-closed in L⁺.

Showing that z⁺ is closed under binary infima taken in L⁺ is a bit more complicated. Let u⁺, v⁺ be two elements of z⁺. By definition of z⁺, u⁺ ∈ x⁺ for some point (x⁺, x^–) ∈ C⁺, and v⁺ ∈ y⁺ for some point (y⁺, y^–) ∈ C⁺. We rewrite u⁺ ∈ x⁺ as (x⁺, x^–) ∈ O⁺_u⁺. Similarly, v⁺ ∈ y⁺ means that (y⁺, y^–) ∈ O⁺_v⁺. Hence C⁺ intersects both O⁺_u⁺ and O⁺_v⁺. Since C⁺ is irreducible, C⁺ must intersect their intersection O⁺_u⁺ ⋂ O⁺_v⁺. But O⁺_u⁺ ⋂ O⁺_v⁺ = O⁺_{u⁺⋀ v⁺}, where ⋀ denotes binary infimum in L⁺. Therefore we can find a point (t⁺, t^–) in the intersection of C⁺ and of O⁺_{u⁺⋀ v⁺}. By definition of O⁺_{u⁺⋀ v⁺}, u⁺⋀ v⁺ is in t⁺, and by definition of z⁺ as the union of all the first components of points of C⁺, t⁺ is included in z⁺; so u⁺⋀ v⁺ is in z⁺, which is what we wanted to prove.

Finally, we show that z⁺ is completely prime. Let (u_i⁺)_{i ∈ I} be an arbitrary family in L⁺, with supremum u⁺ in z⁺. By definition of z⁺, u⁺ must be in x⁺ for some (x⁺, x^–) ∈ C⁺. Since x⁺ is completely prime, some u_i⁺ is in x⁺, hence in the larger set z⁺. (End of Claim L.1. ☐)

Claim L.2. (z⁺, z^–) is in 2pt L.

Proof. Claim L.1 says that z⁺ is a point of L⁺ and that z^– is a point of L^–. It remains to show that for all u⁺, v⁺ ∈ L⁺ and u^–, v^– ∈ L^– such that u⁺ ∈ z⁺, u^– ∈ z^–, v⁺ ∉ z⁺ and v^– ∉ z^–, u⁺; u^– ⊬ v⁺; v^–. Since u⁺ ∈ z⁺, u⁺ ∈ x⁺ for some (x⁺, x^–) ∈ C⁺, and then (x⁺, x^–) is in O⁺_u⁺. Since u^– ∈ z^–, u^– ∈ y^– for some (y⁺, y^–) ∈ C^–, and then (y⁺, y^–) is in O^–_u^–. Hence O⁺_u⁺ intersects C⁺ and O^–_u^– intersects C^–.

We claim O⁺_v⁺ does not intersect C⁺. Otherwise, there would be a point (x⁺, x^–) ∈ C⁺ such that (x⁺, x^–) is in O⁺_v⁺, namely such that v⁺ ∈ x⁺. By definition of z⁺, and since (x⁺, x^–) ∈ C⁺, we would have the inclusion x⁺ ⊆ z⁺. Then we would have v⁺ ∈ z⁺, which is impossible.

Similarly, O^–_v^– does not intersect C^–.

Because (C⁺, C^–) is an irreducible pair, O⁺_u⁺ intersects C⁺, and O^–_u^– intersects C^–, it must be that O⁺_u⁺ ⋂ O^–_u^– intersects C⁺ ⋂ C^–. In other words, there is a point (t⁺, t^–) that is in C⁺, in C^–, such that u⁺ ∈ t⁺ and such that u^– ∈ t^–. We claim that v⁺ ∉ t⁺: otherwise (t⁺, t^–) would be in O⁺_v⁺, contradicting the fact that O⁺_v⁺ does not intersect C⁺. Similarly, v^– ∉ t^–.

We now remember that (t⁺, t^–) is a point (see Definition D). Since u⁺ ∈ t⁺, u^– ∈ t^–, v⁺ ∉ t⁺ and v^– ∉ t^–, by definition of points, we have u⁺; u^– ⊬ v⁺; v^–. (End of Claim L.2. ☐)

Claim J.3. (z⁺, z^–) is in C⁺, and in C^–.

Proof. This is exactly as for Claim J.3 in the June 2025 post, with no change whatsoever.

We will only show that (z⁺, z^–) is in C⁺; the case of C^– is symmetric. By Claim L.2, (z⁺, z^–) is in 2pt L, so we only have to assume that (z⁺, z^–) is not in C⁺ and aim for a contradiction. Since C⁺ is (irreducible) closed in X with the topology O⁺2pt L, its complement is in O⁺2pt L, hence is of the form O⁺_u⁺ for some u⁺ ∈ L⁺. The fact that (z⁺, z^–) is not in C⁺ means that (z⁺, z^–) is in O⁺_u⁺, namely that u⁺ ∈ z⁺. By definition of z⁺, there is a point (x⁺, x^–) ∈ C⁺ such that u⁺ ∈ x⁺. In particular, (x⁺, x^–) ∈ O⁺_u⁺. But O⁺_u⁺ is the complement of C⁺, and therefore (x⁺, x^–) ∈ O⁺_u⁺ contradicts (x⁺, x^–) ∈ C⁺. (End of Claim L.3. ☐)

We can now conclude and show that (C⁺, C^–) = (↓⁺z, ↓^–z) where z ≝ (z⁺, z^–) (a point in 2pt L, by Claim L.2). In order to do so, we show that C⁺ = ↓⁺z; the proof that C^– = ↓^–z is symmetric. By Claim L.3, z = (z⁺, z^–) ∈ C⁺. Since C⁺ is closed with respect to the topology O⁺2pt L, it is downwards-closed in its specialization ordering ≤⁺, so ↓⁺z ⊆ C⁺. Conversely, every point (x⁺, x^–) ∈ C⁺ is such that x⁺ ⊆ z⁺ by definition of z⁺, namely (x⁺, x^–) ≤⁺ (z⁺, z^–). (We remember that ≤⁺ is inclusion on first components.) Therefore C⁺ ⊆ ↓⁺z, and then C⁺ = ↓⁺z. We show that C^– = ↓^–z in a symmetric way. (End of proof of Theorem J. ☐)

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