BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:The valuation locale monad (continued) - Dr Steve
Vickers (School of Computer Science\, University
of Birmingham)
DTSTART:20111122T120000Z
DTEND:20111122T130000Z
UID:TALK734AT
URL:/talk/index/734
DESCRIPTION:In previous talks I recalled some basic ingredient
s of measure theory\, and\ndescribed how they can
be translated into an analogous theory using\nloca
les. Measurable spaces become locales\, measure be
comes valuation.\nThere\nis a theory of lower inte
gration (approximated from below) in which the\nin
tegrand is a map to the lower reals (with Scott to
pology) in the\ninterval\n[0\, infinity].\n\nIn me
asure theory\, much of the structure can be discus
sed in terms of the\n_Giry monad_\, which\, to eac
h measurable space X\, assigns the space of\nmeasu
res on X. A localic analogue is the valuation loca
le: it assigns to\neach locale X a locale VX whose
points are the valuations on X. My draft\npaper (
on the web) proves that V is a commutative monad\,
and proves\nanalogues of the Riesz and Fubini the
orems.\n\nA key technical feature of my treatment
is calculate for VX in terms of a\nfinitary lattic
e L such that every open in the frame of X is a di
rected\njoin of elements of L. This is possible be
cause valuations are Scott\ncontinuous. It provide
s a notion of "simple map"\, used in the same way
as\nin measure theory - arbitrary maps are approxi
mated by simple maps\, and\nintegration is reduced
to the finitary combinatorics of simple maps.\n\n
Another technical trick is to use the locale XxR'\
, where R' is the upper\nreals [0\,infinity). Beca
use the lower reals [0\,infinity] are equivalent t
o\nthe coScott opens of [0\,infinity)\, we get tha
t maps X -> [0\,infinity] are\nequivalent to opens
of XxR'. It follows that integration can be expre
ssed\nas a continuous map from VX to V(XxR').\n\nI
n investigating V(XxR') I showed last time how to
present the frame of\nXxR' in terms of a finitary
tensor product of L and the non-negative\nrational
s\, and I gave a concrete description of that tens
or product\n(concrete as opposed to just giving ge
nerators and relations). This tensor\nproduct is t
he lattice of simple maps.\n\nIn this instalment I
shall give an alternative universal characterizat
ion\nthat brings in the additive structure of simp
le maps. Combining the\nlattice\nand additive stru
ctures\, we are able to show that the image of VX
in\nV(XxR') comprises exactly the linear measures
on XxR'\, and that is our\nRiesz theorem. (Riesz s
ays that measures are equivalent to linear\nfuncti
onals.)\n\nThat may already be enough for one talk
\, but the continuation is to use\nthe Riesz theor
em to define the unit\, multiplication and strengt
h of V as\na\nmonad.\n\n"Commutativity" of a stron
g monad is the property that two obvious ways to\n
define a map VXxVY -> V(XxY) are equal\, and in ou
r situation this is a\nFubini theorem. The proof a
gain relies on the reduction to simple maps\,\nand
\na form of the principle of inclusion and exclusi
on. An interesting logical\nissue is that the lowe
r reals do not form a cancellation monoid\, so a\n
workaround is needed for what would normally be do
ne by subtraction.\n
LOCATION:CS 217
CONTACT:Dan Ghica
END:VEVENT
END:VCALENDAR