nLab
measurable locale

Measurable locales

Idea

Measurable locales are certain locales, which may serve as a basis for measure theory much as general locales serve as a basis for topology (especially in constructive mathematics).

Ironically, in constructive mathematics, measurable locales are not locales (except for the empty space), on pain of excluded middle.

The concept appears to be due to Dmitri Pavlov.

Definitions

At present, there is no purely order-theoretic definition of measurable locales. However, there are a few other ways of defining them. We give first definitions appropriate for classical mathematics.

As a preliminary step, consider the category CompBoolAlg sup of complete boolean algebras and supremum-preserving homomorphisms of boolean algebras. This is a full subcategory of the category Frm of frames and so its opposite category CompBoolAlg sup op is a full subcategory of the category Loc of locales. The category MeasLoc of measurable locales is yet further a full subcategory of CompBoolAlg sup op, so our job is simply to specify which complete boolean algebras are the objects of this category.

By one definition, a complete boolean algebra L is a measurable locale if there is a complete measure space X such that L is isomorphic (as a boolean algebra) to the boolean algebra /𝒩 of measurable subsets of X modulo null subsets. Note that the measure on X is irrelevant except to specify the null subsets. In this way, MeasLoc becomes equivalent to the category LocMeas of localisable measurable spaces.

By another definition, a complete boolean algebra L is a measurable locale if for every element x0 of L there is a normal measure (see below) μ on L valued in [0,] such that μ(x)=1.

By yet another definition, a complete boolean algebra L is a measurable locale if there is a commutative W *-algebra A such that L is isomorphic (as a boolean algebra) to the boolean algebra Proj(A) of projection operator?s in A; see idempotent operator for a construction of Proj(A). In this way, MeasLoc becomes dual to the category CommW *Alg of commutative W *-algebras.

Whichever of these equivalent definitions is adopted, a measurable function between measurable locales is simply a continuous map between them as locales; these are the morphisms of MeasLoc.

In constructive mathematics

(This is the only section not due to Pavlov.)

For purposes of constructive mathematics, I suspect that it is appropriate to use the definition from W -algebras, so long as we allow norms to be upper real numbers. (If they are all located, then Proj(A) has decidable equality, which we don't want to require.) I'm less certain whether the other definitions can work.

For this definition, we need not require that LProj(A) be complete (or even a boolean algebra); this can be proved … classically. But constructively Proj(A) need not be complete (although it is still a boolean algebra). Indeed, consider the point (see the examples), based on A, which is not the complete Heyting algebra of all truth values but only the (possibly incomplete) boolean algebra {,} of classical truth values (corresponding to the self-adjoint idempotent complex numbers 0 and 1).

It seems to me that there is some notion of completeness that applies here; L should in some sense be ‘measurably complete’. In the point, for example, the subsingleton {*P}, where P is a truth value, is measurable iff P is true or false, so the supremum of {P} exists in L under the same circumstances.

Examples

The empty space, which is initial in MeasLoc, is the terminal boolean algebra with one element.

The point, which is terminal in MeasLoc, is the initial boolean algebra {,} of (classical) truth values.

The real line is the boolean algebra of Lebesgue-measurable sets of real numbers modulo the null sets. This is complete as a boolean algebra because … [argument needed] (and even constructively, it is still a boolean algebra).

Applying the classification of W *-algebras, we find that (up to isomorphism), every measurable locale is a direct product (of boolean algebras, which is a coproduct in MeasLoc) of points or of points and infinitely many real lines; a single real line is already isomorphic to the product of countably infinitely many real lines. (Of course, we can't expect this classification theorem? to hold constructively.)

The Borel real line

To do measure theory, it's important to know how to interpret the real line with the Borel sets (rather than Lebesgue sets) as a measurable space. This is actually a little tricky, because Lebesgue measure is not complete on the Borel sets, and passing to the Lebesgue sets gives a different measurable space. We might simply take the Borel sets as they are (so that only the empty set is null), but then this is not complete as a boolean algebra.

One might suspect that there is no Borel real line in MeasLoc, which would cast serious doubts on that as a category for measure theory. But we can argue by abstract nonsense (specifically the representable functor theorem) that it must exist, although it is quite large: something like an uncountable product of points and lines.

More generally, topological spaces give rise to rather complicated measurable locales by taking the Borel sets and applying an analogous argument, while smooth manifolds give rise to much simpler measurable locales by taking the Lebesgue sets (possible since we know which sets are null sets on a manifold). Both processes are functors (B:TopMeasLoc and L:TopManMeasLoc).

Measures

On any complete boolean algebra L, given any abelian monoid R equipped with a convergence structure (such as [0,]), a normal measure on L valued in R is a function μ:LR such that:

One could, of course, define a garden-variety measure by requiring continuity only when S is the image of a decreasing sequence, but apparently normal measures are what we want for measurable locales.

(Perhaps there is a theorem that non-atomic measures on, say, Lebesgue space correspond to normal measures on the real line as a measurable locale? Certainly Lebesgue measure is not normal on the σ-algebra of measurable sets, but presumably it is normal on the boolean algebra of measurable sets modulo null sets, which is what we want.)

References

The theory of measurable locales seems to be published entirely on MathOverflow, in various questions and answers by Dmitri Pavlov. Here is an index:

  • Dmitri Pavlov, answer to Is there a category structure one can place on measure spaces so that category-theoretic products exist? (version: 2011-01-08)

Another post not in this index is: