atomic_probability.tex

\documentclass[a4paper]{amsproc}
\renewcommand\labelenumi{(\roman{enumi})}
\renewcommand\theenumi\labelenumi
\title{An Atomic Topos for Probability Theory}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{fontspec}
\usepackage[hcentering,bindingoffset=0mm]{geometry}
%\usepackage[hyphens]{url} \urlstyle{same}
\usepackage{tikz}
\usepackage{lscape}
\usepackage{mathtools}
\usetikzlibrary{cd}
%\usepackage[dvips]{graphicx} %% Package for inserting illustrations/figures

% I like how the sans serif doesn't stand out as much in this font.
\setmainfont{FreeSerif}

\theoremstyle{plain}
 \newtheorem{theorem}{Theorem}[section]
 \newtheorem{proposition}[theorem]{Proposition}
 \newtheorem{lemma}[theorem]{Lemma}
 \newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
 \newtheorem{example}[theorem]{Example}
 \newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
 \newtheorem{remark}[theorem]{Remark}
 \numberwithin{equation}{section}

% Some shortcuts
% \newcommand{\ob}[1]{ob(#1)}
\newcommand{\id}{\textup{id}}

\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Sh}{Sh}
\newcommand{\y}{\textit{y}}
% The star indicates that subscripts are to be typeset below the operator
% instead of to the right
\DeclareMathOperator*{\limit}{lim}
\DeclareMathOperator*{\colim}{colim}
\DeclareMathOperator{\Lan}{Lan}
\DeclareMathOperator{\eq}{eq}
\newcommand{\s}{\textsf{ }}

\newcommand{\Set}{\textup{\textsf{Set}}}
\newcommand{\FinProb}{\textup{\textsf{FinProb}}}
\newcommand{\BPAlg}{\textup{\textsf{BPAlg}}}
\newcommand{\Ind}{\textsf{Ind}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\Prob}{\mathfrak{Prob}}

\newcommand{\la}{\langle\,}
\newcommand{\ra}{\,\rangle}

\newcommand{\ldoub}{[\![}
\newcommand{\rdoub}{]\!]}
\makeatletter
\newcommand{\rmnum}[1]{\romannumeral #1}
\newcommand{\Rmnum}[1]{\expandafter\@slowromancap\romannumeral #1@}
\makeatother

\author{Adam Dauser, Adrian Marti}

\date{}
\begin{document}

\maketitle

\begin{abstract}
Inspired by probability, we introduce topos $\Prob$. %TODO do this but properly
\end{abstract}

\tableofcontents


\section{Introduction}

Talk about 'bookkeeping' in probability theory. Nobody cares about the choice of base $\sigma$-algebra, as long as it has good properties. Yet, a $\sigma$-algebra must be chosen. Probability theorists always quantify over a good class of $\sigma$-algebras. The domain of a random variable never gets fixed on a particular $\sigma$-algebra. One may try to exploit this by imposing restrictions(of functorial or topological nature) on how statements/sets may depend on the base $\sigma$-algebra. These techniques will lead to an approach to probability theory that works without a choice of $\sigma$-algebra. Outline the standard set up.

First technical improvement: Divide out null sets! (Explain this in detail) Define measure algebras and show how they interact with $\sigma$-algebras.

Step 3:  Intervals model Lebesgue interval. Give the definitions.

%logics
\indent Talk about how this is a substantial application justifying the use of geometric/infinitary logic, since first order logic doesn't suffice. Talk about how one can't even define probability intervals in first order logics. Completeness, Quantifier elimination.\newline
\indent To do this we use the topos $\Prob$. Shortly explain how models of the theory correspond to intervals and how other structure can be transported along that morphism. Here we give background to topos theory. Completeness comes from an 'open surjection' a map of topoi to $\Set$ that preserves and reflects this infinitary first order logics. Completeness legitimizes the belief that the underlying $\sigma$-algebra does not matter, to a certain extend(in the geometric logic sense). Explain enough to justify simple functions. I.e. the universal model. The simple functions are mapped to each other.
\begin{center}\textbf{ALWAYS EXPLAIN THE REASONING BEHIND ALL THE CONCEPTS WHICH APPEAR HERE}\end{center}
Also say that usual Galois theory a la SGA1 does not suffice to capture the group action flavour. The group is simple but profinite groups are completely determined by their closed normal subgroups (or smth. similar). State the main result (group of automorphisms ... commonly called measure preserving dynamical systems).\newline
\indent Combinatorial methods using 'multi-products'. We give a nice calculus of our topos using its "atoms". This also yields a description by a model of ZFA. \newline
\indent Hype!!! $L^p$ spaces and other outlook.

Somewhere in here we should definitely mention Olivia's bridges philosophy and how we give three very distinct site presentations (and the $\infty$-positivization) of $\Prob$.

\subsection{Transfer results for $L^\infty$-spaces}
%TODO: PROVE THAT ANY function $f:\mathbb{R} \to \mathbb{R}$ we get a map $f: \mathcal{S} \to \mathcal{S}$(defined pointwise) that gets sent to the expected map on atomless $\sigma$-algebras.

We will now try to transfer statements between $L^\infty(X,\mu)$ for atomless probability algebras $(X,\mu)$. The key insight is that we know how to transfer statements about simple functions and bounded measurable functions can be approximated by them. Another insight is, that every bounded, measurable function on a probability space is integrable. So $L^\infty(X,\mu)$ is an expectation algebra, in particular, for any probability interval $(X,\mu)$ in \Set.
\begin{definition} For a expectation algebra $S$ we define:
\begin{enumerate}
\item $f\geq g$ if $\exists h. h^2=f-g$
\item $|f|$ is the function uniquely determined by $f^2=|f|^2\wedge |f|\geq 0$
\item $f^+=\frac{1}{2}(f+|f|)$ and $f^-=\frac{1}{2}(f-|-f|)$
\item For $p$ an integer, $||f||_p=r$ if $E_{r^p}(|f|^p)$
\item $||f||_\infty=r$ if $\bigwedge_{k\in\mathbb{N}}\bigvee_{N\in\mathbb{N}}\bigwedge_{n\geq N}\bigvee_{-1/k\leq s\leq 1/k}||f||_{n}=r+s$

\end{enumerate}
\end{definition}
The last definition is motivated by the fact that for the algebras simple functions and bounded functions, we have
\[  \\limit_{n\rightarrow \infty} ||f||_n=||f||_\infty. \]
Note that the fact that all statements of the previous definition are infinitary first order, we can transfer statements using them between algebras of simple functions. The next insight will be that we can actually define given simple functions uniquely using only infinitary first order language in the theory of expectation algebras.\newline
\indent The next step is to characterise simple functions among bounded measurable functions. This will also allow us to classify the definable subsets of algebras of simple functions.
\begin{definition} For an expectation algebra $S$, $f$ is called a
\begin{enumerate}\item \emph{characteristic function} if $(f-1)^+-f^- -(f-1)^-f^+=0$. Write this relation $\chi$.
\item \emph{simple function} if $\bigvee_{n\in \mathbb{N}}\exists f_1 \cdots \exists f_n. \bigwedge_{i=1}^n \chi(f_n)\wedge \bigvee_{r_1,\cdots,r_n\in\mathbb{R}} f=\sum_{i=1}^n r_if_i$. Call this relation $s$.
\end{enumerate}
\end{definition}
In the case of $L^\infty(X,\mu)$ or $S(X,\mu)$, these definitions can easily be seen to be equivalent to the ordinary ones. Note also that these are geometric statements.
\begin{theorem}
The complete boolean algebra of subsets of $S(X,\mu)^n$ for an interval $(X,\mu)$ in \Set, definable by infinitary first order (equivalently geometric) statements in the theory of expectation algebras, with $n$ free variables, is generated by subsets of the form:
\[\{(f_1,\cdots, f_n)\mid f_1,\cdots, f_n\text{have cumulative distribtion function g}\} \]
for $g:\mathbb{R}^n\rightarrow\mathbb{R}$ cumulative distribution functions of $n$-tuples of simple functions.
\end{theorem}
\begin{proof}
These subsets correspond precisely to the images under $f^*$, the inverse image functor classifying $(X,\mu)$, of the atoms of $\mathcal{S}^n$. This shows, that the lattice of definable sets is certainly contained in the lattice given in the statement.\newline
\indent For the converse, we have to construct for any cumulative distribution function of an $n$-tuple of simple functions, a infinitary first order statement satisfied by precisely all the $n$-tuples of simple functions with the same cumulative distribution function. Given simple functions some interval $(X,\mu)$ in \Set $f_i=\sum_{j=1}^{m} r_{j}\chi_{a_j}$ for $1\leq i\leq n$ with and $a_j\neq 0$ disjoint from $a_{j'}$ for  $j\neq j'$ on. Say $\mu(a_{j})=\mu_{j}$.  We claim that the following geometric statement with free variables $h_i$ characterises all the simple functions with the same distribution function as $f_i$:
\[\exists g_1\cdots \exists g_m. \bigwedge_{j=1}^m(\chi (g_j)\wedge E_{\mu_{j}}(g_j))\wedge \bigwedge_{i=1}^n\sum_{j=1}^m r_jg_j=h_i   \]  %make this prettier and internal to $\mathcal{S}$!
\end{proof}
We will now see that we can generalise this theorem to all measurable functions and, with that, get a transfer result. First some lemmas.
\begin{lemma} The one for atomic statements
\end{lemma}
\begin{lemma}\label{atomic_L_infty} Given an atomic statement in the theory of expectation algebras $\Phi(f_1,\cdots,f_n)$ with free variables $f_1,\cdots, f_n$. If it holds for functions $f_1,\cdots ,f_n\in L^\infty(X,\mu)$ for an atomless probability algebra $(X,\mu)$ in \Set, then it holds for all $n$-tuple $f_1',\cdots, f_n'\in L^\infty(X,\mu)$ with the same distribution function $g:\mathbb{R}^n\rightarrow \mathbb{R}$.
\end{lemma}
\begin{proof}
For any $n$-tuple of bounded measurable functions $f_1,\cdots, f_n$ and polynomial $f\in \mathbb{R}[X_1,\cdots, X_n]$, we have:
\[\int_X f(f_1,\cdots,f_n)d\mu=\\limit_{\substack{g_1\rightarrow f_1,\cdots, g_n\rightarrow f_n \text{ in }L^\infty\\ g_1\cdots g_n \text{ simple}}}  \int_Xf(g_1,\cdots,g_n)d\mu \]%formulate this properly
This is true as simple functions are dense in $L^\infty(X,\mu)^n$. Thus we have:
\[E_0(f_1,\cdots,f_n)\iff \forall g_1\cdots \forall g_n.(\bigwedge_{i=1}^n s(g_i))\wedge\bigwedge_{\epsilon>0}\bigvee_{\delta>0}(\bigvee_{0\leq r\leq \delta}||f_i-g_i||_\infty=r \]
\[\implies\bigvee_{|s|\leq\epsilon} E_s(g_1,\cdots,g_n) )\]%bad and ugly
$E_s(g_1,\cdots,g_n)$ only depends on the cumulative distribution function of $g_1,\cdots,g_n$. So it will already hold if not $||f_i-g_i||_\infty=r$ but merely $g_i$ have the same  cumulative distribution function as some $n$-tuple of simple functions for which this holds. The existence of such a tuple can be read off the cumulative distribution function of $f_1,\cdots,f_n$.%Finish the argument
\end{proof}
\begin{lemma}\label{distribution_L_infty} The joint cumulative distribution functions of $n$-tuple of bounded measurable functions on an atomic probability algebra $(X,\mu)$ in \Set are precisely the functions $g:\mathbb{R}^n\rightarrow \mathbb{R}$ which are:
\begin{enumerate}
\item Right-continuous in all variables
\item Non-decreasing in all variables
\item There exist real numbers $r_1,\cdots,r_n,s_1,\cdots, s_n$, such that we have $f(x_1,\cdots,x_n)=0$ for all $x_i\leq r_i$ and $f(x_1,\cdots,x_n)=1$ for all $x_i\geq s_i$  and for each $i$ and numbers $x_j$ for $i\neq j$, $f(x_1,\cdots,x_n)$ is constant in $x_i$ outside $[s_i,r_i]$.%Check this is the right condition
\end{enumerate}
\end{lemma}
\begin{proof}
We adopt a proof of a similar statement from [Probability: Theory and Examples by Rick Durrett, Thm 1.2.1 and 1.2.2].
\begin{enumerate}
\item It is right continuous as $\\limit_{y\rightarrow x^+}f^{-1}(-\infty,y)=f^{-1}(-\infty, x)$
\item The function is non-decreasing in all variables by the monotonicity of the measure
\item As the functions are bounded in both directions, we have $\mathbb{E}((f-c)^+)=1$ for some $c$ small enough and $\mathbb{E}((f-c)^+)=0$ for some $c$ large enough.
\end{enumerate}
Conversely, given such a joint cumulative distribution function, we seek to construct an $n$-tuple of functions with these properties. The reference describes how this can be done for the Lebesque interval. So it suffices to construct a measure preserving measurable function $f:(X,\mu)\rightarrow (I,\lambda)$. We repeatedly use the interval property to define elements $x_{\frac{1}{2}}$ of $X$ of measure $\frac{1}{2}$, then bisecting it and its complement to get elements $x_{\frac{k}{2^n}}$ of measure $\frac{1}{2^n}$. We now define the map by $f^{-1}(0,r)=\bigvee_{\frac{k}{2^n}\leq r} x_{\frac{k}{2^n}} $. %make this precise
\end{proof}
\begin{corollary}\label{quantifierfreeLinfty}
Given a \emph{quantifier-free} infinitary first-order statement $\Phi$ in the theory of expectation algebras and any atomless probability algebras $(X,\mu)$ and $(Y,\nu)$ then we have:
\[L^\infty(X,\mu)\vDash\Phi \iff L^\infty(Y,\nu)\vDash \Phi \]
\end{corollary}
\begin{proof}
This is true for atomic statements simply because they only depend on the joint cumulative distribution function of the free variables and the set of these functions coincides for all choices. A simple symbolic recursion yields the quantifier-free case.
\end{proof}
Interestingly, we \emph{cannot} extend this result to statements containing quantifiers in general! Almost magically, statements in the theory of expectation algebras for $L^\infty(X,\mu)$ can detect whether elements in the underlying probability algebra $(X,\mu)$ are countably generated. This was the case neither for the theory of intervals nor for simple function algebras.
\begin{definition} A probability algebra $(X,\mu)$ is said to be $\aleph_1$\emph{-atomless} if there exists no element $x\in X$ such that the boolean algebra $\downarrow x$ is countably generated.
\end{definition}
These probability algebras have the following saturation property, which is necessary for dealing with quantifiers:
\begin{lemma} Given a function $g:\mathbb{R}^n\rightarrow \mathbb{R}$ with the conditions of lemma \ref{distribution_L_infty} and bounded measurable functions $f_1,\cdots, f_{n-1}\in L^\infty(X,\mu)$ for some $\aleph_1$-atomless probability algebra $(X,\mu)$, such that their joint cumulative distribution function $\tilde{g}:\mathbb{R}^{n-1}\rightarrow \mathbb{R}$ has
\[g(x_1,\cdots, x_n)=\tilde{g}(x_1,\cdots, x_{n-1}) \text{ for }x_n\text{ large enough} \]
Then there exists a bounded measurable function $f_n\in L^\infty(X,\mu)$ such that the joint cumulative distribution function of $f_1,\cdots,f_n $ is $g$.
\end{lemma}
\begin{proof}
This is essentially 4.5 [Keisler paper].
\end{proof}
\begin{remark} It is shown in [Keisler paper] that this lemma fails for the Lebesgue interval. Also note that such probability algebras actually exist, see ibid.
\end{remark}
\begin{theorem}
For any infinitary first order statement in the theory of expectation algebras $\Phi$ and all $\aleph_1$-atomless probability algebras $(X,\mu)$, $(Y,\nu)$, we have:
\[L^\infty(X,\mu)\vDash\Phi \iff L^\infty(Y,\nu)\vDash\Phi \]
Moreover, the subsets of $L^\infty(X,\mu)^n$ definable by infinitary first order statements are precisely unions of sets of the form
\[\{(f_1,\cdots,f_n)\mid f_1,\cdots,f_n \text{ have cumulative distribution function }g \} \]
where $g:\mathbb{R}^n\rightarrow\mathbb{R}$ is right-continuous and non-decreasing, zero for all values small enough and one for all values large enough in all variables.
\end{theorem}
\begin{proof}
We seek to extend the result of \ref{quantifierfreeLinfty} to statements containing quantifiers. To do this we use symbolic recursion:\newline
\indent Assume one has a statement $\Phi(f_1,\cdots f_n)$ with free variables $f_1,\cdots, f_n$ which only depends on the joint cumulative distribution of $f_1,\cdots, f_n$. We seek to show that then, so does $\exists f_1.\Phi(f_1,\cdots f_n)$. \newline
\indent We have shown that the validity of all statements only depends on the joint cumulative distribution function of the free variables. This concludes the first part of the lemma in conjunction with lemma \ref{distribution_L_infty} as the joint cumulative distribution functions are exactly the same.\newline
\indent So it remains to show that we can define the set
\[\{(f_1,\cdots,f_n)\mid f_1,\cdots,f_n \text{ have cumulative distribution function }g \} \]
 with $g$ as in the statement. This is possible with the following statement:
 \[\bigwedge_{n\in \mathbb{N}}\text{There exist a lot of simple functions below it...} \]
This concludes the second part of the lemma.
\end{proof}
\begin{remark} This gives definitive evidence, that there cannot a "universal" $L^\infty$ algebra in $\Prob$, whose images under the inverse image functors given by models $(X,\mu)$ are precisely the expectation algebras $L^\infty(X,\mu)$. For this, we would need a topos that somehow axiomatises the property of being $\aleph_1$-atomless, which is, as we stated it, formulated in second order logic.
\end{remark}
\section{$\Prob$ as a topos of continuous group actions}

We seek to apply the following result due to O.Caramello:

\begin{theorem}\label{olivia}
Let $\C$ be a small, inhabited category satisfying the amalgamation and joint-embedding properties, and let $u$ be a $\C$-universal and $\C$-ultrahomogeneous object in $Ind(\C)$. Then the collection $\mathcal{I}_{\C}$ of sets of the form $\mathcal{I}_{\chi}:=\{f:u\overset{\sim}{\rightarrow} u\mid  f\circ \chi=\chi\} $, for an arrow $\chi:c\rightarrow u$, form an object $c$ of $\C$ to $u$ defines an algebraic base for the group of automorphisms of $u$ in $Ind(\C)$, and, denoted by $Aut_\C$ the resulting topological group, we have an equivalence of toposes
\[\Sh(\C^{op},J_{at})\simeq \text{Cont}(Aut_\C) \]
induced by the functor $F:\C^{op}\rightarrow \text{Cont}(Aut_{\C})$ which sends any object $c$ of $\C$ to the set $\Hom_{Ind(\C)}(c,u)$ equipped with the action by post-composition and any arrow $f:c\rightarrow d$ in $\C$ to pre-composition by $f$.
\end{theorem}

In our context we set $\C=BPAlg_f$ and will show that the Lebesgue interval is $BPAlg_f$-universal and $BPAlg_f$-ultrahomogeneous. But before we do that, we need some remarks that will be used in our proof.

\begin{remark}\label{partitions}
For an element $a \in B$ of a boolean algebra, we will denote the ideal of elements of $B$ that are less than or equal to $a$ by $I(a)$.
\begin{enumerate}
\item In the category of boolean algebras, if one has a \\ boolean algebra $A$, we get the following correspondence between decompositions $A \cong B \times C$ and partitions $a,b$ (i.e. pairs of elements $a,b$ with $a \vee b = 1$ and $a \wedge b = 0$). A decomposition $B \times C$ induces the partition $(1,0), (0,1)$ on $A$ and conversely the partition $a,b$ induces the decomposition \\ $A \cong I(a) \times I(b)$. This lets us interpret the product of boolean algebras as some sort of disjoint union.
\item The interesting thing about this description of products, is that it shows that if we have a map $A \to B$ of boolean algebras and we have a decomposition $A \cong A_1 \times A_2$, then this induces a decomposition of $B$.
\item Given two boolean probability algebras $(A, \mu)$ and $(B, \nu)$, there is a measure $(\mu + \nu)(x,y) := \mu(x) + \nu(y)$ on $A \times B$. Unfortunately, this can't be the product in $\BPAlg$, because $\mu + \nu$ is not a probability measure nor are the projections measure-preserving.
\end{enumerate}
\end{remark}

We could now start proving that the Lebesgue interval satisfies the required properties, but in order to emphasize that the Lebesgue interval is not really special, we will will prove that a well-known more general class of measure algebras is $BPAlg_f$-universal and $BPAlg_f$-ultrahomogeneous. The reader can ignore this and pretend that he is dealing with the Lebesgue interval.

\begin{definition} \label{maharam_type_homogeneous}
% TODO: Maharam-type homogeneous should be emphazised less by intead always requiring the 'ultrahomogeneous' hypothesis.
\begin{enumerate}
\item Let $A$ be a complete boolean algebra. We say that a subset $S \subset A$ generates $A$ if $A$ is the only complete boolean subalgebra of $A$ containing $S$.
\item Let $A$ be a complete boolean algebra. We say that the Maharam type of $A$ is the smallest possible cardinality of a generating set.
\item We moreover say that $A$ is Maharam-type-homogeneous if the Maharam type of every nonzero principal ideal $I(a)$ is the same.
\item Call a measure algebra Maharam-type-homogeneous if its underlying boolean algebra is Maharam-type homogeneous.
\end{enumerate}
\end{definition}

For more information on Maharam-type-homogeneous measure algebras, see chapter 33 of \cite{fremlin}. The crucial fact about Maharam-type-homogeneous measure algebras, is they are isomorphic if and only if they have the same Maharam type and the top element $1$ has the same measure on both measure algebras(see 331I of \cite{fremlin}). Moreover, there is a surprising theorem by Maharam (see 332J in \cite{fremlin}) that lets us decompose any atomless measure algebra into Maharam-type-homogeneous measure algebras.

Now we actually show that homogeneous-Maharam-type probability algebras are $BPAlg_f$-universal and $BPAlg_f$-ultrahomogeneous. More concretely, we prove the following for a Maharam-type-homogeneous probability algebra $(M, \alpha)$:

\begin{lemma}\begin{enumerate}
\item $\FinProb$ has a terminal object, proving the joint embedding property.
\item $\FinProb$ fulfills the right Ore condition.
\item For any $(A,\mu),(B,\nu)$ in $BPAlg_f$ , an arrow $f:(A,\mu)\rightarrow (B,\nu)$ in \\
 $BPAlg_f$, and arrows $\chi_1:(A,\mu)\rightarrow (M, \alpha)$ as well as $\chi_2:(B,\nu)\rightarrow (M, \alpha)$ in $\BPAlg$ there exists an isomorphism $j':(M, \alpha) \rightarrow (M, \alpha)$ such that $j'\circ \chi_1=\chi_2\circ j$:
 \begin{center}
 \begin{tikzcd}
{(A,\mu)} \arrow[r, "\chi_1"] \arrow[d, "j"'] & {(M, \alpha)} \arrow[d, "j'", dotted] \\
{(B,\nu)} \arrow[r, "\chi_2"']                & {(M, \alpha)}
\end{tikzcd}
 \end{center}
\item For any object $(A,\mu)$ of $BPAlg_f$ there exists an arrow $\chi:(A,\mu)\rightarrow (M, \alpha)$ in $\BPAlg$.
\end{enumerate}
\end{lemma}
\begin{proof}
\begin{enumerate}
\item The one-element set $1$ with with measure $\mu(\star)=1$ is the terminal object. Its underlying set the terminal object in $\Set$ and the universal map is tautologically measure preserving.
\item We have already shown this in \ref{pullbackMeasure}.
\item
Now, given boolean probability algebras as in the claim above, we see that $(A, \mu)$ has a partition into atoms $x_i$. Crucially, if we apply a map of boolean algebras to this partition, we get a partition again. This means we can decompose our problem(by \ref{partitions}) into finding a measure-preserving map $j'$ as below:
\[
\begin{tikzcd}
2 \arrow[d, "j"'] \arrow[r, "\chi_1"]  & I(\chi_1 x_i) \arrow[d, "j'", dotted] \\
I(j x_i) \arrow[r, "\chi_2"'] & I(\chi_2 j x_i)
\end{tikzcd}
\]
Since $2 := \{0, 1\}$ is the initial object in boolean algebras, it suffices to show that we have an isomorphism of measure algebras
\[
I(\chi_1 x_i) \cong I(\chi_2 j x_i)
\]
for each $i$. Now both of these measure algebras are Maharam-type-homogeneous and have the same Maharam type, since $(M, \alpha)$ was Maharam-type-homogeneous. Moreover, the top element $1$ has the same measure in both algebras, so we can now use 331I in \cite{fremlin} in order to get our isomorphism.

\item A measure-preserving map $\chi:(\mathcal{P} X,\mu)\rightarrow (A,\mu)$ consists of precisely a partition of $(A,\mu)$ into finitely many elements of predetermined measure. But this is precisely the interval property for atomless measure algebras, see \ref{interval_examples}.

% \item $f_1(\mathcal{B}_1)$ and $f_2(\mathcal{B}_2)$ are subalgebras of $I$, so we may generate the smallest subalgebra of them, containing both. Define $\mathcal{B}_3=\langle f_1(\mathcal{B}_1),f_2(\mathcal{B}_2) \rangle $ with the measure induced by the Lebesgue measure. As $f_1(\mathcal{B}_1)$ and $f_2(\mathcal{B}_2)$ are isomorphism to $\mathcal{B}_1$ resp. $\mathcal{B}_2$, the diagram commutes. It remains to show that $\mathcal{B}_3$ is finite (resp. at most countable). This is obvious, however any element of it may be represented as the unions of intersections of atoms $b_1\wedge b_2$ of $b_1\in \mathcal{B}_1$, $b_2\in\mathcal{B}_2$.
\end{enumerate}
\end{proof}

\begin{remark}
Notice that by using 331I in \cite{fremlin} we have implicitly used the axiom of choice.
\end{remark}

\begin{corollary}\label{Galois} Let $(M, \alpha)$ be a homogeneous-Maharam-type probability algebra. Let $G$ be the group of automorphisms of $(M, \alpha)$ topologised via an algebraic base given by collections $\mathcal{M}_{\chi}:=\{f:u\overset{\sim}{\rightarrow} u\mid f\circ \chi=\chi\} $ of automorphisms fixing a finite partition $\chi: (A,\mu)\rightarrow (M, \alpha)$. Then we get an equivalence of toposes, which is induced as in \ref{olivia}:
\[\Sh(\FinProb, J_{at})\simeq \text{Cont}(G)\]
\end{corollary}
\begin{remark} In the case of the Lebesgue interval, its automorphisms are commonly known as \emph{measure-preserving dynamical systems}. This hints at a connection to ergodic theory.
\end{remark}
%It follows that the atoms of the topos correspond to open subgroups of $G$. We shall classify them. %give ref
\begin{proposition} The automorphism group of a homogeneous-Maharam-type probability algebra is simple by 383Ib \cite{fremlin}. In particular, all topos-theoretic invariants involving any sort of normal subgroup listed in \cite{caramello_lafforgue} are trivial.
\end{proposition}

Another feature of this description is that toposes of continuous group actions are quite well understood. The interest in researching them comes from their connection to set theory and representation theory. So called \emph{permutation models} are one of the main tools of forcing, and they will also appear later in this paper as another interpretation of $\Prob$. In a totally separate field of mathematics, a representation of a topological group on a $k$-vector space (with discrete topology) is nothing but an internal $k$-vector space \cite{XYZ} i.e. a sheaf of $k$-vector spaces in the topos of continuous group actions of that group.

Now that we have proved a non-trivial \emph{bridge}, we briefly discuss an application. We show that the universal model in $\Prob$ has not only finite meets and joins, but all meets and joins, in a sense to be defined.

\begin{definition} A sheaf $L$ of posets with finite meets and top element is called an \emph{internal locale} if the map
\[I: L\rightarrow \mathcal{P}(L) \]
sending ... has a right adjoint. An \emph{internal complete boolean algebra} is accordingly a sheaf of boolean algebras that is an internal locale.
\end{definition}

Our surprising result now follows by glueing some theorems from the literature.

\begin{theorem} The universal model of $\mathbb{T}_{int}$ is an internal complete boolean algebra.
\end{theorem}
\begin{proof}
We use the following equivalence of categories:
\[ \text{Cont}_\tau(\text{Aut}_{\BPAlg}(I,\lambda))\simeq \text{\Set}[\mathbb{T}_{int}]  \]
We can use Theorem 7.3 (and remark 7.2) \cite{caramello_lafforgue} %is this the correct ref?
 to see $(I,\lambda)$ is a special model of $\mathbb{T}_{int}$ and thus the universal model in $\text{Cont}_\tau(\text{Aut}(I,\lambda))$ is $(I,\lambda)$ with the canonical continuous group action.\newline
\indent Thus $U_{\mathbb{T}_{int}}$ is a complete boolean algebra acting on itself via automorphisms.  By C2.5.8(e) \cite{elephant} this proves that the universal model is an internal locale. Hence it is a complete boolean algebra.
\end{proof}

This theorem is remarkable as we get some completeness condition from definitions, which essentially only use statements about finite sets of variables. Nevertheless, we feel like it needs to be commented that the statement of this result might be a bit misleading at first sight. The reason is, that we will see in \ref{choice_failture}, that infinite families of variables often fail to exist inside $\Prob$.


\section{The atoms of $\Prob$ }\label{atoms}

Sheaves on sites are a very complicated data type. Not only does one need to give a set for each object in the site, one also has to specify functions between these set for any morphism in the site. On top of that, all this has to satisfy the sheaf condition. Similarly convoluted is the data of a morphism of sheaves.

Almost miraculously, this complexity can be reduced to next to non. This will require quite a lot of work though. We will see that any sheaf decomposes into a coproduct of \emph{atoms} and morphisms of sheaves are coproducts of maps between these atoms.

\begin{definition} An \emph{atom} of a topos is an object whose only two subobjects are trivial or itself. Note that constant sheaf of the empty set is not an atom.
\end{definition}

\begin{definition} Given a topos, the \emph{category of atoms} of a topos is the full subcategory of objects, which are atoms.
\end{definition}
\begin{theorem}
Given an atomic topos $\mathcal{E}$ and its category of atoms $\mathcal{E}_{at}$, then $\mathcal{E}_{at}$ fulfils the right Ore condition and we have
\[\Sh(\mathcal{E}_{at},J_{at})\simeq \mathcal{E} \]
More concretely, $\mathcal{E}$ is the $\infty$-positivisation of $\mathcal{E}_{at}$. This means any sheaf is a coproduct of atoms and any morphism of sheaves $f: F\rightarrow G$, where $F=\bigsqcup_{i\in M} A_i$ and $G=\bigsqcup_{j\in N} B_j$ for $A_i,B_j\in ob\mathcal{E}_{at}$, is a coproduct of maps $A_i\rightarrow B_{g(i)}$ in $\mathcal{E}_{at}$ for some function $g:M\rightarrow N$.
\end{theorem}
\begin{proof}
The statement is Proposition 4.21 of \cite{caramello}. % TODO: Why is this the same statement? Why is the topology on \mathcal{E}_{at} the atomic topology? There is at least some sort of commentary necessary here. Also, I don't like the usage of undefined terms like infinity positivasation and free completion, because it is not clear what that is even supposed to mean.
\end{proof}
We can quickly give a first description of the category of atoms in our case. But this will be not very workable.
\begin{proposition} Given a topological group $(G,\tau)$, the category of atoms of the topos $\text{Cont}_\tau (G)$ is equivalent to its subcategory of transitive, continuous actions. \cite{XYZ}
\end{proposition}
As our topos is equivalent to $\text{Cont}_\tau(\text{Aut}_{\BPAlg}(I,\lambda))$, this immediately gives a description of its atoms.
But again, it would be nice to have a more combinatorial, workable interpretation of these objects. First we need to classify the atoms (as sheaves on the atomic site on $\FinProb$) and thereby inadvertently the open subgroups of our topological groups.
\newline
\indent We have already seen some of the atoms: $y (X,\mu)$ for any finite probability space $(X,\mu)$. Any morphism $y (X,\mu)\rightarrow A$ for an atom $A$ is necessarily surjective, else its image would be a third subobject. As $A$ is not constantly $\emptyset$ and by the Yoneda lemma, such a map exists. Toposes are effective categories by IV.7.8 \cite{sheaves_geometry_logic}, so there exists an equivalence relation $R$ such that the following fork is a coequalizer diagram:
\begin{center}

\begin{tikzcd}
R \arrow[r, hook] & {y (X,\mu)\times y (X,\mu)} \arrow[r, "\pi_1", shift left] \arrow[r, "\pi_2"', shift right] & {y (X,\mu)}\arrow[r]&A
\end{tikzcd}
\end{center}

To exploit this, we will utilize the combinatorial method outlined in \cite{caramello_lafforgue} Prop 6.7. For this, we will need to understand internal equivalence relations on the sheaves $yU_{r_1\cdots r_n}$. We use \ref{multi-product} to yield the following description of an equivalence relation. \newline
\indent A relation is a subobject
\[R\hookrightarrow yU_{r_1\cdots r_n}\times yU_{r_1\cdots r_n}=\bigsqcup_{\substack{\sum_i t_{ij}=r_j \\ \sum_j t_{ij}=r_i}  }yU_{t_{ij}}\]
As these representable functors are atoms, this is equivalent to giving a subset of the set $S_{r_1\cdots r_n}:=\{(t_{ij})_{0\leq i,j \leq n} \mid \sum_i t_{ij}=r_j,\, \sum_j t_{ij}=r_i \}$ of matrices whose rows and columns sum to the $r_i$'s. We use Definition 6.5 (iii) \cite{caramello_lafforgue} to see that a relation is an equivalence relation iff it fulfils the following conditions:
\begin{enumerate}
\item Reflexivity:  The element induced by the diagonal $\Delta: yU_{r_1\cdots r_n}\rightarrow $\linebreak $ yU_{r_1\cdots r_n}\times yU_{r_1\cdots r_n}$ is in $R$ i.e. the following matrix is in $R$:
\[ \begin{bmatrix}
    r_{1}       & 0 & \dots & 0 \\
    0      & r_2 &  \dots &0 \\
    \vdots & \vdots &  \ddots& \vdots\\
    0       & 0& \dots & r_n
\end{bmatrix} \]
\item Symmetry: $R$ is invariant under swapping the factors of the product $ yU_{r_1\cdots r_n}\times yU_{r_1\cdots r_n}$ i.e. if $T\in R$ then so is its conjugate $T^\top$.
\item Transitivity: Given $(t^{(1)}_{ij})\in R$ and $(t^{(2)}_{jk})\in R$ and $(t_{ijk})$ corresponding to an atom of $yU_{r_1\cdots r_n}\times yU_{r_1\cdots r_n} \times yU_{r_1\cdots r_n}$ such that its images in the product of the first resp. last two components are $(t^{(1)}_{ij})$ resp. $(t^{(2)}_{jk})$ i.e.:
\[\sum_k t_{ijk}=t^{(1)}_{ij} \quad \sum_i t_{ijk}=t^{(2)}_{jk} \]
Then its image in the product of the first and third component lies in $R$ i.e.:
\[(t^{(3)}_{ik})\in R \text{ where }t^{(3)}_{ik}:=\sum_j t_{ijk}    \]
Geometrically:
%Geometrically, this means that for every $3$-dimensional matrix with values in $\mathbb{R}_{\geq 0}$, if the sums of the entries in two of the directions are  matrices in $R$, then so is the third:
\end{enumerate}
\begin{center}
\begin{tikzcd}[row sep=small, column sep= small]
             & t^{(2)}_{n1}                                  &              & t^{(2)}_{nn}                                                     &              &                                               &              \\
t^{(3)}_{n1} & t_{n11} \arrow[l, "\sum"'] \arrow[u, "\sum"'] & \cdots       & t_{n1n} \arrow[u, "\sum"']                                       &              &                                               &              \\
             & \vdots                                        & \ddots       & t_{11}^{(2)}                                                     & \ddots       & t^{(2)}_{1n}                                  &              \\
t^{(3)}_{nn} & t_{nn1} \arrow[l, "\sum"']                    & t^{(3)}_{11} & t_{111} \arrow[rd, "\sum"] \arrow[l, "\sum"'] \arrow[u, "\sum"'] & \cdots       & t_{11n} \arrow[rd, "\sum"] \arrow[u, "\sum"'] &              \\
             &                                               & \ddots       & \vdots                                                           & t^{(1)}_{11} & \vdots                                        & t^{(1)}_{1n} \\
             &                                               & t^{(3)}_{1n} & t_{1n1} \arrow[rd, "\sum"] \arrow[l, "\sum"']                    & \cdots       & t_{1nn} \arrow[rd, "\sum"]                    &              \\
             &                                               &              &                                                                  & t^{(1)}_{n1} &                                               & t^{(1)}_{nn}
\end{tikzcd}
\end{center}
\indent One can generate an equivalence relation by intersecting all those, which contain a given set of the matrices. This can be seen as some kind of \emph{game}, where on starts with some matrices and then constructs all other possible ones with these $3$ "moves".


\begin{remark}
$3$-dimensional non-negative real matrices whose rows sum to three prescribed matrices on the sides have been investigated in combinatorics literature under the name "\emph{3-way axial transportation polytope}", which they form as a subset of $\mathbb{R}^{n\times n\times n}$. See for instance \cite{3way}.\end{remark}%Do we need this?


\begin{definition} Given a non-negative real matrix $M\in \mathbb{R}^{n^2}_{\geq 0}$, define the \emph{graph }$\Gamma(M)$\emph{ of }$M$ as the bipartite graph on $\{1, \cdots, n\}\sqcup \{1, \cdots, n\}$ with an edge between $i$ and $j$ iff $M_{ij}\neq 0$. One can also interpret this as a $(0,1)$-matrix.
\end{definition}
\begin{lemma}\label{2x2x2} Given $0<r_1<1$, setting $r_2=1-r_1$, and  a matrix $\begin{bmatrix}
r_1-a & a\\
a &r_2-a
\end{bmatrix}$ with $0\neq a \leq r_1,r_2$, $a\neq 1/2$, the equivalence relation on $yU_{r_1 r_2}$ generated by it are already all matrices in $S_{r_1r_2}$.
\end{lemma}
\begin{proof} WLOG $r_1\geq r_2$. All matrices in $S_{r_1r_2}$ are of the form as in the statement of the lemma (without the restrictions $a\neq 0,a\neq  1/2$). If we set $t^{(1)}_{ij}=t^{(2)}_{jk}=\begin{bmatrix}
r_1-a & a\\
a &r_2-a
\end{bmatrix}$ then the matrix $t_{ijk}$ has to be if the following form:
\[t_{i1k}=\begin{bmatrix}
r_1-a-b & b\\
b & a-b
\end{bmatrix} \quad t_{i2k}=\begin{bmatrix}
a-c & c\\
c & r_2-a-c
\end{bmatrix}\]
for $b\leq \min \{a, r_1-a \}$, $c\leq \min \{a,r_2-a\}$. Hence:
\[ t_{ik}^{(3)}=\begin{bmatrix}
r_1-b-c &b+ c\\
b+c & r_2-b-c
\end{bmatrix}
\]
Setting $a'=b+c$, these are precisely all the matrices such that $a'\leq \min\{2a, r_1, r_2, r_1+r_2-2a   \}=\min \{2a,r_2, 1-2a \}$. We will iteratively expand the set of  values $a$ such that the equivalence relation generated by them is $S_{r_1r_2}$.
Clearly this holds for all $a\in [\frac{r_2}{2},\frac{ r_1}{2}  ]$ (and $a\leq r_2$ we will always implicitly assume this condition in what follows).\newline
\indent For $n\geq 1$ and $a\in [\frac{r_2}{2^{n+1}},\frac{r_2}{2^n})\cup (\frac{1}{2}-\frac{r_2}{2^n}, \frac{1}{2}-\frac{r_2}{2^{n+1}}] $, choose $a'=\frac{r_2}{2^n}$. Thus for any starting point $a\in (0,\frac{1}{2})$, we can generate, after finitely many steps, some $a\in  [\frac{r_2}{2},\frac{ r_1}{2}  ]$ and hence everything.
\end{proof}
\begin{theorem}
The atoms of the topos $\Prob$ correspond to tuples $(M, \mu, H)$ where $(M,\mu)$ is a finite probability space and $H\leq Aut(M,\mu)$ a subgroup of its automorphism group.
\end{theorem}
\begin{proof}
Given an equivalence relation $R$ on $yU_{r_1\cdots r_n},$ we will conclude the proof via a sequence of reduction steps.\newline
\newline
\emph{Step 1.} If there exists a matrix $M\in R$ such that the associated $(0,1)$-matrix is not a permutation matrix then there exists a node $l\in \{1,\cdots,n\} \sqcup\{1,\cdots,n\}$in its graph with at least two neighbours, WLOG, by reordering, the nodes $1$ and $2$. By symmetry, we may assume $l$ lies in the first component. Setting, as in the description of transitivity as before, $t^{(1)}_{ij}=M$, $t^{(2)}_{jk}=M^\top$, we seek to find an appropriate $n\times n \times n$-matrix for some matrix $L$ in the following block diagonal form
\[ \begin{bmatrix}
    a_{11}      & a_{12} & 0&\dots & 0 \\
    a_{21}     & a_{22} &  0&\dots &0 \\
    0 & 0& r_3 &\dots & 0\\
    \vdots & \vdots & \vdots &  \ddots& \vdots\\
    0       & 0& 0 & \dots & r_n
\end{bmatrix} \]
such that $a_{ij}\neq 0$. One can achieve this by setting for $j\neq l$: $t_{ijk}=\begin{cases}  m_{ij} &\text{if }i=k \\ 0 & \text{else}  \end{cases}$ and $(t_{ilk})_{0\leq i,k\leq n}$ to be the following matrix for some $\min\{m_{1l},m_{2l}\}>\epsilon> 0$:
\[ \begin{bmatrix}
    m_{1l}-\epsilon  & \epsilon & 0&\dots & 0 \\
  \epsilon     &m_{2l}-\epsilon &  0&\dots &0 \\
    0 & 0& m_{3l} &\dots & 0\\
    \vdots & \vdots & \vdots &  \ddots& \vdots\\
    0       & 0& 0 & \dots & m_{nl}
\end{bmatrix} \]
$L$ is then defined to be the sum of these matrices.
\newline
\newline
\emph{Step 2.} Now we can generate the smallest equivalence relation containing $L$. We set $t_{ij}^{(1)}=t^{(2)}_{jk}=L$ and construct all 3-dimensional matrices $t_{ijk}$ with these faces. Clearly, for tuples $ijk$ such that at least one $i>2$, $j>2$ or $k>2$, we must have $t_{ijk}=\begin{cases} r_i &\text{if }i=j=k \\ 0 &\text{else}  \end{cases}$. Hence the problem reduces (up to scaling) to the statement of the previous lemma \ref{2x2x2}. It is applicable as non of the entries are zero and hence the $a$, in the notation of the lemma, is neither $0$ nor $\frac{1}{2}$. The smallest equivalence relation containing $L$ is thus the set of all matrices in the same block-diagonal form as $L$. This can easily be seen to be the equivalence relation $R_{1,2}$ associated the quotient map  $yU_{r_1\cdots r_n}\rightarrow yU_{(r_1+r_2),r_3\cdots r_n}$ sending $1, 2\mapsto 1$ and $j\mapsto j-1$ for $j> 2$.
\newline
\newline
\emph{Step 3.} Replace $R$ on $yU_{r_1\cdots r_n}$ by  the equivalence relation $\tilde{R}$ on $yU_{(r_1+r_2),r_3\cdots r_n}$ defined as what is left over after quotienting out $R_{1,2}$. Repeat these steps until the condition of step 1 is no longer fulfilled. This will terminate as $n$ is finite.\newline
\newline
\emph{Step 4.} The $(0,1)$-matrices of all matrices in $R$ are permutation matrices. The conditions on matrices in $S$ impose that these matrices are automorphisms of $U_{r_1\cdots r_n}$. It remains to prove that they form a subgroup of $S_n$. One can check that $\sigma^\top=\sigma^{-1}$ and the only matrix that can appear as $t^{(3)}_{ik}$ if we set $t^{(1)}_{ij}=\sigma$ and $t^{(2)}_{jk}=\tau$, is $\sigma \tau^{-1}$. It also contains the unit of $S_n$ by reflexivity. Hence it is a subgroup.
\newline
\newline
This concludes the proof as all atoms are quotients of equivalence relations and the relations. The representable functors appear as $(X,\mu, \{\id\})$.
\end{proof}

\begin{lemma} \label{atoms_are_sheaves} Given a finite probability space $(X,\mu)$ and a subgroup $H$ of its automorphism group, we compute the sheaf-theoretic quotient of the corresponding equivalence relation in $\Sh(\FinProb,J_{at})$ to be:
\[ \mathcal{F} :(N,\nu)\mapsto\text{\FinProb}((N,\nu), (X,\mu))/\sim  \]
where $f\sim g$ if there exists $\sigma\in H$ with $ \sigma\circ f=g$. These are partitions up to permutation by elements in $H$.
\end{lemma}
\begin{proof}
One calculates coequalizers in sheaf topoi by calculating the section-wise coequalizer and then sheafifying. The quotient the equivalence relation $R$ associated to $U$ is given by the coequalizer of the composition of the maps
% TODO: Maybe explain previously what they quotients of equivalence relations are
\begin{center}

\begin{tikzcd}
\bigsqcup_{\sigma \in H}\y(X,\mu) \arrow[r, hook] & {\y (X,\mu)\times \y (X,\mu)} \arrow[r, "\pi_1", shift left] \arrow[r, "\pi_2"', shift right] & {\y (X,\mu)}
\end{tikzcd}
\end{center}
Here the components on the left are included as permutation matrices. These compositions are coproducts of the Yoneda embeddings of $\id: (X,\mu)\rightarrow (X,\mu)$ resp. $\sigma: (X,\mu)\rightarrow (X,\mu)$. Thus the quotient presheaf is the sheaf described in the statement.

Sheafification is not needed in our case however as the presheaf given in the statement is a sheaf:  We seek to apply the criterion \ref{sheafConditionWeak}. We need to check that the following is an equalizer diagram for any $f:(Z,\lambda)\rightarrow (Y,\nu)$:
\[
\begin{tikzcd} \mathcal{F} (Y,\nu) \arrow[r, "\mathcal{F}f"] & \mathcal{F} (Z,\lambda) \arrow[r, "\pi_1", shift left] \arrow[r, "\pi_2"', shift right] & \mathcal{F} (Z \times_f Z,\bar{\lambda})
\end{tikzcd} ,
\]

First notice that $\mathcal{F} f$ is injective and its image consists of precisely the $[s] \in \mathcal{F}(Z,\lambda)$ such that $s$ is constant on each fiber of $f$. We want to prove that these elements are precisely the ones with $\pi_1([s]) = \pi_2([s])$.

Since the diagram above always commutes, we just need to to prove that the elements $[s] \in \mathcal{F}(Z,\lambda)$ such that for some $\sigma \in H$, $s \circ \pi_1 = \sigma \circ s \circ \pi_2$, are already constant on the fibers of $f$. Elementwise, our assumption on $s$ is that for all $x,y$ with $f(x) = f(y)$ we have that
\[
    s (x) = \sigma (s y) .
\]

Notice that this immediately implies that $s$ must be constant on the fibers of $f$.
\end{proof}

\begin{remark} The automorphism groups aren't all that complicated. Note that $\text{Aut}(X,\mu)\simeq \prod_{r\in (0,1)} S_{\{x\in X\mid \mu(x)=r \}}$.
\end{remark}

Now we are able to describe the category of atoms of $\Prob$ in a very combinatorial manner.

\begin{theorem} The category $\Prob_{at}$ is equivalent to the following category. \begin{enumerate}
\item Objects are given by tuples $(M,\mu, V)$ where $(M,\mu)$ is a finite probability space and $V$ is a subgroup of its automorphism group.
\item Morphisms $[f]:(M,\mu, V)\rightarrow (N,\nu, U)$ are given by equivalence classses of measure-preserving functions $f:(M,\mu)\rightarrow (N,\nu)$ such that for any $\sigma\in V$ there exists a $\psi\in U$ with $f\circ \sigma =\psi\circ f $; with $f\sim g$ if there exists $\sigma\in U$ with $f=\sigma\circ g$.
\end{enumerate}
\end{theorem}
\begin{proof}
%We use Theorem 6.7 of \cite{caramello_lafforgue}.
We can Yoneda embed $\Prob_{at}$ into $\Prob$.  By the Yoneda lemma, a morphism $\y (M,\mu)\rightarrow \y (N,\nu)/U$ corresponds to an element of $(\y (N,\nu)/U)(M,\mu)$. This has been computed to be maps $(M,\mu)\rightarrow (N,\nu)$ up to permutation by $\sigma\in U$. A morphism $\y (M,\mu)/V \rightarrow \y (N,\nu)/U$ is simply a morphism such that $\y (M,\mu)\rightarrow \y (N,\nu)/U$ factors over the quotient map $\y (M,\mu)\rightarrow \y (M,\mu)/V$. This means it is a morphism $f:(X,\mu)\rightarrow (Y,\nu)$ such that for any $\sigma\in V$ there exists a $\psi\in U$ such that $f\circ \sigma =\psi\circ f $. Hence the statement follows.
\end{proof}

\begin{remark} This shows, in particular that the atoms $\y (X,\mu)/U$, $\y (X,\mu)/V$ for different subgroups $U$ and $V$, which are not conjugated to each other, are non-isomorphic. % is this true?
\end{remark}

\begin{definition} Denote the category given above by $\Prob_{at}$ and call it the atomic completion of $\FinProb$ in accordance with notation in \cite{caramello_lafforgue}.
\end{definition}
This yields a new site presentation, which we will see is extremely easy to work with.
\begin{corollary} \label{coprod_representation}
    $\Prob\simeq \Sh(\Prob_{at},J_{at})$. More concretely, $\Prob$ is the $\infty$-positivisation of $\Prob_{at}$. % TODO: What is this even supposed to mean???
\end{corollary}



%TODO: Insert subsection on group-action perspective on all of this here.


\section{$\Prob$ as a set-theoretical universe}
The findings of the last chapter are so striking, that they allow us to reformulate our constructions, which heavily featured topos theory, in such a way as to not mention topoi in any way whatsoever. The notation introduced there already hints to this possibility. We hope that this makes our theory understandable to a far greater audience. So this chapter is concerned with outlining a translation into the language of set theory.
\begin{definition}[ZFA]  A model of Zermelo-Fraenkel set theory with atoms (or urelements) is a model of the single-sorted first order language with equality relation $=$, membership relation $\in$ and a constant $A$, the set of atoms, with the following axioms:
\begin{center}\begin{tabular}{ |p{3.5 cm}|p{7.5 cm}| }
\hline
Decidability&  $\forall x. (x\in A\vee \neg(x\in A))$  \\ % This seems to be obsolete in classical interpretations
\hline
\Set & $\forall y. (\exists x.x\in y\implies \neg (y\in A))$\\
\hline
Extensionality & $\forall x,y. \neg(x\in A)\wedge \neg(y\in A)\implies [ x=y\iff \forall z.(z\in x \iff z\in y) ] $\\
\hline
Pairing & $\forall x,y \exists z. (x\in z \wedge y\in z)$ \\
\hline
Separation & $\forall x \exists y. \neg (y\in A)  \wedge\exists z. (z\in y\iff z\in x \wedge \phi)$ for $x$ not free in $\phi$. \\
\hline
Union &$\forall x \exists y\forall z. (z\in y\iff \exists w\in x.z\in w)$ \\
\hline
Power-set &$\forall x\exists y \forall z. (z\in y\iff \forall w\in z.w\in x)$ \\
\hline
Infinity & $\exists x(\exists y.y\in x\wedge \forall y\in x.\exists w\in x.y\in w)$\\
\hline
$\in$-induction &$\forall x.(\forall y\in x. \phi(y)\implies \phi(x))\implies \forall x.\phi(x)$ \\
\hline
Collection & $\forall x (\forall y\in x\exists w.\phi\implies \exists z\forall y\in x \exists w\in z. \phi)$\\
\hline
\end{tabular}%what is phi?
\end{center}
\end{definition}
\begin{proposition}\label{ZFA} The internal language of a two-valued atomic topos is a classical model of ZFA.
\end{proposition}
\begin{proof}
This is essentially proved in \cite{set_theory}.
Let $A$ be the coproduct of all the atoms (i.e. one of each isomorphism class).
 Equality is equality but constructing a global membership relation from the datum of a topos is a bit less easy.\newline
\indent We can get bounded membership relations $\in_X\hookrightarrow X\times \Omega^X$ using the cartesian closed structure of our topos.\newline
\indent Now one uses an analogue of the cumulative hierarchy, starting with the set of atoms and then taking power objects and directed colimits just as one would in set-theory. The details can be found in \cite{set_theory}.
\end{proof}
\begin{remark} Models of ZFA like the one given by $\Prob$ are known as \emph{Fraenkel-Mostowski models} or \emph{permutation models}.
\end{remark}
%Maybe remark that this datum of a set theory is equivalent to that of a topos. Quote the paper corresponding to this fact
\begin{theorem}
In the combinatorial interpretation of our topos we have that $A$ is interpreted as \\\[\bigsqcup_{\substack{0<r_1\leq  \cdots\leq r_n \\ \sum_i r_i=1 \\ [V]\text{ conjugacy class of subgroup }V\subset Aut(U_{r_1\cdots r_n})}} yU_{r_1\cdots r_n}/V\]%it would be better to choose one subgroup per conjugacy class
 with element-hood relation and equality given as in \ref{ZFA}.
 \end{theorem}
 This puts the previous intuition that our topos consists of \emph{sets parametrized by partitions of unity (with subgroups of permutations)} on a firm footing.
\begin{remark}[Non-standard probability theory] We can also use language analogous to that used in the set theoretic constructions of non-standard analysis here \cite{XYZ} . One may call sets containing only elements of the form $yU_1$ \emph{standard sets} and these containing at least one different atom \emph{non-standard}. This works well as the following theorem shows. %Maybe also define "standard parts" of a set as the global sections i.e. the yU1 part. This preserves at least finite limits. Also one asign to an internal set its set of atoms i.e the left adjoint to the inclusion of standard sets. This doesn't preserve finite limits however.
\end{remark}
\begin{theorem} If there is any statement of higher order logic $\phi$ where all quantification is bounded over \emph{standard} sets then $\Prob\vDash \phi \iff \text{\Set}\vDash \phi$.
\end{theorem}
\begin{proof}
We essentially use that the topos $\Prob$ is atomic. This means, that the inverse image functor $\Delta: \text{\Set}\rightarrow \Prob$ of the global sections functor is logical. This means it preserves higher order logic \cite{XYZ}. Now we use the site $\Prob\simeq \Sh(\FinProb,J_{at})$. Given a set $A$, $\Delta(A)$ is the sheafification of the constant presheaf with values $A$ by \cite{XYZ}. This presheaf can be given as $\bigsqcup_{a\in A}yU_1$, which is already a sheaf as the site is subcanonical.
Hence an object in $\Prob$ is in its essential image iff it is a standard set.
\end{proof}
This means, dealing with standard sets is really cheap and easy. Quite the contrast to the monstrous descriptions of e.g. power sets of non-standard sets we have seen above. This has some immediate applications.
\begin{example} The natural numbers $\mathbb{N}$ of $\Prob$ are a standard set. In particular, all of arithmetic works just the same. %Is the same true for reals? I believe so.
\end{example}
\begin{proof}
The natural numbers object of a Grothendieck topos is always the constant sheaf with value $\mathbb{N}$. \cite{XYZ}.
\end{proof}
Given a probability interval $(\mathcal{B},\mu)$, we get an interpretation (is this the right word?) of $\Prob$ in $\text{\Set}$. %Do this properly with proper language
\begin{proposition}\label{choice_failture} The internal language of our topos proves the negation of countable choice.
\end{proposition}
\begin{proof} We construct a countable product of non-empty objects, which is empty. Take $yU_{1/n}$ to be the representable functors of the finite probability space with two elements and measure $1/n$ on one of them. Then the multi-limit of this family is empty as there is no finite probability space with a sequence of elements $x_n$ with measures $1/n$. We conclude $\prod_n yU_{1/n}=0$.
\end{proof}

This proof can, in fact be adapted in many situations, to suggest that most countable products of objects are empty. So there is really not much hope to extend the transfer principle to statements containing countably infinitely many variables or more.
\begin{remark} All this is not too exotic, so in practice one may just pretend to work formally in ZFA as one usually pretends to do so in ZFC. The only thing one has to be vary of is the failure of the axiom of choice. But as the proof of the last proposition suggests, the failure of the axiom of choice can be strictly controlled using fairly straight forward multi-product calculations.
\end{remark}


\section{Outlook for further research}

Sheaves and shit maybe? The Grothendieck construction and shit. I don't know how much of it we should mention. We could give the explicit site description and say we think it has all the nice properties. But the technical difficulties are too big and would take up too much time to give them in this paper etc.

Thinks that should go in here:
\begin{enumerate}
    \item $\mathfrak{Rand}$ and the Grothendieck construction. 'Random vectors spaces', 'random groups', etc. as vectors spaces, groups, etc. internal to $\mathfrak{Rand}$.
    \item Difficulties in looking at $L^0$, despite internal completeness. Discussion of the failture of the axiom of choice. Non-open stabilizers.
    \item Philosophically, argue for a solution using internal sheaves over the simple functions, cite Vickers(and maybe someone else) and his ideas in formal topology(this must be explained very well). He does geometric mathematics in 'A monad of valuation locales' and also uses simple functions as a proxy for $L^0$.
    \item Far future: One might expect our 'canonical' framework for probability theory to have much better formal properties than models by intervals in $\Set$. Thus, geometry might be better behaved when using the universal $L^0$ as a base for 'random field stuff'(cite the random fields book!)
    \item A sure bet: Repeat the logical analysis in this paper for many other atomic topoi. More conceptual proofs for algebraically closed fields and real closed fields? Quantifier elimination in infinitary logic as a weaker version of usual q-elim.
    \item The technique that we use for proving that the simple functions are all geometrically equivalent looks extremely easy to reproduce in other contexts. E.g. free modules over algebraically closed fields?
    \item Emulate ideas in this paper by considering $L^2$ equipped with the action of $Aut(I,\lambda)$ (Koopmann operator). "Can only ask questions about distributions", as one should.
\end{enumerate}


\begin{thebibliography}{9}
\bibitem{sheaves_geometry_logic}
Saunders Mac Lane, Ieke Moerdijk. \textit{Sheaves in Geometry and Logic} A First Introduction to Topos Theory.
\bibitem{elephant}
ELEPHANT
\bibitem{caramello_book}
CARAMELLO
\bibitem{fremlin}
FREMLIN
\bibitem{riehl}
Category theory in context
\bibitem{caramello_lafforgue}
Caramello, Olivia, and Laurent Lafforgue. "Some aspects of topological Galois theory." Journal of Geometry and Physics 142 (2019): 287-317.
\bibitem{caramello}
 Caramello, Olivia. "Topological Galois Theory". arXiv e-prints (2013):  1301.0300
\bibitem{set_theory}
Michael P. Fourman. "Sheaf models for set theory". Journal of Pure and Applied Algebra 19 (1980): 91 - 101
\bibitem{matrix}
Brualdi, R."Combinatorial Matrix Classes".Encyclopedia of Mathematics and its Applications. Cambridge  (2006): Cambridge University Press.
\bibitem{3way} Jesús A. De Loera and Edward D. Kim and Shmuel Onn and Francisco Santos. "Graphs of transportation polytopes". Journal of Combinatorial Theory, Series A 116 8 (2009): 1306-1325
\end{thebibliography}




\end{document}