The valuation locale monad (continued)

Add to your list(s) Download to your calendar using vCal

• Dr Steve Vickers (School of Computer Science, University of Birmingham)
• Tuesday 22 November 2011, 12:00-13:00
• CS 217.

If you have a question about this talk, please contact Dan Ghica.

In previous talks I recalled some basic ingredients of measure theory, and described how they can be translated into an analogous theory using locales. Measurable spaces become locales, measure becomes valuation. There is a theory of lower integration (approximated from below) in which the integrand is a map to the lower reals (with Scott topology) in the interval

In measure theory, much of the structure can be discussed in terms of the Giry monad, which, to each measurable space X, assigns the space of measures on X. A localic analogue is the valuation locale: it assigns to each locale X a locale VX whose points are the valuations on X. My draft paper (on the web) proves that V is a commutative monad, and proves analogues of the Riesz and Fubini theorems.

A key technical feature of my treatment is calculate for VX in terms of a finitary lattice L such that every open in the frame of X is a directed join of elements of L. This is possible because valuations are Scott continuous. It provides a notion of “simple map”, used in the same way as in measure theory – arbitrary maps are approximated by simple maps, and integration is reduced to the finitary combinatorics of simple maps.

Another technical trick is to use the locale XxR’, where R’ is the upper reals [0,infinity). Because the lower reals [0,infinity] are equivalent to the coScott opens of [0,infinity), we get that maps X → [0,infinity] are equivalent to opens of XxR’. It follows that integration can be expressed as a continuous map from VX to V(XxR’).

In investigating V(XxR’) I showed last time how to present the frame of XxR’ in terms of a finitary tensor product of L and the non-negative rationals, and I gave a concrete description of that tensor product (concrete as opposed to just giving generators and relations). This tensor product is the lattice of simple maps.

In this instalment I shall give an alternative universal characterization that brings in the additive structure of simple maps. Combining the lattice and additive structures, we are able to show that the image of VX in V(XxR’) comprises exactly the linear measures on XxR’, and that is our Riesz theorem. (Riesz says that measures are equivalent to linear functionals.)

That may already be enough for one talk, but the continuation is to use the Riesz theorem to define the unit, multiplication and strength of V as a monad.

“Commutativity” of a strong monad is the property that two obvious ways to define a map VXxVY → V(XxY) are equal, and in our situation this is a Fubini theorem. The proof again relies on the reduction to simple maps, and a form of the principle of inclusion and exclusion. An interesting logical issue is that the lower reals do not form a cancellation monoid, so a workaround is needed for what would normally be done by subtraction.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.