uniform locale

Uniform Locales


A uniform locale is to a uniform space as a locale is to a topological space.


While an ordinary uniform space is defined directly in terms of subsets, and the underlying topology then constructed secondarily, in the absence of an underlying set it seems more convenient to define a uniform locale as additional structure on a given locale, together with an additional axiom which essentially says “the underlying topology is the same as the one we started with.”

Basic notions

For any EOp(X×X)E\in Op(X\times X) and any sublocale AA of XX, with inclusion map i:AXi:A\to X, we write E[A]E[A] for the image of (i×1) *(E)(i\times 1)^*(E) of A×XA\times X under the projection A×XXA\times X \to X. If AA is overt (such as if AA is an open part of XX and XX is overt, or if excluded middle holds), then E[A]E[A] is an open part of XX, and can equivalently be defined as {VOp(X)Pos(VA)}\bigvee \{ V\in Op(X) \mid Pos(V\cap A) \}, where Pos(W)Pos(W) means “WW is positive”. Otherwise, it is merely a sublocale.

Similarly, if E,FOp(X×X)E,F\in Op(X\times X), we write EFE\circ F for the image of π 23 *(E)π 12 *(F)\pi_{23}^*(E) \cap \pi_{12}^*(F) under the projection π 13:X×X×XX×X\pi_{13}:X\times X\times X\to X\times X. If XX is overt, this is an open part of X×XX\times X; otherwise it is merely a sublocale. We also write E 1E^{-1} for the pullback of EE along the twist map X×XX×XX\times X \cong X\times X.

Covering uniformities

An [open] cover of a locale XX is a collection COp(X)C \subseteq Op(X) of open parts of XX whose join is XX. For covers C iC_i, we define:

  • C 1C_1 refines C 2C_2, written C 1C 2C_1 \prec C_2, if every element of C 1C_1 is \le in some element of C 2C_2.

  • C 1C 2{AB|AC 1,BC 2}C_1 \wedge C_2 \coloneqq \{ A \wedge B \;|\; A \in C_1, B \in C_2 \}; this is also a cover.

  • E C={U×UUC}E_C = \bigcup \{ U\times U \mid U\in C \}, and C[A]=E C[A]C[A] = E_C[A].

  • For AOp(X)A \in Op(X), we write C[A]=E C[A]C[A] = E_C[A] (see above definition). If AA is overt (such as if XX is overt, such as if excluded middle holds), this is equivalent to {BC|AB\bigcup \{ B \in C \;|\; A \cap B is positive }.

  • C *{C[A]|AC}}C^* \coloneqq \{ C[A] \;|\; A \in C\}.

We now define a covering uniformity on a locale XX to be a collection of covers, called uniform covers, such that

  1. There exists a uniform cover; in light of axiom (4), it follows that the cover {X}\{X\} is a uniform cover.

  2. If CC is a uniform cover, there exists a uniform cover CC' such that (C) *C(C')^* \prec C.

  3. If C 1,C 2C_1, C_2 are uniform covers, so is some cover that refines C 1C 2C_1 \wedge C_2. In light of axiom (4), it follows that C 1C 2C_1 \wedge C_2 is a uniform cover.

  4. If CC is a uniform cover and CCC \prec C', then CC' is a uniform cover.

  5. For any open part AOp(X)A\in Op(X), we have

    A={B| a uniform cover C such that C[B]A} A = \bigvee \{ B | \exists \;\text{ a uniform cover }\; C \;\text{ such that }\; C[B] \le A \}

The last condition is the one saying that “the induced topology is again the topology of XX.”; the other conditions correspond precisely to the uniform-cover definition of a uniform topological space.

Entourage uniformities

An entourage uniformity on a locale XX consists of a collection of open parts EOp(X×X)E\in Op(X\times X), called [open] entourages, such that:

  1. There exists an entourage (in light of axiom 4 below, it follows that X×XX\times X is an entourage)

  2. For any entourage EE, there exists an entourage FF such that FFEF\circ F \subseteq E, and an entourage GG such that GE 1G\subseteq E^{-1}. (In light of axiom 4 below, it follows that E 1E^{-1} is itself an entourage.) Note that FFF\circ F is in general only a sublocale (not necessarily open), but we can still ask it to be contained in the open sublocale EE.

  3. If EE and FF are entourages, then so is some open part contained in EFE\cap F (in light of axiom 4 below, it follows that EFE\cap F is itself an entourage)

  4. If EE is an entourage and EFE\subseteq F, then FF is also an entourage.

  5. For any UOp(X)U\in Op(X) we have U={VOp(X)E[V]U for some entourage E}U = \bigcup \{ V\in Op(X) \mid E[V] \subseteq U \text{ for some entourage } E\}.

It is not clear whether these definitions are equivalent. Most references (see below) use only covering uniformities, although Johnstone 89 promises an equivalence to entourage uniformities in a future paper.


This paper developes covering uniformities constructively, and includes citations to several other papers that do it classically:

  • Peter Johnstone, 1989; A constructive theory of uniform locales. I. Uniform covers; General topology and applications, 179–193; Lecture Notes in Pure and Applied Mathematics 134 (1991).

A constructive and predicative theory in the programme of formal topology can be found here:

  • Giovanni Curi?; On the collection of points of a formal space; Annals of Pure and Applied Logic 137 (2006) 1–3, 126–146.

  • Giovanni Curi?; Constructive metrisability in point-free topology; Theoretical Computer Science 305 (2003) 1–3, 85–109.

But we have not read these yet.

Revised on December 18, 2016 03:04:28 by Toby Bartels (