11
$\begingroup$

Let $\mathcal{E}$ be a Grothendieck topos. I want to define a sort of "$\sigma$-algebra" for it, and I'm asking about what it should be—or already is—called. I know from nlab that Cheng spaces are an accepted constructive notion of $\sigma$-algebras but I don't yet see why I might find them interesting. So one may answer this question by instead telling me why my notion (see below) may not be well-behaved, or what's so nice about Cheng spaces. But let's leave that question aside for now.

In the proposed definition below, I'll use the internal language of $\mathcal{E}$. I'll use the convention that $A\Rightarrow B\Rightarrow C$ means $A\Rightarrow(B\Rightarrow C)$. I'll use $\lambda$ notation for terms of exponential objects; for example given types $X$ and $P$ and a term $p:P$, I'll write $\lambda(x:X)\ldotp p$ to denote the function $X\to P$ that is constant at $p$.

Definition: Let $\mathcal{E}$ be a Grothendieck topos, $\top\colon 1\to\Omega$ its subobject classifier, and $\mathbb{N}$ its natural numbers object. A pseudo-$\sigma$ algebra in $\mathcal{E}$ consists of an object $X$ and a morphism $\Sigma\colon \Omega^X\to\Omega$ satisfying the following axioms:

  • $\forall(\omega:\Omega)\ldotp\Sigma\big(\lambda(x:X)\ldotp\omega\big)\;\;\;\;$ ["constant propositions are measurable"]
  • $\forall(\phi,\psi:X\to\Omega)\ldotp \Sigma(\phi)\Rightarrow\Sigma(\psi)\Rightarrow\Sigma(\phi\wedge\psi)\;\;\;\;$ ["closed under $\wedge$"]
  • $\forall(\phi,\psi:X\to\Omega)\ldotp \Sigma(\phi)\Rightarrow\Sigma(\psi)\Rightarrow\Sigma(\phi\vee\psi)\;\;\;\;$ ["closed under $\vee$"]
  • $\forall(\phi,\psi:X\to\Omega)\ldotp \Sigma(\phi)\Rightarrow\Sigma(\psi)\Rightarrow\Sigma(\phi\Rightarrow\psi)\;\;\;\;$ ["closed under $\Rightarrow$"]
  • $\forall(\phi:\mathbb{N}\to\Omega^X)\ldotp\big(\forall(n:\mathbb{N})\ldotp\Sigma(\phi(n))\big)\Rightarrow\Sigma\big(\forall(n:\mathbb{N})\ldotp\phi(n)\big)\;\;\;\;$ ["closed under countable $\forall$"]
  • $\forall(\phi:\mathbb{N}\to\Omega^X)\ldotp\big(\forall(n:\mathbb{N})\ldotp\Sigma(\phi(n))\big)\Rightarrow\Sigma\big(\exists(n:\mathbb{N})\ldotp\phi(n)\big)\;\;\;\;$ ["closed under countable $\exists$"]

For any $\phi:X\to\Omega$, say that $\phi$ is measurable if $\Sigma(\phi)=\top$.

Question: What might be a more common, more useful, or better terminology for what I've called pseudo-$\sigma$ algebras?

I guess it's different than just a sub-Heyting algebra of $\Omega^X$ because of the "countable quantification".

$\endgroup$
  • 1
    $\begingroup$ What is the motivation for this question? Are you trying to develop measure theory in a topos? $\endgroup$ – Dmitri Pavlov Jun 26 '17 at 10:47
  • $\begingroup$ I'm starting to think lightly about it; I haven't delved into it. Eventually, I will want some notion of probability in a particular (étendue) topos. But measure theory in a general topos would be great. $\endgroup$ – David Spivak Jun 26 '17 at 23:38
  • $\begingroup$ Point-set notions such as topological spaces and measurable spaces do not work well in arbitrary toposes. Instead one must replace them with pointfree/pointless notions such as locales and measurable locales. See ncatlab.org/nlab/show/measurable+locale $\endgroup$ – Dmitri Pavlov Jun 27 '17 at 8:29
  • 2
    $\begingroup$ Does this help? mathoverflow.net/questions/141764/… $\endgroup$ – Bas Spitters Jun 27 '17 at 16:42
  • 1
    $\begingroup$ Another work on this topic is Matthew Jackon’s PhD Thesis, A sheaf theoretic approach to measure theory, which gives another approach to developing measure theory in toposes. $\endgroup$ – Peter LeFanu Lumsdaine Jun 28 '17 at 10:17
4
$\begingroup$

This is an answer to the new question formulated in the comments.

Point-set notions of topological spaces are a poor fit for arbitrary toposes because constructing points typically requires the axiom of choice, whereas constructing the lattice of open sets does not. This is the reason why locales are used instead of topological spaces in this context.

This can be concisely illustrated by the following fact: in the presence of the axiom of choice, locally compact locales as well as compact regular locales are spatial, i.e., come from topological spaces.

For example, open sets in the Zariski spectrum of a commutative ring are radical ideals, whereas points are prime ideals, and proving that a ring has sufficiently many prime ideals requires the axiom of choice, whereas proving that it has sufficiently many radical ideals does not. Similar statements can be made about C*-algebras and other types of rings.

The situation for measure spaces is similar. First, if one looks at typical theorems in measure theory, it becomes clear that the data of a σ-algebra alone is never sufficient to formulate an interesting theorem in measure theory; one needs to know at least what the sets of measure 0 are (for more details, see Is there an introduction to probability theory from a structuralist/categorical perspective?).

If we adopt this new notion of measurable space (i.e., a set X, a σ-algebra M of measurable subsets, and a σ-ideal N of negligible sets, equivalently, a measure class), the resulting category of measurable spaces is equivalent to the category of measurable locales (see https://ncatlab.org/nlab/show/measurable+locale): given a measurable space (X,M,N), send it to the poset (a frame, in fact) M/N, i.e., equivalence classes of measurable sets modulo negligible sets.

One can then illustrate the above points (pun intended) for measurable spaces by considering the equivalence between commutative von Neumann algebras, measurable locales, and measurable spaces. A measurable locale can be extracted from a von Neumann algebra in a canonical fashion: it is simply the complete Boolean algebra of its projections. To extract a measurable space, however, one needs the axiom of choice: the points of the measurable space are maximal C*-ideals in the von Neumann algebra.

One must mention that measure theory in a topos has not yet been developed to the same extent that general topology is. For instance, the equivalence between commutative C*-algebras and compact regular locales is proven in a very satisfactory form in arXiv:1411.0898v1. There is no similar exposition for commutative von Neumann algebras and measurable locales in the literature. (I had some correspondence with Simon Henry about this, and the conclusion was that it seems like it can be done, but no details can be found in the literature.)

$\endgroup$
  • $\begingroup$ About measure theory in a topos one should mention these two paper of Steve Vickers : 1) cs.bham.ac.uk/~sjv/integration.pdf 2) cs.bham.ac.uk/~sjv/Riesz.pdf Which develop the notion of measure (=valuation) on locales and integration relative to them in a fully constructive setting. $\endgroup$ – Simon Henry Jun 28 '17 at 8:31
  • $\begingroup$ I also want to add that going to a boolean locales from a locale with a valuation as it can be done in the non-constructive case is hard (and by that I mean impossible) which is the main reason why a constructive version of the equivalence between commutative Von Neumann algebra and "measure space" is hard to obtain. $\endgroup$ – Simon Henry Jun 28 '17 at 8:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.