uniform locale

Uniform Locales

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 is positive }\bigvee \{ B \in C \;|\; A \cap B \text{ is positive } \}, where positive is in the sense of positive element.

  • 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. If CC is a uniform cover and CCC \prec C', then CC' is a uniform cover.

  2. The cover {X}\{X\} is a uniform cover and if C 1,C 2C_1, C_2 are uniform covers, then so is C 1C 2C_1 \wedge C_2.

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

  4. The collection of uniform covers is admissible: 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 (Picado and Pultr, Section XII.1.1) is an open part EOp(X×X)E\in Op(X\times X) such that {uOp(X)u×uE}\{u\in Op(X)\mid u\times u\le E\} is an open cover of XX.

An entourage uniformity (Picado and Pultr, Section XII.2.3) on a locale XX is a collection of entourages such that:

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

  2. The open part X×XX\times X is an entourage and if EE and FF are entourages, then so is EFE\cap F.

  3. If EE is an entourage, then so is E 1E^{-1}.

  4. For any entourage EE, there exists an entourage FF such that FFEF\circ F \subseteq E. The sublocale FFF\circ F is not always open, but we can still ask it to be contained in the open sublocale EE.

  5. The collection of uniform entourages is admissible: for any UOp(X)U\in Op(X) we have U={VOp(X)E[V]U for some uniform entourage E}U = \bigvee \{ V\in Op(X) \mid E[V] \subseteq U \text{ for some uniform entourage } E\}.

From entourage uniformities to covering uniformities

Given an entourage EE on a locale LL, we define an open cover U EU_E by setting

U E={xLx×xE}.U_E=\{x\in L\mid x\times x\subset E\}.

Given an entourage uniformity {E i} i\{E_i\}_i, we construct a covering uniformity out of it by taking all open covers VV that are refined by some U E iU_{E_i}.

From covering uniformities to entourage uniformities

Given an open cover UU, we construct an entourage E UE_U by setting $E U= xUx×x.E_U=\bigvee_{x\in U}x\times x.$

Given a covering uniformity {U i} i\{U^i\}_i, we construct an entourage uniformity out of it by taking all entourages EE that contain some E U iE_{U^i}.

Equivalence between covering uniformities and entourage uniformities

Theorem XII.3.3.4 in Picado and Pultr shows that the above correspondence is bijective. Furthermore, the categories of entourage uniform locales and covering uniform locales are equivalent (Corollary XII.3.4.3 in the cited book). However, since their book uses classical logic throughout, it is not entirely clear whether the same equivalence holds constructively.



A locale admits a uniformity if and only if it is completely regular (\cite[Theorem 2.8.2]{PP}).

Fine uniformity

Uniformities are closed under unions, so any completely regular locale admits a largest uniformity, the fine uniformity.

The fine uniformity consists of all normal covers? (alias numerable covers), where a cover UU is normal if there is a sequence of covers {U n} n0\{U_n\}_{n\ge0} such that U=U 0U=U_0 and U n+1U n+1U_{n+1}U_{n+1} refines U nU_n.

Compact regular locale

On a compact regular locale the system of all covers forms a uniformity. Maps out of compact regular locales are automatically uniform.

Complete uniform locales

A uniform locale LL is complete if every dense uniform embedding LXL\to X is an isomorphism of uniform locales.

The category of complete uniform locales is a reflective subcategory of uniform locales. The reflection functor is known as the completion functor.

Concretely, the completion of a uniform locale LL with a system of uniform covers AA can be described as follows. Its opens are downward-closed subsets UU of the underlying frame of LL that satisfy the following saturation conditions:

  • If for some aLa\in L we have {xLx< Aa}U\{x\in L\mid x\lt_A a\}\subset U, then also aUa\in U. Here x< Aax\lt_A a means that there is CAC\in A such that C[x]aC[x]\le a.

  • If for some CAC\in A and aLa\in L we have aCUa\wedge C\subset U, then also aUa\in U.

Criteria for completeness

Every compact regular locale is complete. The fine uniformity on a paracompact locale is complete.

Isbell’s theorem states that a locale is paracompact if and only if it admits a complete uniformity.

A completely regular locale is compact if and only if it admits a complete uniformity that has a basis in which all covers are finite.


A detailed treatment of uniform locales can be fund in

The following 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).

These ideas are developed further in

  • Graham Manuell, Uniform locales and their constructive aspects, arxiv:2106.00678

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.

Last revised on June 16, 2021 at 17:39:21. See the history of this page for a list of all contributions to it.