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.”

Covering uniformities

A 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.

  • For AOp(X)A \in Op(X), C[A]{BC|ABC[A] \coloneqq \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


Mike Shulman: I do not know the state of a constructive version of uniform locale theory. Most of the papers on uniform locales seem to assume classical logic, in particular in writing C[A]={BC|AB}C[A] = \bigcup \{ B \in C \;|\; A \cap B \neq \bot \}. The above definition seems to me the obvious constructive version, but I don’t know how well it behaves. It’s conceivable one might need to restrict to overt locales, where positivity behaves better.


Apparently there is work on constructive uniform locale theory here:

  • 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).

And indeed, a constructive and predicative theory in the programme of formal topology 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 September 1, 2014 06:29:28 by Toby Bartels (