text:
\begin{document}

\maketitle

\begin{abstract}
Boolean valued models for a signature $\mathcal{L}$ are generalizations of $\mathcal{L}$-structures in which we allow the
$\mathcal{L}$-relation symbols to be interpreted by boolean truth values. For example, for elements $a,b\in\mathcal{M}$ with
$\mathcal{M}$ a $\bool{B}$-valued $\mathcal{L}$-structure for some boolean algebra $\bool{B}$,
$(a=b)$ may be neither true nor false, but get
an intermediate  truth value in $\bool{B}$.
In this paper we expand and relate the work of Mansfield and others on the semantics of boolean valued models,
and of Monro and others on the adjunctions between $\bool{B}$-valued models and $\bool{B}^+$-presheaves for a boolean algebra
$\bool{B}$.
First of all we introduce a topological characterization of the sheafification process
for presheaves on topological spaces induced by the dense Grothendieck topology.
On the way to produce our characterization, we also relate the notion of open continuous mapping between topological spaces to that of complete homomorphism between complete boolean algebras, and to that of
adjoint homomorphism between boolean algebras (e.g. an homomorphism which has a left adjoint, if seen as a functor between partial orders/categories).
Next we link these topological/category theoretic results to the theory of boolean valued models.
First of all we give a different proof of Monro result identifying topological presheaves on Stone spaces with boolean valued models, and sheaves (according to the dense Grothendieck topology) with boolean valued models having the \emph{mixing property}.
Next we give an exact topological
characterization (the so called \emph{fullness property}) of which boolean valued models satisfy
\L o\'s Theorem (i.e. the general form of the Forcing Theorem
which Cohen ---Scott, Solovay, Vopenka--- established for the special case given by the forcing method in set theory).
Then we separate the fullness property from the mixing property, by showing that the latter is strictly stronger.
Finally we give an exact categorical characterization of which
presheaves correspond to full boolean valued models in terms of the structure of global sections of their associated \'etal\'e space.
\end{abstract}

\section*{Summary of main results}
This paper analyzes the correspondences existing between boolean valued models and presheaves on boolean algebras. Our aim is to lay foundations for bridging the gap between set theorists and category theorists, and to bring to light the deep connections of the boolean valued approach to forcing
with sheaf theory.
We start giving a brief summary of the main results (in some cases we are forced to be inaccurate or cryptic as the precise formulation of many of our theorems requires a terminology that cannot be given rightaway):

\begin{enumerate}
\item \label{equiv:boo}
We show that there exists an adjunction
between the category of boolean valued models (see Definitions \ref{def:boolvalmod}, \ref{def:boolvalmorph})
and the category of \emph{separated}\footnote{
A presheaf is separated if any compatible family of local sections admits at most one collation.}
presheaves on Stone spaces with homomorphism induced by \emph{open} continuous mappings (Theorem \ref{thm:adjbvmodpresh}); moreover this adjunction specializes
to an equivalence of categories between the family of \emph{extensional} boolean valued models (Definition
\ref{def:boolvalmod}) and the separated presheaves
in which all local sections are restrictions of global sections (Corollary \ref{thm:adjbvmodpresh}); note that (up to boolean
isomorphism) every
 boolean valued model is extensional.  In this correspondence, models with the mixing
property (Definition \ref{def:mixprop})
are sheaves according to the dense Grothendieck topology, and conversely (Proposition \ref{chr:mix}).
Our result is the special case for boolean algebras of a more general result by Monro \cite[Theorem 5.4]{MONRO86} which proves the existence of an equivalence of categories between Heyting valued models and presheaves defined on topological spaces.
Our direct proof in terms of boolean valued models has the advantage of being accessible to
set theorists as well as to category theorists.
\item \label{full:mix} We investigate the basic features of boolean valued models and their semantics, separating the mixing property and the fullness property (Definition \ref{def:fullness-wellbehaved}); the latter
identifies those $\bool{B}$-valued models for which \L o\'s Theorem ---equivalently  the Forcing Theorem--- holds. Specifically we show that every model with the mixing property is full (Proposition \ref{ful:mod}), that this implication is strict
(Example \ref{non:mix}), and that not all
boolean valued models are full (Example \ref{ex:ana}).
We also find a simple topological property characterizing the fullness property (Theorem \ref{thm:charLosThm}).
\item \label{etal:sp}
With the aim of clarifying further the distinction between fullness and mixing property,
we characterize the fullness property elaborating more on our correspondence between $\bool{B}$-valued models and presheaves,
and taking into account the notion of \'etal\'e space; in particular we use the
following characterization of topological sheaves: a fixed presheaf $\F$
on a topological space $(X,\tau)$ is a topological sheaf if and only if  the global sections of the associated \'etal\'e space are exactly described by the elements of $\F(X)$
\cite[Section II.5, Theorem 1]{MacLMoer}.
Given a $\bool{B}$-valued model $\M$ for a first order language $\LL$,
to every $\LL$-formula $\nphi(\overline{x})$ we associate a presheaf $\G^\nphi_\M$ on
the clopen
$N_{b_\nphi}$ in the Stone space $\St(\bool{B})$ of ultrafilters of $\bool{B}$ (where $b_\nphi$ is the boolean value given to the existential formula
$\exists\overline{x}\nphi(\overline{x})$, and $N_b$ is the clopen subset of $\St(\bool{B})$ given by the ultrafilters to which
$b$ belongs). Roughly the local sections of $\G^\nphi_\M$ are given by the tuples $\ap{\sigma_1,\dots,\sigma_n}$ such that $\Qp{\nphi(\sigma_1,\dots,\sigma_n)}>0_\bool{B}$.
We show that $\M$ is full exactly when, for every formula $\nphi$, the \'etal\'e space associated to $\G^\nphi_\M$ has \emph{at least one} global section
(Theorem \ref{chr:ful}).
\item \label{diff:sheaf}
To obtain the above characterizations of fullness and mixing property,
we introduce a topological construction of the sheafification process induced by the dense Grothendieck topology (which we call the \emph{stonean sheafification}). This construction is performed by means of \'etal\'e spaces (as described in \cite[Section II.5]{MacLMoer}
- see Definition \ref{def:etbund1}).
On the way to produce our characterization (given by Proposition \ref{prop:charLambda1}, Corollary \ref{cor:adjEDCH}, Theorem \ref{thm:gamma1adj})
we also relate the notion of open continuous mapping between topological spaces, to that of complete homomorphism between complete boolean algebras, to that of
adjoint homomorphism between boolean algebras (e.g. an homomorphism of boolean algebras which -seen as a functor between partial orders/categories- has a left adjoint - Theorem \ref{thm:adj-dual-cbaTDCH} and Propositions \ref{prop:openadjpairs} \ref{thm:openmap-->adjoint} in Section \ref{sec:dual}). Furthermore we characterize the extremally disconnected compact Hausdorff spaces as those spaces which are the Stone-\v{C}ech compactification of any of their dense subsets (Proposition \ref{comp:exdisc}).
We also relate our construction to
standard completion processes performed in functional analysis/general topology (Examples \ref{exm:keyetsp} and \ref{exm:sheafLR}) and outline in which ways our topological construction of the stonean sheafification for topological spaces differs from the standard one described in \cite[Section II.5]{MacLMoer}.
Roughly our construction is strictly grounded
in classical logic in that  it  is naturally correlated to a boolean valued semantics on topological presheaves rather than a Heyting valued semantics.
\end{enumerate}

\section*{Forcing, boolean valued models, and sheaves}
Boolean valued models constitute one of the classical approaches to forcing \cite{BELL,JECH}.
They also give a useful method for producing new first order models of a theory; for example the standard ultrapower construction is
just a special instance of a more general procedure to construct boolean valued elementary extensions of a given structure
(see \cite{VIAUSAX} or \cite{MANS71}).
Many interesting spaces of functions (for example $L^\infty(\mathbb{R}), C(X)$ etc.) can be naturally endowed of
the structure of a $\bool{B}$-valued model; for example set $\Qp{f=g}=\qp{\bp{x\in \mathbb{R}: f(x)=g(x)}}_{\bool{MALG}}$
for $f,g\in L^\infty(\mathbb{R})$, where $\bool{MALG}$ is the complete boolean algebra given by
Lebesgue measurable sets modulo Lebesgue null sets; $\Qp{f=g}$ gives a natural measure of the degree of equality
subsisting between $f$ and $g$. In particular by means of boolean valued models one can expect to employ logical methods to analyze
the properties of these function spaces. This can be fruitful, see for example \cite{VIASCHANUEL} or
\cite{MR779056,MR759416,VIAVAC15}.\\
The aim of this paper is to systematize these results and connect them to sheaf theory, in doing so we give a direct proof in terms of boolean valued models of the boolean case of a result of Monro\footnote{We note that we became aware of Monro's results only after preparing the first version of this paper. We thank Greta Coraglia for bringing Monro's work to our attention.} \cite[Theorem 5.4, Proposition 5.6]{MONRO86} (contribution \ref{equiv:boo} above), and we expand and develop this result (contributions \ref{full:mix}, \ref{etal:sp}, \ref{diff:sheaf} above). Our long-stretched hope is that this is a first step towards a fruitful transfer of techniques, ideas and results arising in set theory in the analysis of the forcing method to other domains where a sheaf-theoretic approach to problems is useful.\\
This paper (while written by scholars whose mathematical background is rooted in set theory) is aimed primarily at readers with some expertise in category theory and familiarity with first order logic. We emphasize that
\emph{no knowledge or familiarity with the forcing method as presented in \cite{BELL,JECH,KUNEN} is required} to follow the proofs and statements of the main results.
We will sporadically relate our results to the forcing machinery through some examples (see in particular Examples
\ref{ex:fullnotimplmix}, \ref{ex:fullnotimplmix2}, \ref{exm:sheafLR}) and a few comments,
but that's all. The reader unfamiliar with the forcing method can safely skip them without compromising the comprehension of the main body of this article. \\
Let us spell out more precisely the outcomes of \cite{MR779056,MR759416,VIAVAC15,VIASCHANUEL} for what we will do here.
\cite{MR779056,MR759416,VIAVAC15} show
that there is a ``natural'' identification between:
\begin{itemize}
\item the unit ball of commutative real $C^*$-algebras of the form $C(X)$ with
$X$ compact Hausdorff extremally disconnected;
\item
the $\RO(X)$-names for the unit interval
$[0;1]$ as computed in the forcing extension $V^{\RO(X)}$ of $V$ given by $\RO(X)$ (where $\RO(X)$ denotes the complete boolean algebra of regular open subsets of $X$).
\end{itemize}
In
\cite{VIASCHANUEL} these results are applied to establish a weak form of Schanuel's conjecture on the transcendence
property of the exponential function over the complex numbers.
One of the outcomes of the present paper combined with \cite{VIAVAC15}
will be that the sheafification of the presheaf given by the essentially bounded measurable functions defined on some
measurable subset of $[0;1]$ is exactly given by the sheaf associated to the boolean valued model describing the real
numbers in $[0;1]$ which exist in $V^{\bool{MALG}}$ (see Example \ref{exm:sheafLR}).
These results are just samples of the various roles boolean valued models can play across different mathematical fields,
and why we strongly believe it can be useful to develop a flexible translation tool to relate concepts expressed in rather
different terminology in differents set-up. This is more or less all we will say on the relation between the results of the present paper and forcing. Let us now move to a detailed presentation of our results.

\section*{Structure of the paper}
The paper is organized as follows:
\begin{itemize}
\item Section \ref{sec:prereqbatopsppreord} gives prerequisites on topology, boolean algebras, partial orders.
\item Section \ref{sec:dual} explores the connections between the notion of open continuous map, that of complete homomorphism between complete boolean algebras and that of adjoint homomorphism between boolean algebras (the latter is an homomorphism which seen as a functor among partial orders/categories has a right adjoint).
\item Section \ref{sec:sh} presents our topological construction of the sheafification (stonean sheafification) of a topological presheaf with respect to the dense Grothendieck topology.
\item Section \ref{sec:boolvalmod} gives a rapid presentation of the key properties of boolean valued models.
\item Section \ref{sec:pres} establishes a correspondence between boolean valued models with morphisms and topological presheaves on Stone spaces, which specializes to a duality between boolean valued models with the mixing property and stonean sheaves.
\item Section \ref{sec:charfulletalespace} gives a categorical characterization of the fullness property of boolean valued models in terms of properties of the bundles associated to their presheaf structure.
\end{itemize}

\tableofcontents

\section{Boolean algebras, partial orders, topological spaces, compactifications}\label{sec:prereqbatopsppreord}

In this section we gather a number of folklore results on boolean algebras, partial orders, topological spaces we will use freely along the remainder of the paper. We include proofs of those non-trivial results for which we are not able to trace a reference in the literature. For non-trivial results whose proof is omitted we give appropriate references.

\subsection{Basics on boolean algebras, partial orders, topological spaces}
We recall some basic facts and terminology about boolean algebras, Heyting algebras, partial orders, compact spaces. The missing proofs can be found in \cite{JECH, viale-notesonforcing}.

Given a topological space $(X,\tau)$
and $A$ subset of $X$, $\Reg{A}$ is the interior of the closure of $A$ in $(X,\tau)$.
$A$ is \emph{regular open} if $A=\Int{\Cl{A}}=\Reg{A}$.
$\RO(X,\tau)$ (in short $\RO(X)$ if $\tau$ is clear from the context) denotes the family of regular open subsets of $(X,\tau)$.
$\CLOP(X,\tau)$ (or just $\CLOP(X)$ if $\tau$ is clear from the context) denotes the family of clopen subsets of $(X,\tau)$.
Clearly $\CLOP(X)\subseteq\RO(X)$.
$\mathcal{O}(X,\tau)$  (or just $\mathcal{O}(X)$ if $\tau$ is clear from the context) is $\tau\setminus\bp{\emptyset}$.

By the Stone Representation Theorem (see for instance \cite[Theorem 2.2.32]{viale-notesonforcing} or \cite[Theorem 7.11]{JECH}), every boolean algebra $\bool{B}$ is isomorphic to the boolean algebra
$\CLOP(\St(\bool{B}))$ of the clopen subsets of its Stone space
$\St(\bool{B})$.
The latter is the compact Hausdorff zero-dimensional space
whose points are the ultrafilters on $\bool{B}$, topologized by taking as a base the family of sets
$N_b:=\bp{G\in\St(\bool{B}): b\in G}$ for some $b\in\bool{B}$. These sets are actually the clopen sets of $\St(\bool{B})$.
\begin{notation}\label{not:stonespaces}
For the remainder of this paper, when dealing with Stone spaces $X$ (i.e. $0$-dimensional compact Hausdorff spaces) it is convenient to look at points of $X$ at times as elements of their clopen neighborhoods and at times as ultrafilters on $\CLOP(X)$ as the Stone duality naturally identifies each point of $X$ to the ultrafilter on $\CLOP(X)$ given by its clopen neighborhoods. Thus we will write $G\in U$ for $U\in\CLOP(X)$ and $G\in \St(\CLOP(X))$ if we see $G$ as a point in $X$, and $U\in G$ if we see $G$ as an ultrafilter on $\CLOP(X)$.
\end{notation}

Given a topological space $(X,\tau)$,
$\RO(X)$ is endowed of the structure of a complete boolean algebra by letting
\begin{itemize}
\item
$0_{\RO(X)}:=\emptyset$, $1_{\RO(X)}:=X$,
\item
 for $U, V\in\RO(X)$
\begin{gather*}
U\vee V:=\Reg{U\cup V}, \\
U\wedge V:=U\cap V, \\
\neg U:=X\setminus\Cl{U}.
\end{gather*}
\item
for any family $\bp{U_i: i\in I}\subseteq\RO(X)$
\begin{gather*}
\bigvee_{i\in I}U_i:=\Reg{\bigcup_{i\in I}U_i}, \\
\bigwedge_{i\in I}U_i:=\Reg{\bigcap_{i\in I}U_i}.
\end{gather*}
\end{itemize}
\begin{fact}
\label{comp:bool}
A boolean algebra $\bool{B}$ is complete if and only if $\CLOP(\St(\bool{B}))=\RO(\St(\bool{B}))$ (i.e. if and only if the space $\St(\bool{B})$ is extremally disconnected).
\end{fact}
See \cite[Prop. 3.2.12]{viale-notesonforcing} for a proof.
\begin{remark}
Let $\bp{N_a: a\in A}$ be a family of basic open sets in the Stone space $\St(\bool{B})$ of a boolean algebra $\bool{B}$ such that $\bigvee A$ exists. Then $\bigcup_{a\in A}N_a$ is a dense open set in the clopen set $N_b$ of $\St(\bool{B})$ if and only if $\bigvee_{\bool{B}} A=b$. However, $\bigvee A=b$ holds also in case
$\bigcup_{a\in A}N_a\neq N_b$.
In case $\bool{B}$ is complete,
\[\Reg{\bigcup_{a\in A}N_a}=N_{\bigvee A}.\]
\end{remark}

Given a pre-order $(P, \leq)$, we endow it with the downward topology $\tau_P$:
given $X\subseteq P$,
\[
\downarrow X:=\{p\in P: \textit{ there exists } x\in X \textit{ such that } p\leq x\}.
\]
$X\subseteq P$ is a \emph{down-set} if $X=\downarrow X$. \\
The family $\down(P)$ of the down-sets of $P$ is a topology for $P$, the \emph{downward topology}.
\begin{definition}
\label{def:emb}
An embedding of pre-orders $f:P\to Q$ is an order and incompatibility preserving map, i.e. a map satisfying the following two conditions:
\begin{itemize}
\item if $p_1\leq p_2$ in $P$ then $f(p_1)\leq f(p_2)$ in $Q$;
\item if $p_1\bot p_2$ (i.e. there is no $s\in P$ such that $s\leq p_1$ and $s\leq p_2$) then $f(p_1)\bot f(p_2)$.
\end{itemize}
$f$ is \emph{dense} if $\ran(f)$ is dense in $Q$ endowed with the downward topology.
\end{definition}
Note that an embedding need not be injective: for example, $U\mapsto\Reg{U}$ defines a non-injective (and surjective) embedding of $\tau$ into $\RO(X,\tau)$ provided $\tau\supsetneq\RO(X,\tau)$.

\begin{definition}
A pre-order $P$ is:
\begin{itemize}
\item
\emph{separative} if, for every $p, q\in P$, $p\nleq q$ implies that there exists $r\in P$ such that $r\leq p$ and $r\bot q$;
\item
\emph{upward complete} if it admits suprema for all its non-empty subsets.
\end{itemize}
\end{definition}

Observe the following:
\begin{itemize}
\item Given $(X,\tau)$ a topological space, $\tau$ is an upward complete preorder.
\item If $\bool{B}$ is a boolean algebra, then $\bool{B}^+:=\bool{B}\setminus\{0_\bool{B}\}$ with the induced order is a separative ordered set.
\item A boolean algebra $\bool{B}$ is complete if and only if $\bool{B}^+$ is upward complete.
\item If $P$ is a pre-order, we can always surject it onto a separative pre-order via an order and incompatibility preserving map.
\end{itemize}
\begin{definition}
The \emph{boolean completion} of a partial order $(P,\leq)$ is a complete boolean algebra $\bool{B}$ such that
there exists a dense embedding $e:P\to \bool{B}^+$.\\
 The \emph{boolean completion} of a boolean algebra $\bool{B}$ is the boolean completion of the separative order $\bool{B}^+$.
\end{definition}
\begin{theorem}
\label{boo:com}
If $P$ is a partial order, then $\RO(P,\tau_P)$
is its boolean completion, as witnessed by the map
\[
\begin{aligned}
e:&P\to\RO(P).\\
&p\mapsto \Reg{\downarrow p}.
\end{aligned}
\]
Moreover the boolean completion of $P$ is unique up to isomorphism.
\end{theorem}
\begin{proof}
See the proof of \cite[Theorem 14.10]{JECH} or \cite[Theorem 4.3.1]{viale-notesonforcing}.
\end{proof}
\begin{fact}
\label{alg:com}
Every boolean algebra $\bool{B}$
can be densely embedded in the complete boolean algebra
$\RO(\St(\bool{B}))$
via the Stone duality map
\[
b\mapsto N_b=\bp{G\in\St(\bool{B}):\, b\in G}
\]
which identifies $\bool{B}$ with $\CLOP(\St(\bool{B}))$.
The image is dense because the clopen sets form a base for the topology on
$\St(\bool{B})$. \\
Moreover $\RO(\bool{B}^+,\tau_{\bool{B}^+})\cong\RO(\St(\bool{B}))$
via the unique extension of the map defined on
$\bool{B}^+$ by $b\mapsto N_b$.
\end{fact}

We also recall that a topological space is $T_1$ if any two distinct points can be separated by open sets which contain exactly one of them; it is extremally disconnected if the closure of an open set is open, it is
$0$-dimensional (or totally disconnected) if the clopen sets form a base for the space.

\begin{fact}
Let $(X, \tau)$ be a $T_1$ topological space. Then:
\begin{itemize}
\item if $X$ is $0$-dimensional, it is Hausdorff;
\item if $X$ is Hausdorff, extremally disconnected, it is $0$-dimensional;
\item $X$ is extremally disconnected if and only if $\CLOP(X)=\RO(X)$.
\end{itemize}
\end{fact}
Extremally disconnected compact Hausdorff spaces are also called \emph{stonean} spaces.

We also need the following characterization of  of the regularization operation (see \cite[Lemma 3.2.6]{viale-notesonforcing}):
\begin{lemma}\label{lem:charreg}
Let $(X,\tau)$ be a topological space and $A\subseteq X$. Then its regularization $\Reg{A}$ is the set
\[
\bp{a\in X: \, \exists\, U\text{ open neighborhood of }a \text{ such that }A\cap U\text{ is dense in }U}.
\]
\end{lemma}

Using this characterization (and the fact that the image of a dense set under a continuous dense map\footnote{For us, a map between topological spaces is \emph{dense} if its image is dense in the codomain.} is dense) the following result is almost immediate:
\begin{fact}
Let $i:X\to Y$ be a dense topological embedding (e.g. an homeomorphism of $X$ with its image, which is dense in $Y$). Then $i$ implements an isomorphism of $\RO(Y)$ with $\RO(X)$ given by
$U\mapsto i^{-1}[U]$.
\end{fact}

\subsection{Adjunctions of preorders}

We also need to consider adjunctions of preorders.
The terminology we adopt comes from category theory (i.e.
adjoint functors for categories which are partial orders), and from the Stone duality, which establishes the correspondence between
homomorphisms of boolean algebras and continuous functions on Stone spaces.

\begin{definition}
\label{def:residuatedmappings}
Let $P,Q$ be partial orders and $i:P\to Q$, $\pi:Q\to P$ be order preserving maps between them.
The pair $(\pi, i)$ forms an \emph{adjoint pair} (or a \emph{monotone Galois connection}
or a \emph{pair of residuated mappings})
if for all $p\in P$ and $q\in Q$
\[
i(p)\geq q\text{ if and only if }\pi(q)\leq p.
\]
\end{definition}

\begin{fact}\label{prop:charadjpair}
Let $P,Q$ be partial orders and
$i:P\to Q$, $\pi:Q\to P$ be order preserving maps.
The following are equivalent:
\begin{enumerate}
\item  \label{prop:charadjpair-0}
$(\pi, i)$ is an adjunction;
\item \label{prop:charadjpair-1}
$\pi$ is defined by
\[
\pi(c)=\inf_{P}\bp{b\in P: i(b)\geq c},
\]
and $i$ is defined by
\[
i(b)=\sup_{Q}\bp{c\in Q: b\geq \pi(c)}.
\]
\end{enumerate}
Hence any order preserving map $i:P\to Q$ ($\pi:Q\to P$) can have at most one $\pi:Q\to P$ ($i:P\to Q$)
such that
$(\pi, i)$ is an adjoint pair.
\end{fact}

The proof is an easy application of the definition and is left to the reader.

\subsection{Hausdorff compactifications}

We now recall some basic facts about Hausdorff compactifications.

\begin{definition}
A triple $\ap{Y, \sigma,\iota}$  is a Hausdorff compactification of some topological space $(X,\tau)$ if
$(Y,\sigma)$ is a compact Hausdorff space and $\iota:X\to Y$ is a topological embedding with a dense image.

For $(X, \tau)$ a $T_0$-topological space, its Stone-\v{C}ech compactification (when it exists) is the unique Hausdorff compactification $\ap{Y,\sigma,\iota}$ of $X$
that has the following universal property: any continuous map $f:X\to K$ where $K$ is compact Hausdorff extends uniquely to a continuous map $\beta(f):Y\to K$ such that $\beta(f)\circ\iota=f$.
\end{definition}

The Stone-\v{C}ech compactification exists for a very large class of topological spaces $(X, \tau)$:

\begin{definition}
A topological space $(X,\tau)$ is \emph{Tychonoff} if for any $x\in X$ and $C$ closed subset of $X\setminus\bp{x}$ there is a continuous $f:X\to\mathbb{R}$ which vanishes on $x$ and gets value $1$ constantly on $C$.
\end{definition}

\begin{remark}
Every locally compact Hausdorff space is Tychonoff. Furthermore the Stone-\v{C}ech Compactification Theorem characterizes the spaces which are topologically homeomorphic to subsets of a compact Hausdorff space as the class of Tychonoff spaces.
\end{remark}

We spell out the details of one possible presentation of the Stone-\v{C}ech compactification.

\begin{notation}
Let $(X,\tau)$ be a topological space. $C\subseteq X$ is a \emph{$0$-set} if there is a continuous
 $f:X\to\mathbb{R}$ such that $C=f^{-1}[\bp{0}]$.\\
 We let $\mathcal{O}_0(X)$ denote the open sets which are complements of $0$-sets.
 \end{notation}

 \begin{remark}
Note that, for any topological space, the family of its $0$-sets is closed under finite unions and clopen sets are $0$-sets.
Also note that elements of $\mathcal{O}_0(X)$ can be described as the preimage of $[0;a)$
 for some $a<1$ and some continuous $f:X\to [0;1]$. \\
When $(X,\tau)$ is Tychonoff any closed set is the intersection of $0$-sets and also the intersection of open sets which are the complement of $0$-sets.
Hence in a Tychonoff space $\mathcal{O}_0(X)$ forms a base of open sets closed under finite intersections.
\end{remark}

For any topological space $(X,\tau)$, one can define
 the space $\beta(X)$ whose elements are the maximal filter of $0$-sets with topology $\beta(\tau)$ generated by
$\beta^c(U)=\bp{F\in\beta(X): \,\exists C\in F\, C\subseteq U}$ for $U\in\mathcal{O}_0(X)$.
The map $\iota_X:X\to\beta(X)$ maps any $x\in X$ to the maximal filter given by $0$-sets containing $x$.
This map is well-defined and injective provided the (singletons of) points of $X$ are the intersection of $0$-sets, and a local homeomorphism exactly when $X$ is Tychonoff;  in this latter case it can be shown that $\ap{\beta(X),\beta(\tau),\iota_X}$ is the Stone-\v{C}ech compactification of $(X,\tau)$ (see for instance \cite[Section 7.4]{viale-notesonforcing}).

We can sum up these informations as follows:
\begin{itemize}
\item $\iota_X[X]$ is homeomorphic to $X$ if and only if $X$ is Tychonoff;
\item $\iota_X[X]$ is open in $\beta(X)$ if and only if $X$ is locally compact and Hausdorff.
\end{itemize}

 The following follows almost immediately from the above observations:
\begin{fact}\label{fac:StCe-iso}
Assume $(X,\tau)$ is Tychonoff. Then $\RO(X,\tau)\cong\RO(\beta(X),\beta(\tau))$ via the map $U\mapsto U\cap X$ for $U\in \RO(\beta(X),\beta(\tau))$.
\end{fact}

 \subsection{Maximal filters of closed or open sets and Hausdorff compactifications}
 We now want to relate the points of Hausdorff compact spaces to (maximal) filters of topological sets.

\begin{definition}
Given a partial order $(P,\leq)$, a \emph{filter} on $P$ is an upward closed subset $G$ such that for any $p,q\in G$ there exists
$r\in G$ refining $p,q$.
\end{definition}
The guiding example of filter on a partial order $P$ is given by the family $G_x$ of open neighborhoods of a point $x\in X$  for $(X,\tau)$ a topological space and $(P,\leq)$ the partial order $\mathcal{O}(X)$ given by non-empty open sets of $(X,\tau)$.
This filter in general is not a maximal filter (consider the interval $[0;1]$ with the usual euclidean topology; the filter of open neighborhoods of $1/2$ is not maximal; it can be extended to a maximal filter containing $[0;1/2)$ and to another maximal filter containing $(1/2;1]$).
Moreover if $\mathcal{A}$ is a base of non-empty open sets for $X$, $G_x\cap\mathcal{A}$
is also a filter on the partial order $(\mathcal{A},\subseteq)$, but in general a maximal filter $G$ on
$\mathcal{A}$
may not identify a point of $X$: the intersection of the open sets in $G$ (or even of the closure of the open sets in $G$) may be empty (consider on $\mathbb{R}$ with the euclidean topology a maximal filter of open sets extending
$\bp{(a,+\infty):a\in\mathbb{R}}$). This identification of maximal filters of open sets to points of $X$
is clearly related to the existence of compactifications of $X$.
If $X$ is also compact any maximal filter $G$ on $(\mathcal{A},\subseteq)$ determines a unique point
$x$ of $X$ with $G\supseteq G_x\cap\mathcal{A}$, this point $x$ is the unique
element of the closed set $\bigcap\bp{\Cl{U}:U\in G}$.
However different maximal filters of open (or closed) sets
could determine the same point of $X$ (as shown by the case outlined above for $1/2$ in $[0;1]$).

We now compare various possible ways to describe points of some compactification of
a topological space. Typically we can identify a point of a compact Hausdorff space by means of:
\begin{itemize}
\item its open neighborhoods;
\item its regular open neighborhoods;
\item its open neighborhoods which are complements of $0$-sets;
\item the family of closed sets to which it belongs;
\item the family of $0$-sets to which it belongs;
\item the family of clopen sets to which it belongs (in case the space is $0$-dimensional).
\end{itemize}
Note that each of the above families detects a (maximal?) filter in the corresponding partial order under inclusion.
Hence given any topological space $(X,\tau)$ it is tempting to try to construct a Hausdorff compactification of $X$ whose points should be the maximal filters of one of the above families with respect to $\tau$. This is exactly what occurs
in the case of the above construction of the Stone-\v{C}ech compactification.

We are interested in comparing the above types of maximal filters and understand when these maximal filters define the same ``compactification''.
We now show that:
\begin{itemize}
\item\textbf{For any $(X,\tau)$, maximal filters on $\RO(X)$ naturally correspond to maximal filters of open sets:}
 assume towards a contradiction that some maximal filter $F$ on $\RO(X)$ admits two incompatible extensions $F_0,F_1$ to maximal filters on $\mathcal{O}(X)$.
If any elements of $F_0$ intersects any elements of $F_1$, $F_0\cup F_1$ is a prefilter strictly containing both of them. Hence there are $U_i\in F_i$ such that $U_0\cap U_1$ is empty.
This occurs if and only if $\Reg{U_0}\cap\Reg{U_1}$ is empty.
Now $U_i\cap U$ is non-empty for all $U\in F$ and
this occurs if and only if $\Reg{U_i}\cap U$ is non-empty for all $U\in F$. Since $F$ is maximal this can be the case only if $\Reg{U_i}\in  F$ for both $i$, which contradicts $F$ being a prefilter.\\
We note that for $G$ ultrafilter on $\RO(X)$ the unique maximal filter of open sets $\bar{G}$ is given by
$\bp{U:\Reg{U}\in G}$.
\item\textbf{For any $0$-dimensional $(X,\tau)$ there is a natural identification of maximal filters on $\CLOP(X)$ and maximal filters of closed sets:} if $C$ is closed,
$C$ is an intersection of clopen sets, hence any maximal filter $F$ of closed sets induces a maximal filter on $\CLOP(X)$ given by
\[
\bp{U\in\CLOP(X): \exists C\in F\, U\supseteq C},
\]
and conversely.
\item\textbf{If $(X,\tau)$ is compact Hausdorff, maximal filters of closed sets correspond to maximal filters of $0$-sets:}
Any closed set $C$ is an intersection of $0$-sets since $(X,\tau)$ is Tychonoff.
Now if $\F$ is a maximal filter of closed sets, let $\F^*$ be the intersection of $\F$ with the $0$-sets.

It suffices to argue that $\F^*$ is a maximal filter of $0$-sets. If not there is a $0$-set $D$ such that
$D\cap E$ is non-empty for all $0$-sets in $\F$ and $D\cap C$ is empty for some closed and non-empty
non-$0$-set in $\F$. Now if $C=\bigcap_{i\in I}C_i$ with each $C_i$ a $0$-set, we get that each $C_i$ is in $\F$. Hence we have on the one hand that
\(
\emptyset=D\cap C=\bigcap_{i\in I} D\cap C_i,
\)
on the other hand that $\bp{D\cap C_i:i\in I}$ is a family of closed sets with the finite intersection property. Since $X$ is compact the latter implies that $D\cap C$ is non-empty. We reached a contradiction.

Conversely if $\G$ is a maximal filter of $0$-sets, $\bigcap\G$ is a singleton $\bp{x_\G}$
(we use here that the space is compact Hausdorff).
Therefore $\G^*$ is the intersection with the $0$-sets
of the maximal filter of closed sets given by closed sets containing $x_\G$.
Hence we have a bijective correspondence between maximal filters of closed sets and maximal filters of $0$-sets.

\item\textbf{If $(X,\tau)$ is extremally disconnected, maximal filters on open sets correspond to maximal filters on $\mathcal{O}_0(X)$:}

In extremally disconnected spaces regular open sets are closed, hence they are $0$-sets, and the complement of $0$-sets. This gives that $\mathcal{O}_0(X)\supseteq\RO(X)$. Hence any maximal filter on $\mathcal{O}_0(X)$ induces a maximal filter on $\RO(X)$.
By the first item these overlaps with maximal filters of open sets.
We also note that whenever $\F$ is a maximal filter of open sets, $\F\cap \mathcal{O}_0(X)$ is a
maximal filter on $\mathcal{O}_0(X)$: otherwise $\F\cap \RO(X)$ could have two incompatible extensions to a maximal filter on $\mathcal{O}_0(X)$, and therefore also to $\mathcal{O}(X)$. We already saw that the latter is impossible.
\end{itemize}
Note that if $(X,\tau)$ is extremally disconnected but not $T_1$, the filters of (regular) open neighborhoods of points of $X$ might not be maximal filters of (regular) opens. Also we have already seen that in compact Hausdorff spaces $X$ the maximal filter of closed sets detect points of $X$, hence they may not detect a maximal filter of open sets (in case $X$ is not extremally disconnected).

Wrapping everything together we get the following:
\begin{proposition}
Assume $(X,\tau)$ is extremally disconnected, compact, Hausdorff. Then there are natural identifications of the families of:
\begin{itemize}
\item maximal filters on $\RO(X)$;
\item maximal filters on $\CLOP(X)$;
\item maximal filters on $\mathcal{O}_0(X)$;
\item maximal filters of open sets;
\item maximal filters of closed sets;
\item maximal filters of $0$-sets.
\end{itemize}
\end{proposition}

\subsection{Extremally disconnected compact Hausdorff spaces as Stone-\v{C}ech compactifications}
We conclude this section giving a characterization of extremally disconnected compact Hausdorff spaces as the class of compact Hausdorff spaces which are the  Stone-\v{C}ech compactification of any of their dense subsets\footnote{We are not able to trace the following Proposition in the literature, hence we include a proof of it.}. We will need this characterization in Section \ref{sec:sh}.
 \begin{proposition}
 \label{comp:exdisc}
 Let $(X,\tau)$ be a compact Hausdorff space. Then $X$ is extremally disconnected if and only if it is the Stone-\v{C}ech compactification of any of its dense subsets.
 \end{proposition}
 \begin{proof}
 Assume $(X,\tau)$ is compact Hausdorff but not extremally disconnected. Then there is $U\in\tau$ which is regular open but not closed. This gives that (letting $\neg U= X\setminus\overline{U}$) $U\cup\neg U$ is
 open dense in $X$. Fix $x_0\in U$ and $x_1\in \neg U$. Then $f(x)=x_0$ if $x\in U$ and $f(x)=x_1$ if $x\in\neg U$ is continuous on $U\cup\neg U$ but cannot be extended to a continuous map on the whole of $X$: note that $\overline{U}\cap\overline{\neg U}$ is non-empty (else $U$ is closed); if $y$ belongs to this set and $g$ extends continuously $f$ to $X$, $g(y)$ is either $x_0$ or $x_1$, but it can be neither of them since it is an accumulation point both for $U=f^{-1}[\bp{x_0}]$ and for $\neg U=f^{-1}[\bp{x_1}]$.

 The converse direction is given by the next Lemma.
 \end{proof}

\begin{lemma}
Let $X$ be a compact Hausdorff extremally disconnected space. Then for every dense subset $W\subseteq X$, every compact Hausdorff space $K$ and every continuous function $f:W\to K$, there exists an unique continuous map $\beta(f):X\to K$ such that $\beta(f)\restriction W=f$.
\end{lemma}
\begin{proof}
We can assume that $X=\St(\bool{B})$ where $\RO(\St(\bool{B}))=\bool{B}$ up to isomorphism. In particular
we identify any $G$ in $X$ with the ultrafilter on $\RO(X)$ given by its regular open (clopen) neighboorhoods.
Let $G\in X$. Since $W$ is dense, $W\cap V\neq\emptyset$ for every open neighborhood $V$ of $G$. In particular, the family $\{V\cap W: V\in G\}$ has the finite intersection property. Consequently the same holds for $\{f[V\cap W]: V\in G\}$ and for $\{\overline{f[V\cap W]}: V\in G\}$. Being $K$ compact, we have
\[
\bigcap_{V\in G}\overline{f[V\cap W]}\neq\emptyset.
\]
\begin{claim}
\label{claim1}
Let $U$ be an open subset of $K$.
Then $U\cap\bigcap_{V\in G}\overline{f[V\cap W]}\neq\emptyset$ if and only if $\Reg{f^{-1}[U]}\in G$.
\begin{proof}
\emph{}

\begin{description}
\item[$\Rightarrow$]
Since $U$ is open in $K$, $U\cap f[V\cap W]\neq\emptyset$ for every $V\in G$. Thus (in $X$) $f^{-1}[U]\cap V\neq\emptyset$ for every $V\in G$. This entails that (in $X$) $\Cl{f^{-1}[U]}\cap V\neq\emptyset$ for every $V\in G$. Now (in $X$) $\Reg{f^{-1}[U]}$ is a dense subset of $\Cl{f^{-1}[U]}$, and (in $\Cl{f^{-1}[U]}$) $V\cap\Cl{f^{-1}[U]}$ is a non-empty open subset of $\Cl{f^{-1}[U]}$ for any $V\in G$. Therefore $\Reg{f^{-1}[U]}\cap V\neq\emptyset$ for all $V\in G$, which occurs if and only if $\Reg{f^{-1}[U]}\in G$.

\item[$\Leftarrow$]
Conversely assume that $\Reg{f^{-1}[U]}\in G$.
Then $\Reg{f^{-1}[U]}\cap Z\neq\emptyset$ for all $Z\in G$.
Since $\Reg{f^{-1}[U]}$ is dense  in $\Cl{f^{-1}[U]}$, we get that
$\Cl{f^{-1}[U]}\cap Z\neq\emptyset$ for all $Z\in G$. Since
$f^{-1}[U]$ is dense in $\Cl{f^{-1}[U]}$ and
$\Cl{f^{-1}[U]}\cap Z\neq\emptyset$ is open in $\Cl{f^{-1}[U]}$ for all $Z\in G$,
we get that
$f^{-1}[U]\cap Z\neq\emptyset$ for all $Z\in G$.
This gives that $U\cap f[Z\cap W]\neq\emptyset$ for all $Z\in G$, as desired.
\end{description}

\end{proof}
\end{claim}

\begin{claim}
\label{claim2}
For any $G\in X$, there is exactly one point in $\bigcap_{V\in G}\overline{f[V\cap W]}$.
\end{claim}
\begin{proof}
By contradiction, assume that in $\bigcap_{V\in G}\overline{f[V\cap W]}$ there are two distinct points $y_1, y_2$. Being $K$ Hausdorff, there are disjoint open sets $U_1, U_2$ such that $y_i\in U_i$, $i=1, 2$. By Claim \ref{claim1}, $\Reg{f^{-1}[U_1]}, \Reg{f^{-1}[U_2]}\in G$. Hence $\Reg{f^{-1}[U_1]}\cap\Reg{f^{-1}[U_2]}$ is non-empty clopen. By density of $W$ in $X$, $\Reg{f^{-1}[U_1]}\cap\Reg{f^{-1}[U_2]}\cap W$ is non-empty and clopen in $W$.
Since $f^{-1}[U_1]$ is dense open in $\Reg{f^{-1}[U_1]}\cap W$ we get that $f^{-1}[U_1]$ has non-empty intersection with $\Reg{f^{-1}[U_2]}\cap W$ and is relatively open in it.
Since $ f^{-1}[U_2]$ is dense in $\Reg{f^{-1}[U_2]}\cap W$, we get that $f^{-1}[U_1]\cap f^{-1}[U_2]$
is non-empty, which is a contradiction.
\end{proof}

Thus we can define $\beta(f)(G)$ as the unique point $y_G$ in $\bigcap\{\overline{f[V\cap W]}: V\in G\}$.
We leave to the reader to check that $\beta(f)\restriction W=f$.

Finally, we prove the continuity
 of $\beta(f)$.

\begin{claim}
\label{claim3}
Assume $U$ is an open set of $K$. Then $\beta(f)[\Reg{f^{-1}[U]}]\subseteq \Cl{U}$.
\end{claim}
\begin{proof}
Assume $G\in \Reg{f^{-1}[U]}$.
Note that $G\in \Reg{f^{-1}[V]}$ for any $V$ open neighborhood of $\beta(f)(G)$
 (by Claim \ref{claim1}).
Hence $\Reg{f^{-1}[V]}\cap \Reg{f^{-1}[U]}$ is non-empty for all such $V$.
As in the proof of Claim \ref{claim2}, we obtain that
$f^{-1}[V]\cap f^{-1}[U]$ is non-empty for all such $V$.
Therefore so is
\(
U\cap V
\)
 for all $V$ open neighborhood of $\beta(f)(G)$.

We conclude that $\beta(f)(G)$ is an accumulation point of $U$.
\end{proof}

Now, fix $G\in X$ and take an open neighborhood $A$ of $\beta(f)(G)$. We prove that there exists an open neighborhood $U$ of $G$ such that $\beta(f)[U]\subseteq A$:
by normality of $K$ (being it compact Hausdorff), we can find an open neighborhood $V$ of $\beta(f)(G)$ such that $\Cl{V}\subseteq A$. By Claim \ref{claim1}, $\Reg{f^{-1}[V]}$ is an open neighborhood of $G$. By Claim \ref{claim3} its image is contained in $\Cl{V}\subseteq A$.
\end{proof}

\section{Dualities and adjuctions on topological spaces with open continuous maps}
\label{sec:dual}

In this section we define the type of partial orders/topological spaces over which we consider presheaves.
To state our main theorems we need a bit of terminology.

\begin{definition}\label{def:adjhom}
Let $\bool{B},\bool{C}$ be boolean algebras.

A map $i:\mathsf{B}\to\mathsf{C}$ is:
\begin{itemize}
\item
an \emph{homomorphism} if it preserves the boolean
operations (equivalently if  it is order preserving);

\item
a \emph{complete homomorphism} if for all $A\subseteq\bool{B}$ and $a\in \bool{B}$ such that $\bigvee_{\bool{B}}A=a$, we have that $\bigvee_{\bool{C}}i[A]=i(a)$;

\item an
\emph{adjoint homomorphism} if it has a left adjoint $\pi_i:\bool{C}\to\bool{B}$.
\end{itemize}
Define $\pi^*_i:\St(\bool{C})\to\St(\bool{B})$ by $\pi^*_i(G)=i^{-1}[G]$.
\end{definition}

\begin{notation}\label{not:kfpii}
Let $(X,\tau)$, $(Y,\sigma)$ be topological spaces and $f:X\to Y$ be a continuous map.
Define
$\bar{\bar{k}}_f:\sigma\to\tau$ by $\bar{\bar{k}}_f(U)=f^{-1}[U]$.

Let $\bar{k}_f=\bar{\bar{k}}_f\restriction \RO(Y)$ and $k_f=\bar{k}_f\restriction\CLOP(Y)$.
\end{notation}

The continuity of $f$ grants  that the range of $k_f$ is included in $\CLOP(X)$.
In principle it is not clear that the range of $\bar{k}_f$ is included in $\RO(X)$; we will see that this is the case when $f$ is an open map.

We will use the above to define contravariant functors from (variations of) the category of topological spaces with open maps to (variations of) the category of boolean algebras with \emph{adjoint} homomorphisms.
First of all we need notation to define the relevant categories and functors.
\begin{notation}
\emph{}

\begin{itemize}
\item $\bool{Top}_{\mathrm{open}}$ denotes the category of topological spaces with continuous open maps.
\item $\bool{TDCH}_{\mathrm{open}}$ denotes the subcategory with the same arrows but with objects given by the $0$-dimensional compact Hausdorff spaces.
\item $\bool{EDCH}_{\mathrm{open}}$ denotes
the subcategory with the same arrows but with objects given by the extremally disconnected compact Hausdorff spaces.
\item $\bool{BA}_{\mathrm{adj}}$ denotes the category of boolean algebras with arrows given by \emph{adjoint} homomorphisms.
\item $\bool{CBA}$ denotes the category of complete boolean algebras with arrows given by complete homomorphisms.
\end{itemize}

\begin{align*}
\mathcal{L}^*: & \bool{Top}_{\mathrm{open}}\to \bool{CBA}\\
& (X,\tau)\mapsto \RO(X)\\
& (f:X\to Y) \mapsto (\bar{k}_f:\RO(Y)\to\RO(X))
\end{align*}

\begin{align*}
\mathcal{D}: & \bool{TDCH}_{\mathrm{open}}\to \bool{BA}_{\mathrm{adj}}\\
& (X,\tau)\mapsto \CLOP(X)\\
& (f:X\to Y) \mapsto (k_f:\CLOP(Y)\to\CLOP(X))
\end{align*}

\begin{align*}
\mathcal{R}: & \bool{BA}_{\mathrm{adj}} \to \bool{TDCH}_{\mathrm{open}}\\
& \bool{B} \mapsto \St(\bool{B})\\
& (i:\bool{B}\to \bool{C}) \mapsto (\pi^*_i:\St(\bool{C})\to\St(\bool{B}))
\end{align*}

\end{notation}

The adjunctions/dualities we want to bring forward are summarized in the following theorem:

\begin{theorem}\label{thm:adj-dual-cbaTDCH}
The following holds:
\begin{enumerate}
\item
$\mathcal{D}$, $\mathcal{L}^*$, $\mathcal{R}$ are well defined functors.
\item
$\mathcal{D}$ implements a duality between $\bool{TDCH}_{\mathrm{open}}$ and
$\bool{BA}_{\mathrm{adj}}$ with inverse given by $\mathcal{R}$.
\item
$\mathcal{D}\restriction\bool{EDCH}_{\mathrm{open}}$ implements a duality between $\bool{EDCH}_{\mathrm{open}}$ and
$\bool{CBA}$ with inverse given by $\mathcal{R}\restriction\bool{CBA}$.
\item
Let
$\mathcal{L}=\mathcal{L}^*\restriction  \bool{TDCH}_{\mathrm{open}}$.
Then $(\mathcal{L},\mathcal{R}\restriction\bool{CBA})$ is a contravariant adjunction.
\end{enumerate}
\end{theorem}

The proof is an easy outcome of the following
propositions\footnote{We expect their content to be folklore; however we have not been able to trace in the literature items  (\ref{prop:openadjpairs-4})  and (\ref{prop:openadjpairs-7}) of Proposition \ref{prop:openadjpairs}, and item (\ref{cor:openmapscomplhomI}) of Proposition \ref{thm:openmap-->adjoint}.} linking the properties of (complete injective) homomorphisms to those of
(open surjective) continuous functions and of adjoint pairs:

\begin{proposition}\label{prop:openadjpairs}
	Let $i: \bool{B} \rightarrow \bool{C}$ be an homomorphism of boolean algebras, and
	$f:X\to Y$ be a continuous function between compact $0$-dimensional Hausdorff spaces.

	Then:
	\begin{enumerate}[(i)]
	\item \label{prop:openadjpairs-1}
	$\pi^*_i$ is continuous and closed;
	\item \label{prop:openadjpairs-2}
	$i$ is injective if and only if $\pi^*_i$ is surjective, in which case $\pi^*_i[N_{i(b)}]=N_b$;
	\item \label{prop:openadjpairs-3}
	$i=k_{\pi^*_i}$ modulo the identification of $\bool{D}$ with $\CLOP(\St(\bool{D}))$ given by
	$b\mapsto N_b$ for $\bool{D}$ a boolean algebra;
	\item \label{prop:openadjpairs-4}
	$i$ has a left adjoint $\pi_i$ if and only if $\pi^*_i$ is an open map, in which case $N_{\pi_i(c)}=\pi^*_i[N_c]$, and $i$ is a complete homomorphism;
	\item \label{prop:openadjpairs-5}
	$k_f$ is an homomorphism;
	\item \label{prop:openadjpairs-6}
	$\pi^*_{k_f}=f$ modulo the identification of $Z$ with $\St(\CLOP(Z))$ given by
	\[
	z\mapsto G_z=\bp{U\in\CLOP(Z): z\in U}
	\]
	for $Z$ compact $0$-dimensional Hausdorff space;
	\item  \label{prop:openadjpairs-7}
	 $k_f$ has a left adjoint $\pi_f$ if and only if $f$ is an open map, in which case
	 $N_{\pi_f(c)}=f[N_c]$, and $k_f$ is a complete homomorphism.
	 \end{enumerate}
	 \end{proposition}

	 Furthermore the above can be meshed with the following
	 \begin{proposition} \label{thm:openmap-->adjoint}
	 Let $X,Y$ be arbitrary topological spaces and
	  $f:X\to Y$ be an open continuous map, we have that
	 \begin{enumerate}[(A)]
	 \item\label{cor:openmapscomplhomI}
	 $\Reg{f^{-1}[U]}=f^{-1}[\Reg{U}]$ for any open set $U$ of $Y$;
	 \item\label{cor:openmapscomplhomII}
	 $\bar{k}_f:\RO(Y)\to\RO(X)$ given by $U\mapsto f^{-1}[U]$ is a complete homomorphism
	 with right adjoint $\bar{\pi}_f:\RO(X)\to\RO(Y)$ given by $V\mapsto f[V]$;
	 \item \label{cor:openmapscomplhomIII}
	 In case $X,Y$ are $0$-dimensional compact Hausdorff $\bar{k}_f\restriction\CLOP(Y)=k_f$
	 and $\bar{\pi}_f\restriction\CLOP(X)$ is the left adjoint of $k_f$;
	 \item \label{cor:openmapscomplhomIV}
	 In case $X,Y$ are extremally disconnected compact Hausdorff $\bar{k}_f=k_f$.
	 \end{enumerate}
	 \end{proposition}

\begin{remark}
Let $\bool{B}$ be the boolean algebra given by finite and cofinite subsets of $\omega$ and
$i:\bool{B}\to\pow{\omega}$ be the inclusion map. It can be checked that $i$ is a complete injective
homomorphism
and $\pi^*_i$ is not an open map\footnote{This counterexample has been given by D. Monk.}.
On the other hand if $i:\bool{B}\to\bool{C}$ is an homomorphism between complete boolean algebras,
$i$ has an adjoint if and only if $i$ is complete.
In particular the notion of complete homomorphisms is weaker than that of
adjoint homomorphism only when considering non-complete boolean algebras.
\end{remark}

First of all we prove Theorem \ref{thm:adj-dual-cbaTDCH} assuming the two propositions:
\begin{proof}
The fact that $\mathcal{L}^*$ is a well defined functor follows from \ref{cor:openmapscomplhomI} of
Proposition \ref{thm:openmap-->adjoint}.
 $\mathcal{D}$ is a duality by Stone duality and by (\ref{prop:openadjpairs-3}) and (\ref{prop:openadjpairs-4}) of Proposition \ref{prop:openadjpairs}. $\mathcal{D}\restriction\bool{EDCH}$ is also a duality by
the known result that the Stone duality maps the object of $\bool{EDCH}$ onto those of $\bool{CBA}$
bijectively up to isomorphism, by (\ref{prop:openadjpairs-3}) and (\ref{prop:openadjpairs-4}) of Proposition \ref{prop:openadjpairs}, and by
Proposition \ref{thm:openmap-->adjoint}. $(\mathcal{L},\mathcal{R}\restriction\bool{CBA})$ is an adjunction by Proposition \ref{thm:openmap-->adjoint} and by (\ref{prop:openadjpairs-3}) and (\ref{prop:openadjpairs-4}) of Proposition \ref{prop:openadjpairs}.
\end{proof}

We start with the proof of Proposition \ref{thm:openmap-->adjoint}.
\begin{proof}
\emph{}

\begin{description}
\item[(\ref{cor:openmapscomplhomI})]
Assume $U$ is open and $x\in \Reg{f^{-1}[U]}$. Then (by Lemma \ref{lem:charreg}) $x$ has an open neighborhood $V$ such that $V\cap f^{-1}[U]$ is dense in $V$. Since $f$ is open, $f[V]$ is an open neighborhood of $f(x)$. It is enough to show that
$U\cap f[V]$ is dense in $f[V]$ (again by Lemma \ref{lem:charreg}). Pick $Z$ open subset of $f[V]$. Then $f^{-1}[Z]$ is an open subset of $V$,
hence it has non empty intersection with $f^{-1}[U]$. If $z$ is in this latter set, $f(z)$ is in $Z\cap U$.

Conversely assume $x\in f^{-1}[\Reg{U}]$. Then (by Lemma \ref{lem:charreg}) $f(x)$ has an open neighborhood $V$ such that
$U\cap V$ is dense in $V$. It is enough to show that
$f^{-1}[U]\cap f^{-1}[V]$ is dense in $f^{-1}[V]$ (again by Lemma \ref{lem:charreg}). Pick $A$ non-empty  open subset of $f^{-1}[V]$.
Then $f[A]$ is a non-empty open subset of $V$, hence it has non-empty intersection with $U$. This easily gives
that $A\cap f^{-1}[U]$ is non-empty.

\item[(\ref{cor:openmapscomplhomII})]
By (\ref{cor:openmapscomplhomI}) we get that for $U$ regular open subset of $Y$
\[
\Reg{f^{-1}[U]}=f^{-1}[\Reg{U}]=f^{-1}[U],
\]
hence $f^{-1}[U]$ is a regular open subset of $X$ and $\bar{k}_f$ is well defined.

It is immediate to check that $\bar{k}_f$ is order preserving.

Furthermore
if $\bp{A_i:i\in I}$ is a family of regular open subsets of $Y$ and $A=\bigcup_{i\in I}A_i$, we have that
\begin{align*}
\bigvee_{\RO(X)}\bp{\bar{k}_f(A_i):i\in I}=\Reg{\bigcup_{i\in I}f^{-1}[A_i]}=\Reg{f^{-1}[\bigcup_{i\in I}A_i]}=
\Reg{f^{-1}[A]}=\\
=f^{-1}[\Reg{A}]=f^{-1}[\bigvee_{\RO(Y)}\bp{A_i:i\in I}]=\bar{k}_f(\bigvee_{\RO(Y)}\bp{A_i:i\in I}),
\end{align*}
hence $\bar{k}_f$ is a complete morphism of partial orders.

It is well known that a map $k:\bool{B}\to\bool{C}$ is a complete homomorphism of complete boolean algebras if and only if $k$ is suprema and order preserving. Hence $\bar{k}_f$ is a complete homomorphism.

It is also immediate to check that for $U\in\RO(Y)$ and $V\in\RO(X)$,
$\bar{k}_f(U)=f^{-1}[U]\supseteq V$ if and only if $U\supseteq f[V]=\bar{\pi}_f(V)$, hence
$(\bar{\pi}_f, \bar{k}_f)$ is an adjoint pair.
\item[(\ref{cor:openmapscomplhomIII}) and (\ref{cor:openmapscomplhomIV})] Trivial.
\end{description}
\end{proof}

We now prove Proposition \ref{prop:openadjpairs}:

\begin{proof}
\emph{}

\begin{description}
\item[(\ref{prop:openadjpairs-1}), (\ref{prop:openadjpairs-2}), (\ref{prop:openadjpairs-3})]
This is part of the standard proofs of Stone duality.

\item[(\ref{prop:openadjpairs-4})]
If $\pi^*_i$ is open we have that $\pi^*_i[N_c]$ is clopen for all $c\in\bool{C}$.
Furthermore for all $b\in\bool{B}$ and $c\in\bool{C}$
\[
N_{i(b)}\supseteq N_c\text{ if and only if }(\pi^*_i)^{-1}[N_b]\supseteq N_c
\text{ if and only if } N_b\supseteq \pi^*_i[N_c].
\]
Hence
the map $\pi_i:N_c\mapsto \pi^*_i[N_c]$ is the left adjoint of $k_{\pi^*_i}$, or equivalently (letting
$\pi_i(c)=\bigwedge_{\bool{B}}\bp{b:i(b)\geq c}$) $\pi_i$ is well defined and is the right adjoint of $i$.

For the completeness of $\pi_i$, apply  (\ref{cor:openmapscomplhomIII}) of  Proposition \ref{thm:openmap-->adjoint}, since infima and suprema in $\CLOP(X)$ are computed using the same operations of $\RO(X)$ (when they exist).

\item[(\ref{prop:openadjpairs-5})]
Trivial by continuity of $f$.

\item[(\ref{prop:openadjpairs-6})]
See (\ref{prop:openadjpairs-3}) or else:
\begin{align*}
\pi^*_{k_f}(G_x)=\bp{V\in\CLOP(Y): k_f(V)\in G_x}=\bp{V\in\CLOP(Y): f^{-1}[V]\in G_x}=\\
=\bp{V\in\CLOP(Y): x\in f^{-1}[V]}=\bp{V\in\CLOP(Y): f(x)\in V}=G_{f(x)}.
\end{align*}

\item[(\ref{prop:openadjpairs-7})]
Use (\ref{cor:openmapscomplhomIII}) of  Proposition \ref{thm:openmap-->adjoint}.

\end{description}
\end{proof}

\section{stonean sheafifications}
\label{sec:sh}
In this section we define a \emph{stonean} sheafification process for presheaves
on topological spaces $(X,\tau)$ which will associate to them \'etal\'e spaces whose stalks are indexed by maximal filters of open sets of $\tau$.
Our stonean sheafification construction gives an explicit topological representation of the sheafification process induced by the dense Grothendieck topology  when applied to a presheaf on an arbitrary topological space $(X,\tau)$.
We mimick the standard construction of sheaves (as described for example in \cite[II]{MacLMoer}) for presheaves defined on topological spaces; e.g. we associate to each presheaf $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ an \'etal\'e bundle and we obtain the sheafification of $\F$ by taking the local section of the (one point compactification) of the bundle. In performing both the constructions of the \'etal\'e bundle and the selection of the local section of this bundle we are more generous in our definitions and we blow up the base space of the bundle (which is not anymore $X$ but $\St(\RO(X))$ and the type of local sections of the bundle we put into the sheafification, which are those continuous functions from $\St(\RO(X))$ to the one point compactification of the (domain of the) bundle which take value almost everywhere in the (domain of the) bundle.
Therefore our sheafification process produces a variety of stalks in the corresponding \'etal\'e space which cannot exist in the \'etal\'e space associated to the standard sheafification process (as described for example in \cite[II]{MacLMoer}): the existence of these additional stalks is based on the use of logical principles not available in intuitionistic logic.
Looking at our stonean sheafification process with the lenses of boolean valued semantics, it describes a canonical process to ``complete'' a $\bool{B}$-valued models $\mathcal{M}$ to a $\RO(\bool{B}^+)$-valued model $\mathcal{M}^*$ which roughly satisfies the same semantics but which also has the mixing property. We will outline in Section \ref{sec:pres} the correspondence between boolean valued models and presheaves. In this correspondence, boolean valued models with the mixing property are stonean sheaves.  When dealing with a $\bool{B}$-model $\M$ without the mixing property, it would be convenient to find a canonical way to ``mixify'' $\M$. This is exactly what our stonean sheafification process does (see Cor. \ref{cor:mixbvm}).
\cite{MacLMoer} is our reference for unexplained terminology.

\subsection{Stonean sheaves versus topological sheaves}
In this section we introduce and analyze the type of sheaves one is naturally led to consider when looking at boolean valued models. We stick whenever possible to the notation of \cite{MacLMoer}.
Let us start giving an explicit definition of the type of (pre)sheaves we will consider:

\begin{definition}
Let $(P,\leq)$ be a partial order.

\begin{itemize}
\item
A \emph{presheaf} $\F:P^\mathrm{op}\to\dSet$ is a contravariant functor
from $P$ (seen as a category whose arrows are determined by the order relation) to the category
$\dSet$ (with arrow induced by functions).
\item
A \emph{topological presheaf} $\F$ on a topological space $(X,\tau)$ is a presheaf $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$
(where $\mathcal{O}(X)=\tau\setminus\bp{\emptyset}$ is ordered by inclusion).
\end{itemize}
\end{definition}

\begin{notation}
Let $(P,\leq)$ be a partial order.
\begin{itemize}
\item
$A\subseteq P$ is a \emph{dense covering} of $p\in P$ if it is a predense subset of $P\restriction p$ e.g. for every $q\in P$ refining $p$ there is $r\in A$ and a common refinement $s$ of $r$ and $q$.
\item
Let $(P,\leq)$ be an upward complete partial order.
$A\subseteq p$ is a \emph{complete covering} of $p$ if $\bigvee_P A=p$.
\end{itemize}

Let $\F:P^{\mathrm{op}}\to\dSet$ be a presheaf.
\begin{itemize}
\item
A \emph{compatible family} $\bp{f_i:i\in I}$ for $\F$ is a family of elements $f_i\in \F(p_i)$ such that for all
$i,j$ and $r$ refining $p_i,p_j$ $f_i\restriction r=f_j\restriction r$ (letting  $\F(s\leq t)(f)=f\restriction s$ for $f\in\F(t)$).
\item
A \emph{collation} of a compatible family $\bp{f_i:i\in I}$ on some $p$ is some $f\in \F(p)$ such that $f\restriction r=f_i\restriction r$ for all $i\in I$ and $r$ refining $p,p_i$.
\end{itemize}
\end{notation}

\begin{definition}
Let $(P,\leq)$ be a partial order, and
$\F:P^{\mathrm{op}}\to\dSet$ be a presheaf.
\begin{itemize}
\item
$\F$ is a\footnote{We adopt the terminology of \cite[III Section 2 item (e) pp. 115]{MacLMoer}.} \emph{sheaf for the dense Grothendieck topology on $P$} when for every $p\in P$
and every compatible family $\bp{f_i:i\in I}$ for $\F$ with  $f_i\in \F(p_i)$, if $A=\bp{p_i:i\in I}$ is a dense covering of $p$, then there is a unique collation $f\in \F(p)$ on $p$ of the family.
\item Assume further that $P$ is upward complete.
$\F$ is a\footnote{We adopt the terminology of \cite[III Section 2 item (d) pp. 114-115]{MacLMoer}.}  \emph{sheaf for the sup Grothendieck topology on $P$} when for every $p\in P$ and every
compatible family $\bp{f_i:i\in I}$ for $\F$ with  $f_i\in \F(p_i)$, if $A=\bp{p_i:i\in I}$ is a complete covering of $p$, there is a unique collation $f\in \F(p)$ of the family.
\end{itemize}

Let $(X,\tau)$ be a topological space and $\F:\mathcal{O}(X)^{\mathrm{op}}\to \dSet$ be a presheaf.
\begin{itemize}
\item
$\F$ is a \emph{topological sheaf} on $(X,\tau)$ if $\F$ is a sheaf for the sup Grothendieck topology
on $\mathcal{O}(X)$.
\item
$\F$ is a \emph{stonean sheaf} on $(X,\tau)$ if $\F$ is a sheaf for the dense Grothendieck topology
on $\mathcal{O}(X)$.
\end{itemize}
\end{definition}
The standard notion of sheaf on a topological space as defined in \cite[II Sections 5, 6]{MacLMoer} corresponds to our notion of topological sheaf. However a topological sheaf need not be
a stonean sheaf (see Example \ref{exm:keyetsp} below).
On the other hand the converse is the case:
\begin{fact}
Let $\F:\mathcal{O}(X)^{\mathrm{op}}\to \dSet$ be a stonean sheaf. Then $\F$ is also a topological sheaf.
\end{fact}
\begin{proof}
Assume $\bp{f_i:i\in I}$ is compatible for $\F$ with  $f_i\in \F(U_i)$. Let $A=\bigcup\bp{U_i:i\in I}$. Then $\bp{U_i:i\in I}$ is a dense covering of $A$. Since $\F$ is a stonean sheaf we have that there is a unique $f\in \F(A)$ which collates the family $\bp{U_i:i\in I}$.
\end{proof}

The following is the key property relating the two notion of sheaf:
\begin{lemma}
Let $(X,\tau)$ be a topological space whose regular open sets form a base for the topology.
Let $\F:\mathcal{O}(X)^{\mathrm{op}}\to \dSet$ be a presheaf.
$\F$ is a stonean sheaf on $(X,\tau)$ if and only if $\F\restriction\RO(X)^+$ is a
sheaf for the sup Grothendieck topology on $\RO(X)^+$.
\end{lemma}
\begin{proof}
The key point is that (since the regular open sets form a base for the topology), $A$ is predense below $U$ in $\mathcal{O}(X)$ if and only if
\[
D_A=\bp{V\in\RO(X): V\subseteq W\cap U\text{ for some }W\in A}
\]
is such that $\bigcup D_A$ is a dense open subset of $\Reg{U}$.
Hence in $\RO(X)^+$ we have that
\[
\bigvee_{\RO(X)}D_A=\Reg{U}.
\]
Now let $\bp{f_i:i\in I}$ be compatible for $\F$ with $U=\bigcup\bp{U_i:i\in I}$ and each $f_i\in \F(U_i)$.
Without loss of generality (since the regular open sets form a base for the topology) it suffice to consider just the case in which each $U_i$ is regular open.
Then $f\in \F(\Reg{U})$ is a collation of $\bp{f_i:i\in I}$ with respect to the dense topology
on $\mathcal{O}(X)$
if and only if it is such with respect to the complete topology on $\RO(X)^+$.

\end{proof}

We outline a few key properties of \emph{stonean sheaves}:

\begin{proposition}
Assume $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ is a stonean sheaf with $\F(X)\neq\emptyset$.
Then $\F(U)=\bp{f\restriction U: f\in \F(X)}$ for all $U\in\mathcal{O}(X)$.
\end{proposition}
\begin{proof}
For any $U\in\mathcal{O}(X)$, $\bp{U,X\setminus\Cl{U}}$ is a dense covering for $X$.
Let $g\in\F(X)$ and $f\in \F(U)$. Then $\bp{g\restriction X\setminus\Cl{U},f}$ is a compatible family indexed by a dense covering of $X$. If $h\in\F(X)$ is a collation of this family, $h\restriction U=f$.
\end{proof}

We can also see that  a stonean sheaf necessarily is a topological sheaf on an extremally disconnected compact Hausdorff space, at least under very mild assumptions on its local sections:
\begin{fact}
Assume $\F$ is a stonean sheaf on some Hausdoff compact space $(X,\tau)$
such that for some Hausdorff space
$(Y,\sigma)$ with more than one point and
for every regular open set $U$ of $X$, $\F(U)$ consists of continuous maps from $U$ to $Y$ and includes at least two distinct constant maps. Then $(X,\tau)$ is also extremally disconnected.
\end{fact}
\begin{proof}

Assume $(X,\tau)$ is compact Hausdorff but not extremally disconnected. Then there is $U\in\tau$ which is regular open but not closed. This gives that (letting $\neg U= X\setminus\overline{U}$) $\bp{U,\neg U}$ is
 a dense cover in $X$. Fix $x_0\neq x_1\in Y$ such that  $f_0:x\mapsto x_0$ is in $\F(U)$ and $f_1:x\mapsto x_1$ is in $\F(\neg U)$. Then $\bp{f_0,f_1}$ is a compatible family indexed by a dense cover which cannot have a collation on $X$: note that $\overline{U}\cap\overline{\neg U}$ is non-empty (else $U$ is closed); if $y$ belongs to this set and $g$ extends continuously $f_0\cup f_1$ to $X$, $g(y)$ is either $x_0$ or $x_1$, but it can be neither of them since $y$ is an accumulation point both for $U=f_0^{-1}[\bp{x_0}]$ and for $\neg U=f_1^{-1}[\bp{x_1}]$.
\end{proof}

\subsection{Stonean bundles and stonean sheaves}

We stick  to the notation of \cite[II Sections 5, 6]{MacLMoer}. The unique notational difference is that we will write $(\Lambda^0_\F, p^0_\F)$ (instead of $(\Lambda_\F, p_\F)$) for the \'etal\'e space associated to the presheaf $\F$ and $\Gamma^0_p$ (instead of $\Gamma_p$) for the sheaf associated to the bundle $p$. This choice is motivated by our choice to use a similar notation ($(\Lambda^1_\F, p^1_\F)$ and $\Gamma^1_p, \Gamma^{1/2}_p$, respectively) for our constructions.
\begin{definition}
Let $X$ be a topological space. A \emph{bundle} over $X$ is a continuous (possibly non surjective) map $p:E\to X$.\\
A \emph{(global) section} of the bundle\footnote{Global sections can exist only if the bundle is surjective.} $p:E\to X$ is a continuous map $s:X\to E$ such that $p\circ s$ is the identity on $X$. If $U$ is an open set of $X$, a \emph{(local) section} of $p$ over $U$ is a section of the bundle $p\restriction p^{-1}[U]:p^{-1}[U]\to U$.
If $p:E\to X$ is a bundle and $x\in X$, the \emph{fiber} at $x$ is $p^{-1}[\bp{x}]$.\\
A bundle $p:E\to X$ is an \emph{\'etal\'e space} if it is a local homeomorphism in the following sense: for every $e\in E$ there exists an open neighborhood $V$ of $e$ such that $p[V]$ is open in $X$ and $p\restriction V:V\to p[V]$ is an homeomorphism.
\end{definition}
\begin{definition}\label{def:etbund0} \cite[Section II.5]{MacLMoer}
Let $(X, \tau)$ be a topological space and
$\F:\mathcal{O}(X)^{\textrm{op}}\to\dSet$ be a presheaf.
\[
\Lambda^0_\F:=\coprod_{x\in X}\F_x=\bp{[f]_{\sim_x}: x\in X, f\in\F(U), x\in U\in\mathcal{O}(X)}
\]
(where $[f]_{\sim x}$ is the equivalence class induced by $f\equiv_{\sim x} g$ if and only if $f\restriction U=g\restriction U$ for some
$x\in U\in\mathcal{O}(X)$),
\[
\begin{aligned}
p^0_\F:& \Lambda_\F\to X\\
&[f]_{\sim_x}\mapsto x
\end{aligned}.
\]
Each $f\in\F(U)$ determines
\[
\begin{aligned}
\dot{f}:&U\to\Lambda^0_\F\\
&x\mapsto[f]_{\sim_x}
\end{aligned},
\]
which is a section of $p^0_\F$ over $U$ ($\dot{f}$ is injective: if $x\neq y$, $[f]_{\sim_x}\neq[f]_{\sim_y}$, since $\F_x,\F_y$ are disjoint). \\
$\Lambda^0_\F$ is topologized by taking as a (semi)base\footnote{The topology generated by this semibase shows that this semibase is a base.} of open sets the family of all the image sets $\dot{f}[U]$ for
$U\in\mathcal{O}(X)$ and $f\in\F(U)$.
\end{definition}
This topology on $\Lambda^0_\F$ in general is not Hausdorff, but renders the map $p^0_\F$ continuous
and the sections
$\dot{f}$ continuous and open. In particular, it is easy to see that $p^0_\F:\Lambda^0_\F\to X$ is an \'etal\'e space over $X$.\\
Conversely, any bundle $p:E\to X$ over a topological space $X$ gives rise to a sheaf, the \emph{sheaf of sections} of $E$.  It is defined as follows in \cite{MacLMoer}:
\begin{definition}\cite[Section II.6]{MacLMoer} \label{def:standsheafif}
Let $p:E\to X$ be a continuous map between the topological spaces $(X,\tau)$, $(E,\sigma)$.
For $U$ a non-empty open subset of $X$, let
\[
\Gamma^0_p(U):=\bp{s: U\to E: s\emph{ is a section of $p$ over $U$}}.
\]
\end{definition}
Let us spend a few words about this correspondence between a presheaf $\F$ on $(X,\tau)$ and the sheaf
$\Gamma^0_{p^0_\F}$. Let $\mathcal{A}$ be a base for $(X, \tau)$. Assume $h:U\to\Lambda^0_\F$ is a section in $\Gamma^0_{p^0_\F}(U)$. Then, for every
$x\in U$, there is an open neighborhood $x\in U_x\subseteq U$ with $U_x\in\mathcal{A}$ such that $h(x)$ is the germ at $x$ of some element
$f_x\in\F(U_x)$, i.e. $h(x)=[f_x]_{\sim_x}=\dot{f}_x(x)$. Now, $h$ is continuous and $\dot{f_x}[U_x]$ is a basic open subset of
$\Lambda^0_\F$.
By continuity, there exists an open subset $V_x\in\mathcal{A}$ with $x\in V_x\subseteq U_x$ such that
$h[V_x]\subseteq\dot{f_x}[U_x]$. This means that $h$ coincides with $\dot{f_x}$ on $V_x$.
Therefore every section of the bundle $\Gamma^0_{p^0_\F}$ associated to $\F$ is locally a section induced by an element of $\F$.

For any presheaf $\mathcal{F}:\mathcal{O}(X)^{\textrm{op}}\to\dSet$,
$\Gamma^0_{p^0_\F}:\mathcal{O}(X)^{\textrm{op}}\to\dSet$ is always a topological sheaf but in general not a stonean sheaf.
This is exactly what occurs in the following Example which separates the notion of stonean sheaf from that of topological sheaf.

\begin{example}\label{exm:keyetsp}
Consider
the presheaf $\mathcal{G}$ of continuous real valued functions defined on some \emph{regular open} subset of $[0; 1]$ with range a bounded subset of $\mathbb{R}$.
This is not a sheaf as the collation of a compatible family of bounded continuous functions could results in an unbounded continuous function.
Nonetheless the \'etal\'e space $\Lambda^0_\mathcal{F}$ associated to this sheaf can be identified with the
germs of continuous functions $f:U\to\mathbb{R}$
at points $x\in [0;1]$ with $U$ an open neighborhood of $x$, and the (topological - according to our notation) sheaf $\Gamma^0\Lambda^0_\F$
of local sections on $\Lambda^0_\mathcal{F}$
corresponds to the topological sheaf of real valued continuous functions defined on some open subset of $[0;1]$.

Consider now the family of partial constant functions $f_n$ for $n\in\mathbb{N}$  with $f_n$ constant with value $n$ on the interval $(\frac{1}{n},\frac{1}{n+1})$. This gives a specific family of elements of $\mathcal{F}$
which can be collated in $\Gamma^0\Lambda^0_\F$.
Their collation $f=\bigcup_{n\in\mathbb{N}}f_n$ however is defined only on the dense open subset
$(0;1]\setminus\{\frac{1}{n}: n\in\mathbb{N}\}$ and does not have a germ at $0$, because it does not admit a continuous extension to any
open neighborhood of $0$. In particular it does not identify a global section of $\Lambda^0_\mathcal{F}$.

We conclude that $\Gamma^0\Lambda^0_\F$ is a topological sheaf which is not stonean exactly because the compatible family $\bp{f_n:n\in\mathbb{N}}$ is indexed by a  covering of $\mathbb{R}$ for the dense topology which does not have a collation defined on $\mathbb{R}$.

$f$ is a function regular enough to be of interest in our analysis, hence we want to be able to include it as part of the global sections of the \'etal\'e space we wish to associate to $\mathcal{F}$.
To reach this objective we associate to $\F$ the \'etal\'e bundle $\Lambda^1_\mathcal{F}$ (see Definition \ref{def:etbund1})
given by the germs of functions in $\mathcal{F}$ induced by
maximal filters of open intervals, or equivalently by ultrafilters on the complete boolean algebra $\RO([0;1])$
given by the regular open subsets of $[0;1]$. In this case it is possible to show that the global sections of
$\Lambda^1_\mathcal{F}$ induce continuous functions from $\St(\RO([0;1]))$ to the one point compactification of $\mathbb{R}$.
In this set-up, $f$ defines a unique global section of $\Lambda^1_\mathcal{F}$ which induces
the following continuous function $\beta(f):\St(\RO([0;1]))\to \mathbb{R}\cup\bp{\infty}$:
\begin{equation*}
G\mapsto
\begin{cases*}
      n \text{ if }(\frac{1}{n},\frac{1}{n+1})\in G  \\
      \infty \text{ if for no $n$ } (\frac{1}{n},\frac{1}{n+1})\in G.
    \end{cases*}
\end{equation*}
We will then use this \'etal\'e space/bundle to define a stonean sheaf $\Gamma^{1}\Lambda^1_\F$
which will comprise $\beta(f)$ among its global sections.
 \end{example}
We will detail more on this as we unfold our concepts (the reader is referred also to \cite[Section 5.2]{viale-notesonforcing}).

Our focus from now on will be on the definition of the construction which will bring from $\mathcal{F}$ to $\Gamma^{1}_{\Lambda^1_\mathcal{F}}$, rather than the usual
one bringing from $\mathcal{F}$ to $\Gamma^0_{\Lambda^0_\mathcal{F}}$.
Loosely speaking the variant of the sheafification process we are interested in will be able to comprise as global sections of the \'etal\'e space of
$\mathcal{F}$ also the pointwise limits of continuous functions; for an arbitrary topological sheaf $\F$ the sheaf of sections of the \'etal\'e space $\Lambda^1_\mathcal{F}$ may not be at all isomorphic to $\mathcal{F}$, as the latter is always a stonean sheaf even if the former is not.

We want to devise a sheafification process which given a presheaf
$\mathcal{F}:\mathcal{O}(X)^{\textrm{op}}\to\dSet$, yields first a bundle
$p^1_\F:\Lambda^1_\F\to \St(\RO(X))$ and then a stonean sheaf $\Gamma^{1}_{p^1_\F}$ given by local sections of $p^1_\F$ which can be seen as the natural
``stonean'' sheafification of $\F$.
The success of our approach is outlined by Theorem \ref{thm:gamma1adj} which states that
$\Gamma^{1}_{p^1_\F}$ is the left adjoint of the inclusion functor of the full subcategory of stonean sheaves into the category of topological presheaves on some topological space\footnote{Since the base space of the presheaves vary, the notion of morphism in this category is delicate, see Section \ref{subsec:stsheafadj}, Def. \ref{def:presh*morph}.}.

It is convenient for the rest of this section to look at a boolean algebra at times as an algebraic structure and at other times as the clopens of its Stone space. We will freely do so in the sequel. Hence we write $b\in G$ when we think of $\bool{B}$ as a boolean algebra, $b$ as an element of $\bool{B}$, $G$ as an ultrafilter on $\bool{B}$, or $G\in b$ when we think of $G$ as an element of $\St(\bool{B})$ and $b$ as a clopen subset of $\St(\bool{B})$. We also consider $\bool{B}$ a dense subalgebra of $\RO(\bool{B}^+)$
and we note that for any ultrafilter $G$ on $\RO(\bool{B}^+)$ $G\cap \bool{B}$ is a ultrafilter on
$\bool{B}$.

We start by introducing a new notion of stonean  \'etal\'e space associated to a given topological presheaf.

\begin{definition}\label{def:etbund1}
Let $(X,\tau)$ be a topological space and $\mathcal{F}:\mathcal{O}(X)^{\textrm{op}}\to \dSet$ be a presheaf. Given $G$ ultrafilter in $\St(\RO(X,\tau))$, let $\bar{G}$ be the unique maximal filter of $\mathcal{O}(X)$ induced by $G$ (i.e. $U\in\bar{G}$ if and only if $\Reg{U}\in G$).

We let for $G\in\St(\RO(X,\tau))$:
\begin{itemize}
\item for $f\in \F(U_f), g\in\F(U_g)$ and $U_f,U_g\in \bar{G}$,
$f\equiv_{G} g$ if and only if for some $U\in \bar{G}$ refining $U_f,U_g$
 \[
D_{f,g}=\bp{V\in\mathcal{O}(X):\, f\restriction V=g\restriction V}
 \]
 is dense below $U$
(where $\mathcal{F}(U\leq V)(f)=f\restriction U$);
\item
$[f]_{G}$ be the equivalence class of $f$ induced by $\equiv_{G}$;
\item

$\F_G:=\bp{[f]_G: f\in\F(U_f), U_f\in \bar{G}}$.
\end{itemize}

We also let:
\begin{itemize}
\item
$\Lambda^1_\F:=\coprod_{G\in \St(\RO(X))}\F_G$;
\item $p^1_\F$ be defined by
\[
\begin{aligned}
p^1_\F:& \Lambda^1_\F\to \St(\RO(X))\\
&[f]_{G}\mapsto G
\end{aligned} .
\]
\end{itemize}
Each $f\in\F(U)$ determines
\[
\begin{aligned}
\dot{f}:&\Reg{U}\to\Lambda^1_\F\\
&G\mapsto[f]_G
\end{aligned}.
\]
We topologize $\Lambda^1_\F$ with topology $\tau^1_\F$ by taking as a semibase of open sets the family
\[
B^1_\F=\{\dot{f}[q]: q\in\RO(X),\, q\subseteq \Reg{U}, \, f\in\F(U), \, U\in \mathcal{O}(X)\}.
\]
\end{definition}

We start to unfold the properties of $\Lambda^1_\F$:
\begin{proposition}\label{prop:charLambda1}
Let $(X,\tau)$ be a topological space and $\mathcal{F}:\mathcal{O}(X)^{\textrm{op}}\to \dSet$ be a presheaf.
Then
\begin{itemize}
\item
$B^1_\F$ is a base of compact open sets for $(\Lambda^1_\F,\tau^1_\F)$; hence $(\Lambda^1_\F,\tau^1_\F)$ is locally compact.
\item
For any $G\in\St(\RO(X))$ the stalk $\F_G$ over $G$ in $\Lambda^1_\F$ is a discrete and closed
subspace.
\item
$p^1_\F:\, \Lambda^1_\F\to \St(\RO(X))$ is the bundle associated to $(\Lambda^1_\F,\tau^1_\F)$, and each $\dot{f}$ is a local section over $\Reg{U}$ whenever $f\in \F(U)$; hence $\Lambda^1_\F$ is an \'etal\'e space over $\St(\RO(X))$.
\item

$\Lambda^1_\F$ is Hausdorff and $0$-dimensional, in particular it is Tychonoff.
\item
If $\Lambda^1_\F$ has an infinite stalk, it is non-compact.

\end{itemize}
\end{proposition}

\begin{proof}
\emph{}

 \begin{description}
 \item[$B^1_\F$ is a base for $\tau^1_\F$] It suffices to show that  finite intersections of elements of $B^1_\F$ are unions of elements of $B^1_\F$. We sketch the argument for binary intersections and leave to the reader the general case.
 Note that $[f]_G=[h]_K$ if and only if $G=K$ and $D_{f,g}$ is dense below $U$ for some $U\in G$.
 This gives that for $q\subseteq\Reg{U_f}$, $r\subseteq \Reg{U_g}$
\begin{align*}
\dot{f}[q]\cap\dot{g}[r]=&
\bp{[f]_G:\, [f]_G=[g]_G,\, q\wedge r\in G}=\\
=&\bp{[f]_G:\,\exists\,W\subseteq q\cap r,\, D_{f,g}\text{ is dense below }W\text{ and } W\in \bar{G}}\\

=&\bigcup\bp{\dot{f}[\Reg{W}]: \,W\subseteq q\cap r,\, D_{f,g}\text{ is dense below }W,\,W\in\mathcal{O}_X}.
 \end{align*}

 \item[$\dot{f}$ is a local section over $\Reg{U}$ whenever $f\in \F(U)$]
 It is clear that $\dot{f}$ is injective and $(p^1_\F\circ\dot{f})(G)=G$ for any $G\in \Reg{U}$; furthermore for any  $V\subseteq \Reg{U}$ open set of $\St(\RO(X))$
 \[
 \dot{f}[V]=\bigcup\bp{\dot{f}[q]:\,  q\subseteq V, q\in\RO(X)=\CLOP(\St(\RO(X)))}.
 \]
 This easily gives that $\dot{f}$ is open and continuous on its domain.

 \item[$(\Lambda^1_\F,\tau^1_\F)$ is locally compact] This is an immediate consequence of the already established fact that each local section $\dot{f}$ is an homeomorphism of the compact subspace
 $\Reg{U_f}$ of $\St(\bool{B})$ with the open subspace $\dot{f}[\Reg{U_f}]$ of $\Lambda^1_\F$.

  \item[$p^1_\F$ is continuous] For any $U$ open in $\St(\RO(X))$,
 \[
 (p^1_\F)^{-1}[U]=\bigcup\bp{\dot{f}[\Reg{V}]: \Reg{V}\subseteq U,\, f\in \F(V)},
 \]
 hence it is a union of basic open sets.

\item[The stalks of $\Lambda^1_\F$ are discrete and closed] The complement of the stalk on some $G\in \St(\RO(X))$ is given by the union of the images of sections in $\Gamma^0_{p^1_\F}$ on $\St(\RO(X))\setminus\bp{G}$, hence the stalk on $G$ is closed; any stalk is also discrete (the intersection of a local section with a stalk is a point).

  \item[$\Lambda^1_\F$ is Hausdorff and $0$-dimensional] The delicate part is to establish the Hausdorff separation property. In this task the only interesting case is how to separate points
 $[f]_G\neq[g]_G$ on the same stalk over $G\in \St(\bool{B})$ with $f\in \F(U_f)$, $g\in \F(U_g)$,
 $\Reg{U_f},\Reg{U_g}\in G$.\\

  Let (in $\RO(X)$)

  $b=\bigvee_{\RO(X)} D_{f,g}$. Then either $b\in G$ or $\neg b\in G$. Clearly $b\notin G$ else
  $p=b\wedge \Reg{U_f}\wedge \Reg{U_g}$ is in $G$ and $D_{f,g}$ is dense below it, yielding
  $[f]_G=[g]_G$. Hence $\neg b\in G$. Now if $V\subseteq p=\neg b\wedge \Reg{U_f}\wedge \Reg{U_g}$ is open in $X$, we have that $V\not\in D_{f,g}$. Hence $f\restriction V\neq g\restriction V$ for all $V\subseteq p$ in $\mathcal{O}(X)$, therefore $[f]_H\neq [g]_H$ for all $H\in p$.

 This gives that $\dot{f}[p]$ and $\dot{g}[p]$
 are disjoint, and each is a compact open neighborhood respectively of $[f]_G$, $[g]_G$.

 Since each $\dot{f}[\Reg{U_f}]$ is compact, it is also closed
 in $\Lambda^1_\F$ (because $\Lambda^1_\F$ is Hausdorff), hence the family of local sections $\dot{f}[\Reg{U}]$ for $f\in \F(U)$ provides a base of clopen sets for $\Lambda^1_\F$.

 \item[$\Lambda^1_\F$ is non-compact if some stalk of $\Lambda^1_\F$ is infinite] An infinite stalk of $\Lambda^1_\F$ is a closed and discrete (hence non-compact) subset; hence
$\Lambda^1_\F$ is not compact, being Hausdorff and containing a closed non-compact subset.

 \end{description}
 \end{proof}
Given a locally compact Hausdorff space $(X,\tau)$ let $\beta_0(X)$ denote its one point compactification $X\cup\bp{\infty}$ with neighborhood of $\infty$ given by the complements of compact subsets of $X$.

We can now introduce the type of sheaf we want to associate to bundles. Compactifications will play a crucial role in our ability to describe global sections; thus we limit the scope of our definition to bundles $p:E\to X$ with $E$ locally compact Hausdorff\footnote{Actually we could be slightly more liberal  in Definition \ref{def:sheafregbundle} and allow $E$ to be Tychonoff space (in which case in the rest of Definition \ref{def:sheafregbundle} we should replace $\beta_0(E)$ with $\beta(E)$). In order for Definition \ref{def:sheafregbundle} to work properly, we only need to be able to define an Hausdorff compactification of $E$, which is the case if the latter is Tychonoff.
However to define the stonean sheafification of a presheaf $\F$, it suffices to consider $E$ locally compact Hausdorff, since so is $\Lambda^1_\F$.}.

  \begin{definition}\label{def:sheafregbundle}
  A continuous map $p:E\to X$ is an \emph{extremally disconnected bundle} if:
 \begin{itemize}
 \item $E$ is locally compact and $X$ is Hausdorff, extremally disconnected, and compact;
 \item $p[E]$ is a dense open subset of $X$.
 \end{itemize}
 Let $p:E\to X$ be  an extremally disconnected bundle;
$\Gamma^1_p:\mathcal{O}(X)^\text{op}\to\dSet$ is defined by:
\begin{itemize}
\item
$\Gamma^1_p(U)$ is the set of continuous $f:U\to \beta_0(E)$ such that:
\begin{itemize}
\item
$\bp{x\in U:\, f(x)\in E}$ contains an open dense subset $D_f$ of $U$;
\item
 $f\restriction D_f$ is a local section of $p$ (e.g.
$f\restriction D_f\in \Gamma^0_p(D_f)$);
\end{itemize}
\item
$\Gamma^1_p(U\subseteq V)(f):=f\restriction U$ for every $f\in\Gamma^1_p(V)$.
\end{itemize}

$\Gamma^{1/2}_p$ is given by $\Gamma^1_p\restriction \RO(X,\tau)^+$.
 \end{definition}

 \begin{proposition}
 Let $p:E\to X$ be an extremally disconnected  bundle.
 Let also $U\in\mathcal{O}(X)$ and
 $f\in\prod_{\bp{G\in U}} (p^{-1}[\bp{G}]\cup\bp{\infty})$. The following are equivalent:
 \begin{itemize}
 \item $f$ is a local section of $p$ over $U$ for $\Gamma^1_p$;
 \item $f:U\to \beta_0(E)$ is open and continuous and $f^{-1}[\bp{\infty}]$ is nowhere dense in $U$.
 \end{itemize}
 \end{proposition}
 \begin{proof}
 One implication is trivial.
 Now assume $f:U\to \beta_0(E)$ is open and continuous and $f^{-1}[\bp{\infty}]$ is nowhere dense in $U$. Then
 \[
D_f=\bp{G\in U: f(G)\in E}
 \]
 is open and dense in $U$.

 Since $f$ is open and continuous for each $G\in D_f$ there is some $g_G:U_G\to E$ local homeomorphism with $G\in V_G\subseteq U_G$, $f(G)=g_G(G)$, $V_G$ clopen subset of $D_f$,
 $U_G$ clopen subset of $X$, $g_G[U_G]$ clopen subset of $E$, $f[V_G]\subseteq g_G[U_G]$.
 Hence $f\restriction D_f=\bigcup_{G\in D_f}g_G\restriction V_G$ is a local section.
Since $D_f$ is a dense subset of $U$, we conclude that $f\in \Gamma^1_p(U)$.
\end{proof}

\begin{proposition}
\label{gamma1:sheaf}
For any extremally disconnected  bundle $p:E\to X$, $\Gamma^1_p$ is a stonean sheaf
and $\Gamma^{1/2}_p$ is a sheaf both for the sup-topology on $\RO(X)$ and for the dense topology on
$\RO(X)^+$.
\end{proposition}

\begin{proof}
We prove the thesis in details for $\Gamma^{1/2}_p$ with respect to the sup-topology on $\RO(X)$, we leave to the reader the details for the other assertions.

Since $X$ is Hausdorff extremally disconnected  compact, $\Reg{U}=\Cl{U}$ for every open $U\subseteq X$; therefore (by Proposition \ref{comp:exdisc}) for any open $U\subseteq X$ its Stone-\v{C}ech compactification $\beta(U)$ is (homeomorphic to) $\Reg{U}$ and
any continuous function $f$ defined on some open subset
$U\subseteq X$ and range in a compact Hausdorff space admits a unique continuous extension $\beta(f)$ to $\Cl{U}=\Reg{U}=\beta(U)$.

Assume now $\bp{f_i:U_i\to \beta_0(E):i\in I}$ is a matching family for $\Gamma^{1/2}_p$.
Then, letting $f=\bigcup_{i\in I} f_i$, $f$ has domain $U=\bigcup_{i\in I}U_i$ and $\beta(f)$ is continuous with domain the clopen set
\[
\bigvee_{\RO(X)}\bp{U_i:i\in I}=\Cl{U}
\]
and collates the matching family in $\Gamma^{1/2}_p$; furthemore
$D_f=\bigcup_{i\in I}D_{f_i}\subseteq U$ is a dense open subset of $\Cl{U}$ on which $f$ takes values in $E$, and $f\restriction D_f$ is a local section of $\Lambda^0_p$. Hence $\beta(f)$ is the unique continuous extension of the local section $f\restriction D_f\in \Gamma^0_p(D_f)$ to a function with range in $\beta_0(E)$, and $\beta(f)$ can take as value the unique point $\infty \in\beta_0(E)\setminus E$ only on the nowhere dense closed set $\Cl{U}\setminus D_f$.
\end{proof}

 \begin{proposition}
  Let $X$ be an extremally disconnected  compact Hausdorff space.
 $\F$ is a stonean sheaf on $X$ if and only if (up to a natural isomorphism)
 $\F\cong\Gamma^{1}_{p^1_\F}$ and each local section of $\Gamma^{1}_{p^1_\F}$ takes values only in $\Lambda^1_{\F}$.
 \end{proposition}
 \begin{proof}
 Since $X$ is extremally disconnected  compact Hausdorff space we have that up to homeomorphism $\F$ and $\Gamma^{1}_{p^1_\F}$ are stonean sheaves on $X$.

stonean sheaves are uniquely determined by the global sections, hence we just need to find a natural identification of $\F(X)$ with $\Gamma^{1}_{p^1_\F}(\St(\RO(X))$.

Now an element of  $\Gamma^{1}_{p^1_\F}(\St(\RO(X))$ is some $f:\St(\RO(X))\to\beta_0(E)$
such that on some $D_f$ dense subset of $\St(\RO(X))$, $f\restriction D_f$ takes vaules in $E$,
$f=\beta(f\restriction D_f)$ and furthermore $D_f=\bigcup_{i\in I}V_i$ so that:
\begin{itemize}
\item $f\restriction V_i=\dot{f}_i$ for some $f_i\in \F(V_i)$,
\item $V_i$ is regular open in $X$ for all $i\in I$.
\end{itemize}
This gives that the family $\bp{f_i:i\in I}$ is a compatible family in $\F$ and $\bp{V_i:i\in I}$
is a dense covering of $X$. Since $\F$ is a stonean sheaf, there is some $h\in \F(X)$ such that
$h\restriction V_i=f_i$ for all $i\in I$.
Then $\dot{h}:\St(\RO(X))\to\beta_0(E)$ takes values only in $E$ and
\[
\dot{h}(G)=[h]_G=[f_i]_G=\dot{f}_i(G)=f(G)
\]
for all $G\in V_i$ and $i\in I$.
Hence $f$ is $h$ since they are both continuous and overlap on the dense set $D_f$ (modulo the identification of $X$ with $\St(\RO(X))$).
\end{proof}

\begin{corollary}
Let $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ be a stonean sheaf with $X$ extremally disconnected  compact Hausdorff. Then (up to natural isomorphism)  there is an extremally disconnected and surjective bundle $p_\F:E_\F\to X$ such that for each $U$ open in $X$
$\F(U)$ is the family of sections $f:U\to E_\F$ and the pointwise image of these sections form a base of clopen sets for $E_\F$.
\end{corollary}

\begin{corollary}\label{cor:adjEDCH}
Let $X$ be extremally disconnected  compact Hausdorff.
Then the pair $\Gamma^1\circ\Lambda^1$ is left adjoint of the inclusion functor between the category $\Presh(X,\dSet)$ and the category $\Sh^*(X,\dSet)$ of stonean sheaves on $X$.
\end{corollary}
The above can be proved using the general methods on sheafification of presheaves with respect to Grothendieck topologies as given in \cite[III]{MacLMoer}.

\subsection{Stonean sheafification as an adjoint functor}\label{subsec:stsheafadj}

We aim for a more general adjunction result than the one given in Corollary \ref{cor:adjEDCH} as the latter
does not describe the relation between
$\Presh^*(X,\dSet)$ and $\Sh^*(\St(\RO(X)),\dSet)$ given by the functor $\Gamma^1\circ\Lambda^1$ when $X$ is not extremally disconnected, compact Hausdorff.

Toward this aim we need to describe what are the natural morphisms between presheaves
defined on different topological spaces.

We have to give an ad-hoc definition (or at least one not present in \cite[I]{MacLMoer}),
since such morphisms are comparing functors defined on different categories.

Since our focus is on the sheafification process induced by the dense topology,
we should consider only morphisms from $\F_0$ to $\F_1$
for $\F_i:X_i\to\dSet$ which map
compatible families of functions in $\F_0$ indexed by a dense covering of some open set of $X_0$ to compatible functions of functions in $\F_1$ indexed by a dense covering of the corresponding (via the morphism) open set of $X_1$. Furthermore these morphisms should map a collation of such a compatible families existing in $\F_0$ to a
collation of the pointwise image under the morphism of such a compatible family existing in $\F_1$.
If these requests are not met by a potential morphism, this potential morphism may not commute with the sheafification process applied on each of the $\F_i$. We will see that these are the unique requests we must impose.

To define these morphisms we first need to view presheaves as presheaves of local sections (e.g. presheaves $\F$ such that
$\F(U)$ is a set of maps with domain $U$). This can be done using the
functor $\Gamma^0\circ\Lambda^0$ (see \cite[II]{MacLMoer}).
\begin{fact}
Let $\F:\mathcal{A}\to\dSet$ be a presheaf defined on some $\mathcal{A}\subseteq\mathcal{O}(X)$. Then
$\F$ is naturally isomorphic in the category $\Presh(\mathcal{A},\dSet)$ to the functor $\mathrm{ls}(\F)$
defined on objects by
$U\mapsto\bp{(\Gamma^0\circ\Lambda^0)_U(f):f\in\F(U)}$ where
\[
(\Gamma^0\circ\Lambda^0)_U(f)=\bp{\ap{x,[f]_{\sim_x}}:\, x\in U}
\]
for any $U\in\mathcal{A}$ and $f\in \F(U)$ and on arrows by
\[
(U\subseteq V)\mapsto (f\in\mathrm{ls}(\F)(V)\mapsto f\restriction U).
\]
\end{fact}

Furthermore it is useful to note that the stonean sheafification of some presheaf $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ depends only on $\F\restriction\RO(X)$ (at least when the regular opens are a base for the topology).
\begin{fact}\label{fac:extrestrpreshROX}
Let $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ be a presheaf on $(X,\tau)$, and $\mathcal{G}:\RO(X)^{\mathrm{op}}\to\dSet$
be also a presheaf (of local sections). Define $\mathrm{ext}(\mathcal{G}):\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ on objects by
\[
\mathrm{ext}(\mathcal{G})(U)=\mathcal{G}(\Reg{U})\restriction U,
\]
and on arrows
\[
\mathrm{ext}(\mathcal{G})(U\subseteq V): f\in \mathrm{ext}(\mathcal{G})(V) \mapsto f\restriction U.
\]

Then with respect to the categories of presheaves on $\mathcal{O}(X)$ and of presheaves on $\RO(X)$:
\begin{itemize}
\item $\mathrm{ext}$ is left adjoint to $\F\mapsto \F\restriction\RO(X)$,
$\mathrm{ext}(\F)\restriction\RO(X)=\F$, and $\mathrm{ext}(\F\restriction\RO(X))$ is a subobject of $\F$ in $\Presh(X,\dSet)$.
\item
If $\RO(X)$ is a dense subset of $\mathcal{O}(X)$, then for any $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$
\[
\Gamma^1\circ\Lambda^1\circ\mathrm{ext}(\F\restriction\RO(X))=
\Gamma^1\circ\Lambda^1(\F).
\]
\end{itemize}
\end{fact}

These facts show that morphisms on presheaves in order to commute with stonean sheafifications
should not depend on their behaviour outside of the regular open sets.

We should also expect that a morphism  $\iota:\F_0\to\F_1$ naturally induces an order morphism
$k_\iota:\mathcal{O}(X_0)\to\mathcal{O}(X_1)$.
If $\iota$ maps compatible families indexed by dense coverings to compatible families indexed by dense coverings, we must have that $k_\iota$ maps dense coverings to dense coverings.
In view of Proposition \ref{thm:openmap-->adjoint} we may consider only $k_\iota$ of the form $\bar{\bar{k}}_f$ for some continuous open $f:X_1\to X_0$ or (more generally)
such that $k_\iota\restriction\RO(X)$ is a complete homomorphism\footnote{Note that
there can be
complete homomorphisms $k:\RO(X)\to\RO(Y)$ which are not of the form $k_f$ for any continuous open $f:Y\to X$. For example let $k:\pow{\bp{0,1}}\to\RO([0;1])$ be given by
$k(\bp{0})=[0;1/2)$, $k(\bp{1})=(1/2;1]$. Then no continuous function $f:[0;1]\to \bp{0,1}$ can have $k$ as $k_f$.}.

Also we can naturally lift using continuous maps (or complete homomorphisms on regular open algebras) a presheaf (of local sections)
to a presheaf (of local sections) as follows:
\begin{notation}
Let $f:Y\to X$ be a continuous open function,
$\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$ be a presheaf,
$\Theta:\F_0\to\F_1$ be a natural transformation of presheaves on $X$.

We let:
\begin{itemize}
\item
$f^*(\F):\mathcal{O}(Y)^{\mathrm{op}}\to\dSet$ be the presheaf defined by
\[
U\mapsto\bp{g\circ f: g\in \F(f[U])}
\]
for $U\in\mathcal{O}(Y)$,
and by
\[
(U\subseteq V)\mapsto \bp{g\circ f\restriction U: g\in \F(f[V])}
\]
for $U\subseteq V$ and both in $\mathcal{O}(Y)$.

We let for $g\in\F(f[U])$ $f^*(g)$ be the section $g\circ f$ of $f^*(\F)(U)$.
\item
$f^*(\Theta)$  be defined by
\begin{align*}
f^*(\Theta)_U: & f^*(\F_0)(U)\to f^*(\F_1)(U)\\
&  g\circ f\mapsto \Theta_{f[U]}(g)\circ f
\end{align*}
for $U$ in $\mathcal{O}(Y)$ and $g\in \F_0(f(U))$.

\end{itemize}

Conversely let $i:\RO(X)\to\RO(Y)$ be a complete homomorphism.
Then it admits $\pi_i:\RO(Y)\to\RO(X)$ left adjoint map.

We let:
\begin{itemize}
\item
 $i_*(\F\restriction\RO(X)):\RO(Y)^{\mathrm{op}}\to\dSet$ be defined by
\[
U\mapsto \F(\pi_i(U))
\]
for $U\in\RO(Y)$,
and by
\[
(U\subseteq V)\mapsto \F(\pi_i(U)\subseteq \pi_i(V))
\]
for $U\subseteq V$ and both in $\RO(Y)$.
\item
$i_*(\Theta\restriction\RO(X))$  be defined by
\begin{align*}
i_*(\Theta)_U: & i_*(\F_0)(U)\to i_*(\F_1)(U)\\
&  h\mapsto \Theta_{\pi_i(U)}(h)
\end{align*}
for $U\in\RO(Y)$ and $h\in \F_0(\pi_i(U))$.

\end{itemize}
$i_*(\F)$ is defined to be $\mathrm{ext}(i_*(\F\restriction\RO(X)))$ and
$i_*(\Theta)$ is defined as $\mathrm{ext}(i_*(\Theta\restriction\RO(X)))$.
\end{notation}
It is clear that (up to natural isomorphism) $f^*= (k_f)_*$.

We see below that both of the above lifting operators are well defined and
commute well with the stonean sheafification operation.

\begin{notation}
Given a topological space $(X,\tau)$ we let
$i_{X}:\RO(X)\to\CLOP(\St(\RO(X)))$ be the Stone duality map
\[
V\mapsto N_V=\bp{G\in\St(\RO(X)): V\in G}.
\]
In case $(X,\tau)$ is compact Hausdorff we also define the natural projection
$\pi_X:\St(\RO(X))\to X$ which maps $G$ to the unique point in $\bigcap\bp{\Cl{U}: U\in G}$.
\end{notation}
For $\F$ a presheaf on $(X,\tau)$ and $\Theta$ a natural transformation on presheaves on $X$, we have that $(i_X)_*(\F)$ is a presheaf on $\St(\RO(X))$ and
$(i_X)_*(\Theta)$ is a natural transformations of presheaves on $\St(\RO(X))$.
Furthermore in case $X$ is compact Hausdorff $(\pi_X)^*(\F)$ is up to isomorphism equal to $(i_X)_*(\F)$ and the same holds for $(\pi_X)^*(\Theta)$ and $(i_X)_*(\Theta)$ (now in the category of natural transformations on presheaves on $\St(\RO(X))$).

The key property of these lifting operators is that they commute well with stonean sheafification
(Recall Definition \ref{def:adjhom} for the definition of
$\pi^*_i:\St(\RO(Y)\to\St(\RO(X))$)

\begin{lemma}\label{lem:liftcommsheaf}
Let $\Theta:\F_0\to\F_1$ be a natural transformation for presheaves $\F_j:\mathcal{O}(X_j)\to\dSet$ and $i:\RO(X_0)\to\RO(X_1)$ be a complete homomorphism.

Then:
\begin{itemize}
\item
$(\pi^*_i)^*(\Gamma^1\circ\Lambda^1(\F_0))\cong \Gamma^1\circ\Lambda^1(i_*(\F_0))$,
\item
$(\pi^*_i)^*(\Gamma^1\circ\Lambda^1((i_{X_0})_*(\Theta)))\cong \Gamma^1\circ\Lambda^1((i_{X_1})_*\circ i_*(\Theta))$.
\end{itemize}
\end{lemma}

\begin{proof}
A detailed proof of all items requires a careful diagram chasing, which we do not want to pursue in its entirety.
We give a few key hints of why everything works well for presheaves $\F:\mathcal{O}(X)^{\mathrm{op}}\to\dSet$. The case of natural transformations is notationally much more involved but does not need any further idea, hence we dare to leave it to the reader.

Let  $g:A\to\beta(\Lambda^1_{i_*(\F)})$ be a local section of $\Gamma^1\circ\Lambda^1(i^*(\F))$ for some $A$ open in $\St(\RO(Y))$.
Then $g$ is the collation in
$\Gamma^1\circ\Lambda^1(i^*(\F))$
of local sections $\bp{g_i: i\in I}$ such that:
\begin{itemize}
\item
each
\[
g_i=\dot{h}_i=\bp{\ap{H,[h_i]_H}:\, V_i\in H,\, h_i\in \F(i(V_i))}
\]
for some
$h_i\in \F(i(V_i))$ and $V_i\in\RO(Y)$;
\item
$\bigcup\bp{N_{V_i}: i\in I}$ is a dense subset of $A$ in $\St(\RO(Y))$.
\end{itemize}
We note that this imposes that $\bp{h_i:i\in I}$ is a compatible family of local sections in $\F$ each one defined on the open set $i(V_i)$ with $\bigcup\bp{N_{i(V_i)}: i\in I}$ a dense subset of the open set
$B=\Reg{\bigcup_{i\in I}N_{i(V_i)}}$ in $\St(\RO(X))$ and also with $(\pi^*_{i})^{-1}[B]$ containing $A$ has a dense subset (since $\pi^*_i[N_V]=N_{\pi_i}(V)$ for any $V\in \RO(Y)$).
Since
$\Gamma^1\circ\Lambda^1(\F)$ is a stonean sheaf, there is a unique collation $\bar{g}$ of $\bp{\dot{h}_i:i\in I}$
defined on $\Reg{B}$. Then $(\pi^*_{i})^*(\bar{g})=\bar{g}\circ\pi^*_{i}$ and $g$ coincide on the dense in $A$ open set
$\bigcup\bp{N_{V_i}: i\in I}$, hence they must be equal on $A$.

A similar reasoning shows the converse inclusion.

The case of natural transformations is notationally more involved and is also left to the reader.
\end{proof}

We condense these observations in the following definition:

\begin{definition}\label{def:presh*morph}
Let  $\F_0$ and $\F_1$ be presheaves
$\F_i:\mathcal{O}(X_i)^{\mathrm{op}}\to\dSet$ for $i=0,1$.

$\iota=(i_\iota,\Theta_\iota)$ defines a morphism of $\F_0$ to $\F_1$ if:
\begin{itemize}
\item $i_\iota:\RO(X_0)\to \RO(X_1)$ is a complete homomorphism;
\item $\Theta_\iota:(i_\iota)_*(\F_0)\to \F_1$ is a
natural transformation in the category $\Presh(X_1,\dSet)$.

\end{itemize}
\end{definition}

\begin{definition}
$\Presh^*(\dSet)$ is the category of presheaves on the open sets of some topological space
with morphisms given by Definition \ref{def:presh*morph}.

$\Sh^*(\dSet)$ is the subcategory of $\Presh^*(\dSet)$ given by stonean sheaves $\F:\mathcal{O}(X)^\text{op}\to\dSet$
for some compact Hausdorff extremally disconnected $(X,\tau)$.
\end{definition}

We are now in the position to state our adjunction result for the sheafification process induced
by $\Gamma^1\circ\Lambda^1$.

To formulate it we just need to define precisely how
$\Gamma^1\circ\Lambda^1$ acts on the morphisms of $\Presh^*(\dSet)$.

\begin{definition}\label{def:morphpresh}
Let $\iota=(i_\iota,\Theta_\iota)$ be a morphism of $\F_0$ to $\F_1$
induced by a complete homomorphism $i_\iota:\RO(X_0)\to \RO(X_1)$ and a natural transformation $\Theta_\iota$ of
$\Presh(X_1,\dSet)$ from $(i_\iota)_*(\F_0)$ to $\F_1$.

Then
\[
\Gamma^1\circ\Lambda^1(\iota)=\iota^1=(i^1_\iota,\Theta^1_\iota)
\]
is defined as follows:
\begin{itemize}
\item $i^1_{\iota}=k_{\pi^*_{i_\iota}}:\RO(\St(\RO(X_0)))\to \RO(\St(\RO(X_1)))$ which maps $N_U$ to $N_{i_\iota(U)}$ (recall Notation \ref{not:kfpii}).
\item
$\Theta^1_\iota$ is $\Gamma^1\circ\Lambda^1((i_{X_1})_*(\Theta_\iota))$.
\end{itemize}
\end{definition}

\begin{lemma}
For each presheaf morphism $\iota=\ap{i_\iota,\Theta_\iota}$ of $\F_0$ to $\F_1$,
$\Theta^1_\iota$ as defined in \ref{def:morphpresh} is a well-defined natural transformation.
\end{lemma}
\begin{proof}
This is a tiresome check we leave to the reader. The key point is that the required compositions and liftings commute with collations of local sections in view of Lemma \ref{lem:liftcommsheaf}.
\end{proof}

\begin{theorem}\label{thm:gamma1adj}
$\Gamma^1\circ\Lambda^1$ is a well defined functor.

Furthermore the inclusion functor of $\Sh^*(\dSet)$ into $\Presh^*(\dSet)$
is right adjoint to $\Gamma^1\circ\Lambda^1$.
\end{theorem}

The proof of this theorem is a lengthy and tiresome check that (any of the standard set of) the clauses defining an adjunction are satisfied by $\Gamma^1\circ\Lambda^1$.

We briefly outline some delicate points of the proof, but we omit a detailed argument since it would only amount to a few pages of uninformative and tiresome calculations.

\begin{proof}
The first delicate point is to check that $\Gamma^1\circ\Lambda^1$
is well defined on morphisms $\iota$. This is the content of Lemma
\ref{lem:liftcommsheaf}.

 The functoriality of $\Gamma^1\circ\Lambda^1$ is a tiresome check we leave to the reader.

 The key ideas in the  proof that $\Gamma^1\circ\Lambda^1$ is a left adjoint follow again from
 Lemma \ref{lem:liftcommsheaf}.
 \end{proof}

There are some key observations to make:
\begin{remark}
\emph{}
Assume $\bool{B}=\RO(X,\tau)$
for some Tychonoff topological space $(X, \tau)$ and $\mathcal{F}:\mathcal{O}(X)^{\textrm{op}}\to \dSet$ is a separated presheaf. In particular $\RO(\St(\bool{B}))=\bool{B}$ and thus $\Lambda^1_{\F}$ is an \'etal\'e space on $\St(\bool{B})$
and $p^1_\F$ is an extremally disconnected bundle.
Then
$\Gamma^1_{p^1_\F}$ and $\Gamma^0_{p^0_\F}$ can have really little to share:
\begin{itemize}
\item If $X$ is connected
there cannot be a continuous map of $X$ into $\St(\RO(X))$ since the latter is $0$-dimensional.
\item
Since $X$ admits a base of regular open sets, we have a natural projection of a dense subset of $\St(\RO(X))$ to $X$ mapping $G$ to $x$ if $G$ extends the filter of regular open neighborhoods of $X$ (however this filter need not be a maximal filter of open sets: consider the case of the filter of regular open
neighborhoods of
$1/2$ for $[0;1]$ with euclidean topology).
\end{itemize}
In particular certain maximal filters on $\RO(X)$ do not correspond to points of $X$ (if $X$ is non-compact), or there could be points in $X$
whose filter of open neighborhoods admits different extensions to maximal filters on $\RO(X)$.\\

Assume now $(X,\tau)$ is compact Hausdorff and extremally disconnected.
Then $\St(\RO(X))=\St(\CLOP(X))$
is homeomorphic to $X$ via the map
\[
x\mapsto G_x=\bp{U\in \RO(X,\tau):\, x\in U}.
\]
Fix any presheaf $\mathcal{F}:\mathcal{O}(X)^{\textrm{op}}\to \dSet$ with base set $X$.
We can use Proposition \ref{comp:exdisc} to argue that $[f]_G=[g]_G$ holds in $\Lambda^1_\F$ if and only if $[f]_G=[g]_G$ holds in $\Lambda^0_\F$. This yields that $\Lambda^0_\F$ and $\Lambda^1_\F$ (as well as $p^0_\F$ and $p^1_\F$) are the same.

Now $\Gamma^1_{p^1_\F}$ and $\Gamma^0_{p^0_\F}$ are both sheaves $\mathcal{O}(X)^{\textrm{op}}\to\dSet$. However they may be different (see the following example).
\end{remark}

\begin{example}

 Let
 $(X,\tau)$ be a compact Hausdorff extremally disconnected,  and
 $\C(X)$ be the set of continuous complex valued functions on $X$.
 $\C(X)$ is  the set of global sections of the sheaf $\F$ of continuous complex valued functions defined on an open subset of $X$. This amounts to say that (up to functorial equivalence)
 $\F$ is exactly $\Gamma^0_{p^0_\F}$.
 Notice however that, even though $\F$ is a topological sheaf on the topological space $X$, when restricted to $\bool{B}^+=\RO(X)\setminus\bp{\emptyset}$ it is not anymore a sheaf on the partial order $\bool{B}^+$ with coverings given by the double negation topology (e.g. $\Gamma^0_{p^0_\F}\restriction \RO(X)^+$ is not a sheaf).

To see this, let $\bp{U_n:n\in\mathbb{Z}}$ be a maximal antichain of $\RO(X)^+$ and let $f_n\in \F(U_n)$ be constant with value $n$. Then $\bp{f_n:n\in\mathbb{Z}}$ is a matching family of $\Gamma^0_{p^0_\F}\restriction \RO(X)$
which cannot be collated in $\Gamma^0_{p^0_\F}\restriction\RO(X)^+$ (but can be collated in $\Gamma^{1}_{p^0_\F}$). The point being that for $G\in X\setminus \bigcup_{n\in\mathbb{Z}}U_n$
$\beta(f):X\to\beta_0(\Lambda^1_\F)$ maps $G$ to $\infty$.

Consider now the set
\[
\C^+(X):=\bp{f:X\to\beta_0(\mathbb{C}): f \textit{ is continuous and }f^{-1}[\{\infty\}]\textit{ is nowhere dense}}.
\]
It turns out that $\C^+(X)$ defines the global sections of the \emph{stonean sheafification} $\Gamma^{1}_{p^1_\F}$ of the sheaf $\F$ associated to $\C(X)$.

Indeed, we already noticed that $\Lambda^1_{\F}=\Lambda^0_{\F}$, since $X$ is homeomorphic to $\St(\RO(X))$. Now, if $s\in\Gamma^1_{\Lambda^0_{\F}}(X)$, then we can find a family
$\{V_i: i\in I\}$ of (disjoint) regular open subsets of $X$ such that $\bigcup_{i\in I}V_i$ is open dense in $X$ and $s\restriction V_i=\dot{f}_i$ for some $f_i\in\C(V_i)$. Then $\bigcup_{i\in I}f_i\in\C(\bigcup_{i\in I}V_i)$ and thus $s\restriction\bigcup_{i\in I}V_i=(\bigcup_{i\in I}f_i)\restriction\bigcup_{i\in I}V_i$. Therefore we can identify $s$ with the unique continuous extension $\beta(\bigcup_{i\in I}f_i):X=\beta(\bigcup_{i\in I}V_i)\to\beta_0(\mathbb{C})$, which is an element in $\C^+(X)$.
\end{example}

In model theoretic terms (according to the terminology we introduce in Section \ref{sec:boolvalmod})  $\C(X)$ (seen as a $\RO(X)$-valued model) does not have the mixing property (see Proposition \ref{chr:mix}), while $\C^+(X)$ does. \cite{VIAVAC15} gives a detailed analysis of the boolean valued model structure of $\C(X)$ and $\C^+(X)$.
Other connections between functional analysis, sheaf theory, and set theory will be given in Example \ref{exm:sheafLR}.

We end this section with the following corollary, which stresses the fact that our stonean sheafification is exactly the generalization to topological spaces of the usual sheafification process for presheaves defined on complete boolean algebras.
\begin{corollary}
Let $\bool{B}=\RO(\St(\bool{B}))$ be a complete boolean algebra. Then the functor $\Presh(\bool{B}, \dSet)\to\Sh(\bool{B}, \dSet)$ such that $\F\mapsto(\Gamma^{1/2}\circ\Lambda^1)(\mathrm{ext}(\F))$ is the left adjoint of the inclusion of $\Sh(\bool{B}, \dSet)$ in $\Presh(\bool{B}, \dSet)$ (where $\Sh(\bool{B}, \dSet)$ is the category of sheaves according to the sup Grothendieck topology).
\end{corollary}

\section{Boolean valued models}\label{sec:boolvalmod}
We consider only boolean valued models for relational languages as (at least for our purposes) there is no lack of generality in doing so, and our proofs are notationally smoother in this set up.
\begin{definition}\label{def:boolvalmod}
Let $\LL=\bp{R_i: i\in I, c_j: j\in J}$ be a relational language (i.e. without functional symbols; constant symbols are allowed) and let $\bool{B}$ be a boolean algebra. A \emph{$\bool{B}$-valued model} $\M$ for $\LL$ consists of:
\begin{enumerate}
\item a non-empty set $M$, called the \emph{domain} of $\M$;
\item the boolean value of the equality symbol, which is a function
\[
\begin{aligned}
=^\M:&M^2\to\bool{B}\\
\ap{\sigma,& \tau}\mapsto\Qp{\sigma=\tau}^\M_{\bool{B}}
\end{aligned};
\]
\item for each $n$-ary relational symbol $R\in\LL$, a function
\[
\begin{aligned}
R^\M:&M^n\to\bool{B}\\
\ap{\sigma_1, \dots,& \sigma_n}\mapsto\Qp{R(\sigma_1, \dots, \sigma_n)}^\M_{\bool{B}}
\end{aligned};
\]
\item for each constant symbol $c\in\LL$, an element $c^\M\in M$.
\end{enumerate}
We require the following conditions to hold:
\begin{enumerate}
\item for every $\sigma, \tau, \pi\in M$,
\[
\begin{gathered}
\Qp{\sigma=\sigma}^\M_{\bool{B}}=1_{\bool{B}},\\
\Qp{\sigma=\tau}^\M_{\bool{B}}=\Qp{\tau=\sigma}^\M_{\bool{B}},\\
\Qp{\sigma=\tau}^\M_{\bool{B}}\wedge\Qp{\tau=\pi}^\M_{\bool{B}}\leq\Qp{\sigma=\pi}^\M_{\bool{B}};
\end{gathered}
\]
\item for every $n$-ary relational symbol $R\in\LL$ and for every $\sigma_1, \dots, \sigma_n, \tau_1, \dots, \tau_n\in M$,
\[
\Bigl(\bigwedge_{i=1}^n\Qp{\sigma_i=\tau_i}^\M_{\bool{B}}\Bigr)\wedge\Qp{R(\sigma_1, \dots, \sigma_n)}^\M_{\bool{B}}\leq\Qp{R(\tau_1, \dots, \tau_n)}^\M_{\bool{B}}.
\]
\end{enumerate}
A $\bool{B}$-valued model $\M$ is \emph{extensional} if $\Qp{\sigma=\tau}^\M_{\bool{B}}=1_{\bool{B}}$ entails $\sigma=\tau$ for all $\sigma, \tau\in M$.
\end{definition}
If no confusion can arise, we avoid the supscript $\M$ and the subscript $\bool{B}$. Moreover, we write equivalently $\sigma\in M$ or $\sigma\in\M$, identifying a boolean valued model $\M$ with its underlying set $M$.\\
Monro does not require in \cite{MONRO86} that $\Qp{\sigma=\sigma}=1_\bool{B}$
for every $\sigma\in M$; he calls \emph{global elements} the ones satisfying this condition.
\begin{definition}\label{def:boolvalmorph}
Fix a language $\LL$. Let $\M_1$ be a $\bool{B}_1$-valued model for $\LL$ and $\M_2$ be a $\bool{B}_2$-valued model for $\LL$, where $\bool{B}_1$ and $\bool{B}_2$ are boolean algebras. A \emph{morphism of boolean valued models for $\LL$} is a pair $(\Phi, i)$ where:
\begin{itemize}
\item $i: \bool{B}_1\to \bool{B}_2$ is an adjoint morphism of boolean algebras;

\item $\Phi:M_1\to M_2$ is an \emph{$i$-morphism}, that is: for every $n$-ary relational symbol $R$ and every constant symbol $c$ in the language and for every
$\tau_1,\dots, \tau_n\in M_1$,
\[\Phi(c^{\M_1})=c^{\M_2},\]
\[ i(\llbracket R(\tau_1, \dots, \tau_n)\rrbracket^{\M_1}_{\bool{B}_1})\leq
\llbracket R(\Phi(\tau_1), \dots, \Phi(\tau_n))\rrbracket^{\M_2}_{\bool{B}_2},\]
\[ i(\llbracket \tau_1=\tau_2\rrbracket^{\M_1}_{\bool{B}_1})\leq \llbracket\Phi(\tau_1)=\Phi(\tau_2)\rrbracket^{\M_2}_{\bool{B}_2}.\]
If in both these equations equality holds, we call $\Phi$ an \emph{$i$-embedding}.\end{itemize}
If $i$ is an isomorphism, $\Phi$ is an $i$-embedding, and for all $\tau\in M_2$ there is $\sigma\in M_1$ such that
$\Qp{\Phi(\sigma)=\tau}_{\bool{B}_2}=1_{\bool{B}_2}$, $\ap{\Phi,i}$ is an \emph{isomorphism of boolean valued models}.
\end{definition}
Clearly, if $\bool{B}_1=\bool{B}_2=2$ and both $\M_1$ and $\M_2$ are extensional, an $\Id_2$-morphism and an $\Id_2$-embedding are exactly a morphism and an embedding between two
Tarski models, respectively.\\
It is worth noting that Monro considers as a morphism an equivalence class of such functions, where $\Phi$ and $\Psi$ are equivalent whenever $i(\llbracket\tau=\tau\rrbracket)\leq\llbracket\Phi(\tau)=\Psi(\tau)\rrbracket$\footnote{Remember that Monro does not require $\llbracket\tau=\tau\rrbracket=1_{\bool{B}}$.} for every $\tau$ in the first model (see \cite[Definition 5.2]{MONRO86}).\\
We now define the boolean valued semantics. By now, we have not required any condition on the boolean algebra $\bool{B}$.
 For the definition of the semantic, however, we need to compute some infinite suprema. For this reason, we will always assume in the sequel that formulae are assigned truth values in the boolean completion $\RO(\bool{B}^+)$ of $\bool{B}$ and we identify
 $\bool{B}^+$ with a dense subset of the partial order $\RO(\bool{B}^+)^+$. In most cases $\bool{B}$ is rightaway a complete booolean algebra in which case
$\RO(\bool{B}^+)=\bool{B}$ and this complication vanishes.
\begin{definition}
Let $\M=\ap{M, =^\M, R^\M_i: i\in I}$ be a $\bool{B}$-valued model for the relational language $\LL=\bp{R_i: i\in I}$. We evaluate the formulae without free variables in the extended language $\LL_\M:=\LL\cup\bp{c_\sigma: \sigma\in M}$
by maps with values in the boolean completion $\RO(\bool{B}^+)$ of $\bool{B}$ as follows:
\begin{itemize}
\item $\Qp{c_\sigma=c_\tau}^{\M}_{\RO(\bool{B}^+)}:=\Qp{\sigma=\tau}^\M_\bool{B}$ and
$\Qp{R(c_{\sigma_1}, \dots, c_{\sigma_n})}^{\M}_{\RO(\bool{B}^+)}:=\Qp{R(\sigma_1, \dots, \sigma_n)}^\M_\bool{B}$;
\item $\Qp{\nphi\wedge\psi}^{\M}_{\RO(\bool{B}^+)}:=
\Qp{\nphi}^\M_{\RO(\bool{B}^+)}\wedge\Qp{\psi}^\M_{\RO(\bool{B}^+)}$;
\item $\Qp{\neg\nphi}^\M_{\RO(\bool{B}^+)}:=\neg\Qp{\nphi}^\M_{\RO(\bool{B}^+)}$;
\item $\Qp{\exists x\nphi(x, c_{\sigma_1}, \dots, c_{\sigma_n})}^\M_{\RO(\bool{B}^+)}:=
\bigvee_{\tau\in M}\Qp{\nphi(c_\tau, c_{\sigma_1}, \dots c_{\sigma_n})}^\M_{\RO(\bool{B}^+)}.$
\end{itemize}
If $\nphi(x_1, \dots, x_n)$ is any $\LL$-formula with free variables $x_1, \dots, x_n$ and $\nu$ is an assignment, we define $\Qp{\nu(\nphi(x_1, \dots, x_n))}^\M_{\RO(\bool{B}^+)}:=
\Qp{\nphi(c_{\nu(x_1)}, \dots, c_{\nu(x_n)})}^\M_{\RO(\bool{B}^+)}$.
\end{definition}
We will often write $\nphi(\sigma_1, \dots, \sigma_n)$ rather than $\nphi(c_{\sigma_1}, \dots, c_{\sigma_n})$
and $\Qp{\nphi(\tau_1, \dots, \tau_n)}$ rather than $\Qp{\nphi(\tau_1, \dots, \tau_n)}^\M_{\RO(\bool{B}^+)}$ if
no confusion can arise.

By induction on the complexity of $\LL$-formulae, it is possible to show the following:
\begin{fact}
For every $\sigma_1, \dots, \sigma_n, \tau_1, \dots, \tau_n\in M$ and for every $\LL$-formula $\nphi(x_1, \dots, x_n)$ with displayed free variables, the following holds:
\begin{equation}
\Bigl(\bigwedge_{i=1}^n\Qp{\sigma_i=\tau_i}\Bigr)\wedge\Qp{\nphi(\sigma_1, \dots, \sigma_n)}
\leq\Qp{\nphi(\tau_1, \dots, \tau_n)}.
\end{equation}
\end{fact}

\begin{remark}
Given a signature $\mathcal{L}$,
and a morphism $(\Theta,i)$ of a $\bool{B}$-valued model $\M$ for $\mathcal{L}$ into a $\bool{C}$-valued model $\N$ for $\mathcal{L}$
it is a natural request that of imposing $i$ to be an adjoint homomorphism: otherwise the truth value of $i(\Qp{\exists x\psi(x)}^\M_{\bool{B}})$ might not be $\bigvee_{\bool{C}}\bp{i(\Qp{\psi(\sigma)}^\M_\bool{B}): \sigma\in\M}$, in which case the morphism would not preserve the expected meaning of quantifiers.
\end{remark}

The following is the correct generalization to boolean valued semantics of the notion of elementary embedding between Tarski structures:
\begin{definition}\label{def:elembvm}
Given a signature $\mathcal{L}$,
a morphism $(\Theta,i)$ of a $\bool{B}$-valued model $\M$ for $\mathcal{L}$ into a $\bool{C}$-valued model $\N$
for $\mathcal{L}$ is elementary if for all $a_1,\dots,a_n\in\M$ and $\mathcal{L}$-formulae $\phi(x_1,\dots,x_n)$
\[
i(\Qp{\phi(a_1,\dots,a_n}^\M_\bool{B})=\Qp{\phi(\Theta(a_1),\dots,\Theta(a_n)}^\N_\bool{C}.
\]
\end{definition}

\begin{definition}
A sentence $\nphi$ in the language $\LL$ is \emph{valid} in a $\bool{B}$-valued model $\M$ for $\LL$ if $\Qp{\nphi}=1_{\RO(\bool{B})}$.

A theory $T$ is \emph{valid} in $\M$ (equivalently, $\M$ is a $\bool{B}$-model for $T$) if every axiom of $T$ is valid in $\M$.
\end{definition}
\begin{theorem}[Soundness and Completeness]
Let $\LL$ be a relational language. An $\LL$-formula $\nphi$ is provable syntactically by an $\LL$-theory $T$ if and only if, for every boolean algebra $\bool{B}$ and for every $\bool{B}$-valued model $\M$ for $T$, $\Qp{\nu(\nphi)}^\M_{\RO(\bool{B})}=1_{\RO(\bool{B})}$ for every assignment $\nu$ taking values in $\M$.
\end{theorem}
\begin{proof}
See for instance \cite[Theorems 4.1.5 and 4.1.8]{viale-notesonforcing}.
\end{proof}

\subsection{\L o\'s Theorem for boolean valued models and fullness}

\begin{definition}\label{def:quotboolmod}
Let $\bool{B}$ be a boolean algebra and let $\M=\ap{M, =^\M, R^\M_i: i\in I}$ be a $\bool{B}$-valued model for the relational language $\LL=\bp{R_i: i\in I}$. Let $F$ be a filter of $\bool{B}$. The \emph{quotient} $\M/_F$ is the $\bool{B}/_F$-valued model for $\LL$ defined as follows:
\begin{itemize}
\item the domain is $M/_F:=\bp{[\sigma]_F: \sigma\in M}$, where $[\sigma]_F:=\bp{\tau\in M: \Qp{\tau=\sigma}\in F}$;
\item if $R\in\LL$ is an $n$-ary relational symbol and $[\sigma_1]_F, \dots, [\sigma_n]_F\in M/_{F}$,
\[
\Qp{R([\sigma_1]_F, \dots, [\sigma_n]_F)}^{\M/_F}_{\bool{B}/_F}:=\Bigl[\Qp{R(\sigma_1, \dots, \sigma_n)}^\M_{\bool{B}}\Bigr]_F\in\bool{B}/_F.
\]
\end{itemize}
\end{definition}
It is easy to check that this quotient is well-defined. In particular, if $G$ is an ultrafilter, the quotient
$\M/_G$ is a two-valued Tarski structure for $\LL$.
On the other hand if $\bool{B}$ is a boolean algebra and $F$ is a filter on $\bool{B}$, it can happen that
$\bool{B}$ is complete while $\bool{B}/_F$ is not, and conversely. In particular it is not clear how the semantics of
formulae with quantifiers is affected by the quotient operation. We now address this problem.
\begin{definition}\label{def:fullness-wellbehaved}
Given a first order signature $\LL$,
a $\bool{B}$-valued model $\M$ for $\LL$ is
\begin{itemize}
\item
\emph{well behaved} if:
for all $\LL$-formulae $\phi(x_1,\dots,x_n)$
and $\tau_1,\dots,\tau_n\in\M$ $\Qp{\phi(\tau_1,\dots,\tau_n)}^\M_{\RO(\bool{B})}$ is in $\bool{B}$;
\item
\emph{full} if for all ultrafilters $G$ on $\bool{B}$, all $\LL$-formulae $\phi(x_1,\dots,x_n)$
and all $\tau_1,\dots,\tau_n\in\M$
\[
\M/_G\models\phi([\tau_1]_G,\dots,[\tau_n]_G)\qquad\text{ if and only if }\qquad\Qp{\phi(\tau_1,\dots,\tau_n)}^\M\in G.
\]
\end{itemize}
\end{definition}
Notice that if $\bool{B}$ is complete $\bool{B}\cong\RO(\bool{B}^+)$ hence any $\bool{B}$-valued model
$\M$ is automatically well-behaved. But being well-behaved does not require $\bool{B}$ to be complete, just to be able to compute all the suprema and infima required by the satisfaction clauses for $\exists,\forall$.
On the other hand for atomic $\LL_\M$-formulae the condition expressing fullness is automatic by definition.
The unique delicate case occurs for $\LL_\M$-formulae  in
which the principal connective is a quantifier, for example of the form $\exists x\phi(x)$, in which case
the fullness conditions for the formula amounts to ask that $\sup_{\sigma\in\M}\Qp{\phi(\sigma)}^\M$ is actually a finite supremum, as we will see. We will investigate this property in many details in the last two sections of this paper. For the moment letting a
$\LL_\M$-formula $\phi(x_1,\dots,x_n)$ be \emph{$F$-full} for a filter $F$ if and only if
\[
\Qp{\phi([\tau_1]_G,\dots,[\tau_n]_G)}^{\M/_F}=1_{\bool{B}/_F}\qquad\Longleftrightarrow\qquad\Qp{\phi(\tau_1,\dots,\tau_n)}^\M\in F,
\]
we automatically have that the family of $F$-full $\LL_\M$-formulae includes the atomic formulae and is closed under conjuctions for any filter $F$, and under boolean
combinations for any ultrafilter $F$.
Another key observation is that if $F$ is a filter and
\[
\bigvee_{i=1}^m\Qp{\phi(\sigma_i)}^{\M}=\Qp{\exists x\,\phi(x)}^{\M}=\bigvee_{\tau\in \M}\Qp{\phi(\tau)}^{\M},
\]
then
\[
\bigvee_{i=1}^m\Qp{\phi([\sigma_i]_F)}^{\M/_F}=\Qp{\exists x\,\phi(x)}^{\M/_F},
\]
since
\[
\bigvee_{i=1}^m[\Qp{\phi(\sigma_i)}^\M]_F=\Bigl[\bigvee_{i=1}^m\Qp{\phi(\sigma_i)}^{\M}\Bigr]_F\geq_F [\Qp{\phi(\tau)}^{\M}]_F
\]
holds for all $\tau\in\M$.
The notion of full $\bool{B}$-valued model displays its full power in the following result:
\begin{theorem}[\L o\'s Theorem for boolean valued models] \label{thm:charLosThm}
Let $\M$ be a well behaved $\bool{B}$-valued model for the signature $\LL$.
The following are equivalent:
\begin{itemize}
\item $\M$ is full.
\item for all $\LL_\M$-formulae $\phi(x_0,\dots,x_n)$
and all $\tau_1,\dots,\tau_n\in\M$ there exist $\sigma_1, \dots, \sigma_m\in\M$ such that
\[
\bigvee_{\tau\in \M}\Qp{\phi(\tau,\tau_1,\dots,\tau_n)}=\bigvee_{i=1}^m\Qp{\phi(\sigma_i,\tau_1,\dots,\tau_n)}.
\]
\end{itemize}
\end{theorem}
\begin{proof}
We sketch the proof for the case of existential formulae.\\
First, assume $\M$ to be full:
\[
\M/_G\models\exists x\psi(x, [\tau_1]_G,\dots,[\tau_n]_G)\quad\Leftrightarrow\quad\Qp{\exists x\psi(x, \tau_1,\dots,\tau_n)}^\M\in G.
\]
Thus for every $G$ such that $\Qp{\exists x\psi(x, \tau_1,\dots,\tau_n)}^\M\in G$ there exists $\sigma_G\in\M$ such that $\M/_G\models\psi([\sigma_G]_G, [\tau_1]_G,\dots,[\tau_n]_G).$ \\
Again using the hypothesis, we obtain that for every $G\in N_{\Qp{\exists x\psi(x, \tau_1,\dots,\tau_n)}}$ there exists $\sigma_G\in\M$ such that $G\in N_{\Qp{\psi(\sigma_G, \tau_1,\dots,\tau_n)}}$, that is:
\[
N_{\Qp{\exists x\psi(x, \tau_1,\dots,\tau_n)}}\subseteq\bigcup_{\sigma\in\M}N_{\Qp{\psi(\sigma, \tau_1,\dots,\tau_n)}}.
\]
By compactness, $N_{\Qp{\exists x\psi(x, \tau_1,\dots,\tau_n)}}=\bigcup_{i=1}^mN_{\Qp{\psi(\sigma_i, \tau_1, \dots, \tau_n)}}$, which is our thesis.\\
Conversely, assume that for every formula $\phi$, $\tau_1, \dots, \tau_n\in\M$ there exist $\sigma_1, \dots, \sigma_m\in\M$ such that
\[
\bigvee_{\tau\in \M}\Qp{\phi(\tau,\tau_1,\dots,\tau_n)}=\bigvee_{i=1}^m\Qp{\phi(\sigma_i,\tau_1,\dots,\tau_n)}.
\]
By induction on the complexity of the formulae we prove that $\M$ is full. Let us consider only the non-trivial case: $\psi(x_1,\dots, x_n)=\exists x\phi(x, x_1, \dots, x_n)$. Then
\begin{align*}
\M/G\models\exists x\phi(x, [\tau_1]_G, \dots, [\tau_n]_G)\Leftrightarrow&\M/G\models\phi([\sigma]_G, [\tau_1]_G, \dots, [\tau_n]_G)\\
&\textit{ for some }\sigma\in\M\\
\Leftrightarrow&\Qp{\phi(\sigma,\tau_1, \dots, \tau_n)}\in G\textit{ for some }\sigma\in\M\\
\Rightarrow&\Qp{\exists x\phi(x, \tau_1, \dots, \tau_n)}\in G.
\end{align*}
Conversely, if $\Qp{\exists x\phi(x, \tau_1, \dots, \tau_n)}\in G$, since $\Qp{\exists x\phi(x, \tau_1, \dots, \tau_n)}=\bigvee_{i=1}^m\Qp{\phi(\sigma_i, \tau_1, \dots, \tau_n)}$, there exists $i\in\bp{1, \dots, m}$ such that $\Qp{\phi(\sigma_i, \tau_1, \dots, \tau_n)}\in G$. By inductive hypothesis
\[
\M/G\models\phi([\sigma_i]_G, [\tau_1]_G, \dots, [\tau_n]_G)
\]
and so $\M/G\models\exists x\phi(x, [\tau_1]_G, \dots, [\tau_n]_G)$.
\end{proof}
One recovers the standard \L o\'s Theorem for ultraproducts observing that any product $\prod_{i\in I}N_i$ of $\LL$-structures
is a full $\pow{I}$-valued model for $\LL$, and that the semantic of the quotient structure $\bigl(\prod_{i\in I}N_i\bigr)/G$ for $G$ ultrafilter on $\pow{I}$
is exactly ruled by the conditions set up in the above theorem.\\

To appreciate the fact that fullness is not automatic (and as we will see is a slight weakening of the notion of sheaf)
we will give now a counterexample to fullness.
\begin{example}
\label{ex:ana}
Let $\R$ be equipped with the Lebesgue measure $\mu_L$. Let $\mathscr{M}_L(\R)$ be the family of Lebesgue measurable subsets of $\R$, which is obviously a boolean algebra. Let $\Null$ be the ideal of null subsets and define the \emph{measure algebra} as $\malg:=\mathscr{M}_L(\R)/\Null$. It can be checked that $\malg$ is a complete boolean algebra, whose countable suprema are easily computed by taking the equivalence class of the union of representatives. For further details we refer to \cite[Section 3.3.1]{viale-notesonforcing}.\\
We make the set $\analytic{\R}$ of analytic functions $\R\to\R$ the domain of a $\malg$-valued model
for the language $\LL=\bp{<, C}$ as follows. For $f, g\in\analytic{\R}$, let
\[
\begin{aligned}
\Qp{f=g}:=&\bigl[\bp{r\in\R: f(r)=g(r)}\bigr]_\Null\\
\Qp{f<g}:=&\bigl[\bp{r\in\R: f(r)<g(r)}\bigr]_\Null\\
\Qp{C(f)}:=&\bigvee\bp{[U]_\Null\in\malg: f\restriction U\textit{ is constant}}.
\end{aligned}
\]
A key property of analytic functions in one variable is that they are constant on a non discrete set
if and only if they are everywhere constant.\\
The reader can check that
$(\analytic{\R}, \Qp{-=-}, \Qp{-<-}, \Qp{C(-)})$ is a $\malg$-valued model. \\
Fix $f\in\analytic{\R}$ and consider the sentence $\phi:=\exists y(f<y\wedge C(y))$. Let $c_r$ denote the map $\R\to\R$
which is constantly $r$ and let $a_n:=\sup(f\restriction {(n-1, n)})+1$. Then
\[
\begin{aligned}
\Qp{\exists y(f<y\wedge C(y))}&=\bigvee_{g\in\analytic{\R}}\Qp{f<g\wedge C(g)}\geq\bigvee_{r\in\R}\Qp{f<c_r}\wedge\Qp{C(c_r)}\\
&=\bigvee_{r\in\R}\Qp{f<c_r}\geq\bigvee_{n\in\Z}\Qp{f<c_{a_n}}\\
&\geq\bigvee_{n\in\Z}[(n-1, n)]_\Null=[\R]_\Null.
\end{aligned}
\]
In particular, taking $f=\Id_\R$, we have
\[
\Qp{\exists y(\Id_\R<y\wedge C(y)}^{\analytic{\R}}=1_\malg.
\]
However, let $G$ be an ultrafilter in $\malg$ which extends the family $\bp{[(n, +\infty)]_\Null: n\in\Z}$. Then, for every $r\in\R$,
\[
\Qp{\neg(\Id_\R<c_r)}=\qp{(r, +\infty)}_\Null\in G,
\]
therefore $\analytic{\R}/G\models\neg\exists y([\Id_\R]_G<y\wedge C(y))$.
\end{example}

\subsection{The mixing property and fullness}

The mixing property gives us a sufficient condition for having the fullness property which is, usually, easier to check; as we will see later the mixing property characterizes those boolean valued models which are stonean sheaves.
\begin{definition}\label{def:mixprop}
Let $\kappa$ be a cardinal,
$\LL$ be a first order language, $\bool{B}$ a
$\kappa$-complete boolean algebra,
$\M$ a $\bool{B}$-valued model for $\LL$.
\begin{itemize}
\item
$\M$ satisfies the \emph{$\kappa$-mixing property} if for every antichain $A\subset \bool{B}$
of size at most $\kappa$, and for every subset $\{\tau_a: a\in A\}\subseteq M$, there exists
$\tau\in M$ such that $a\leq\llbracket\tau=\tau_a\rrbracket$ for every $a\in A$.
\item
$\M$ satisfies the \emph{$<\kappa$-mixing property}
if it satisfies the $\lambda$-mixing property for all
cardinals $\lambda<\kappa$.
\item
$\M$ satisfies the \emph{mixing property}
if it satisfies the $|\bool{B}|$-mixing property.
\end{itemize}
In \cite{HODG} models with the $<\omega$-mixing property are called models which \emph{admit gluing}.
\end{definition}
Whether a $\bool{B}$-valued model $\M$ has the mixing property depends only on the interpretation of the equality symbol by $\Qp{-=-}^\M$.
\begin{proposition}
\label{ful:mod}
Let $\bool{B}$ be a complete boolean algebra and let $\M$ be a $\bool{B}$-valued model for $\LL$.  Assume that $\M$ satisfies the $\kappa$-mixing property for some $\kappa\geq\min\bp{|\bool{B}|, |M|}$. Then $\M$ is full.
\end{proposition}
\begin{proof}
Fix a formula $\phi(x, y_1,\dots, y_n)$ in $\LL$ and $\sigma_1, \dots, \sigma_n\in M$.
Fix moreover an enumeration $\ap{\tau_i: i\in I}$ of $M$.
Since $\Qp{\exists x\nphi(x, \sigma_1, \dots, \sigma_n)}=\bigvee_{i\in I}\Qp{\nphi(\tau_i, \sigma_1, \dots, \sigma_n)},$
we can refine the family $\bp{\Qp{(\nphi(\tau_i, \sigma_1, \dots, \sigma_n)}: i\in I}$ to an antichain $\bp{a_j: j\in J}$
as follows: let
\[
J:=I\setminus\bp{i\in I: \Qp{\nphi(\tau_i, \sigma_1, \dots, \sigma_n)}\setminus\bigvee_{j<i}\Qp{\nphi(\tau_j, \sigma_1, \dots, \sigma_n)}=0}.
\]
In particular, $J$ is well-ordered with the order induced by $I$ and we have that $\min J=\min I$.
Define \[a_{\min J}:=\Qp{\nphi(\tau_{\min I}, \sigma_1, \dots, \sigma_n)}\]and, for $J\ni i>\min J$,
\[a_i:= \Qp{\nphi(\tau_i, \sigma_1, \dots, \sigma_n)}\setminus\bigvee_{J\ni j<i}\Qp{\nphi(\tau_j, \sigma_1, \dots, \sigma_n)}.\]
If $A:=\bp{a_j: j\in J}$, it is clear that $\bigvee A=\Qp{\exists x\nphi(x, \sigma_1, \dots, \sigma_n)}$ and
$|A|\leq|M|, |\bool{B}|\leq\kappa$. Since $\M$ satisfies the $\kappa$-mixing property, there exists $\tau\in M$ such that
\[a_i\leq\Qp{\tau=\tau_i}\] for every $i\in J$. In particular, since $a_i\leq\Qp{\nphi(\tau_i, \sigma_1, \dots, \sigma_n)}$, we have that
\[
a_i=a_i\wedge\Qp{\tau=\tau_i}\leq\Qp{\nphi(\tau_i, \sigma_1, \dots, \sigma_n)}\wedge\Qp{\tau=\tau_i}\leq\Qp{\nphi(\tau, \sigma_1, \dots, \sigma_n)}
\]
for every $i\in J$.
Hence $\Qp{\nphi(\tau, \sigma_1, \dots, \sigma_n)}\geq\bigvee_{i\in J}a_i=\bigvee A=\Qp{\exists x\nphi(x, \sigma_1, \dots, \sigma_n)}$ and so $\M$ is full.
\end{proof}
\begin{remark}
The result just proven actually shows that the mixing property implies a strong version of fullness, that is: for every formula $\phi(x_0, x_1, \dots, x_n)$ and for every $\tau_1, \dots, \tau_n\in\M$ there exists an element $\tau_0$ such that
\[
\bigvee_{\sigma_\in\M}\Qp{\phi(\sigma, \tau_1, \dots, \tau_n)}=\Qp{\phi(\tau_0, \tau_1, \dots, \tau_n)}.
\]
This is actually the definition of fullness one can find for instance in \cite{JECH}. It is easy to see that this property is true in every full model $\M$ satisfying the $<\omega$-mixing property.
\end{remark}
We will now exhibit an example of full boolean valued model which does not satisfy the mixing property. To do so, we let $V$
denote the class of all sets and assume $(V,\in)$ is a model of \ZFC. The reader not familiar with forcing as developed in
Kunen's \cite{KUNEN}, Jech's \cite{JECH}, or Bell's \cite{BELL} textbooks can safely skip this example without compromising the comprehension of the remainder of this article.
\begin{example}\label{ex:fullnotimplmix}
\label{non:mix}
We stick in this example to the standard terminology on forcing as can be found in Jech's \cite{JECH} or Bell's \cite{BELL} books.
Let $M\in V$ be a countable transitive model of (a sufficiently large fragment of) $\ZFC$ and let $\bool{B}\in M$ be an
infinite boolean algebra which $M$ models to be complete. Consider the $\bool{B}$-valued model
$(M^{\bool{B}},\Qp{-=-}^{M^{\bool{B}}},\Qp{-\in-}^{M^{\bool{B}}})$, which is a definable class in $(M,\in)$
(and a countable set in $V$). Now, it can be proved (see \cite[Mixing Lemma 1.25]{BELL}) that
\[
M\models (M^{\bool{B}},\Qp{-=-}^{M^{\bool{B}}})\textit{ has the mixing property}
\]
In particular,
\[
M\models (M^{\bool{B}},\Qp{-=-}^{M^{\bool{B}}},\Qp{-\in-}^{M^{\bool{B}}})\textit{ is full}.
\]
The notion of being full is absolute between transitive models of set theory,\footnote{If $M$ proves that $M^{\bool{B}}$ is full, $M$ proves that a certain element $\bigvee_{i=1}^m\Qp{\nphi(a_i)}^{M^{\bool{B}}}\in\bool{B}$ is equal to the element
$\Qp{\exists x\nphi(x)}^{M^{\bool{B}}}\in\bool{B}$, and this equality between elements of $\bool{B}$ must be true also in $V$.}
therefore
\[
(V,\in)\models(M^{\bool{B}},\Qp{-=-}^{M^{\bool{B}}},\Qp{-\in-}^{M^{\bool{B}}})\textit{ is full}.
\]
For a complete discussion of the fullness of $M^\bool{B}$ we refer to \cite[Sections 5.1.2 and 5.2]{viale-notesonforcing} and in particular to \cite[Lemma 5.2.1]{viale-notesonforcing}.\\
We will now show that, in $V$, $(M^{\bool{B}},\Qp{-=-}^{M^{\bool{B}}},\Qp{-\in-}^{M^{\bool{B}}})$ does not satisfy the
mixing property. Being $M$ countable, for sure there exists a maximal antichain $A$ of $\bool{B}\subseteq M$ such that
$A\in V\setminus M$. We claim that this antichain witnesses the fact that the $\bool{B}$-valued model
$(M^{\bool{B}},\Qp{-=-}^{M^{\bool{B}}},\Qp{-\in-}^{M^{\bool{B}}})$
does not have the mixing property.\\
By contradiction, let $\tau\in M^{\bool{B}}$ be such that
\[
\Qp{\tau=\check{a}}\geq a
\]
for every $a\in A$. Then $A$ is definable in $M$ by the formula $\nphi(x,\bool{B})$ where
\[
\nphi(x,\bool{B}):=(x\textit{ is an antichain of $\bool{B}$})\wedge(\bigvee_{\bool{B}}x=1_{\bool{B}})\wedge\forall y(y\in x\lrao(y\in\bool{B}\wedge\Qp{\tau=\check{y}}\geq y)).
\]
The antichain $A$ is the unique solution of the formula $\nphi$. Indeed, assume $C$ to be another solution of $\nphi$.
Let $c\in C\setminus A$. Then, by the maximality of $A$, there exists $a\in A$ such that $a\wedge c>0$.
Being $A$ and $C$ solutions of $\nphi$, we have
\[
0_\bool{B}<a\wedge c\leq\Qp{\tau=\check{a}}\wedge\Qp{\tau=\check{c}}\leq\Qp{\check{a}=\check{c}}=0_{\bool{B}},
\]
where $\Qp{\check{a}=\check{c}}=0_\bool{B}$ since $M\models(a\neq c)$ and so
\[
M\models\Qp{\neg(\check{a}=\check{c})}^{M^{\bool{B}}}_{\bool{B}}=1_\bool{B}.
\]
Being $A$ a subset of $\bool{B}$ definable in $M$, by the Axiom of Comprehension (which holds in the $\ZFC$-model $M$) we have that $A\in M$, against our assumption.
\end{example}

\section{The presheaf structure of a boolean valued model}
\label{sec:pres}

In this section we will describe the correspondence between boolean valued models and presheaves. Moreover, we will use this correspondence to describe the mixing property in terms of sections of \'etal\'e spaces.\\
Our results can be obtained as easy corollaries of Monro's works \cite{MONRO86}. However we decide to give explicitly the proofs to make our presentation self-contained and accessible to readers  (as we are) familiar with set theory, and not so much at ease with categories to read without problems Monro's work.

Fix a boolean algebra $\bool{B}$ and a $\bool{B}$-valued model $\M$.

For every $b\in B$, let $F_b$ be the filter generated by $b$, and consider

the $\bool{B}/_{F_b}$-valued model $\M/_{F_b}$.
Note that if $N_b\subseteq N_c$ (i.e. $b\leq c$), then $F_b\supseteq F_c;$ therefore the
natural map
\begin{align*}
i^\M_{bc}:& \M/_{F_c}\to \M/_{F_b}\\
& [\tau]_{F_c}\mapsto [\tau]_{F_b}
\end{align*}
defines a morphism from the $\bool{B}/_{F_c}$ valued model $\M/_{F_c}$ onto the $\bool{B}/_{F_b}$-valued
model $\M/_{F_b}$.\\
It is convenient from now on to look at a boolean algebra at times as an algebraic structure and at other times as the clopens of its Stone space. We will freely do so in the sequel.

\begin{definition}
$\Mod^{\textit{bool}}_\LL$ denotes the category of boolean valued models for the language $\LL$ and morphisms between them.
\end{definition}

\begin{definition}\label{def:preshbvm}
Given a Boolean algebra $\bool{B}$
and a $\bool{B}$-valued model $\M$, its associated presheaf $\F_\M:(\bool{B}^+)^{\textrm{op}}\to\Mod^{\textit{Bool}}_\LL$ is defined by:
\begin{itemize}
\item $\F_\M(b)=\M/_{F_b}$ for any $b\in\bool{B}^+$;
\item $\F_\M(b\leq c)$ for $b\leq c\in\bool{B}^+$ is the map
\begin{align*}
i^\M_{bc}:& \M/_{F_c}\to \M/_{F_b}.\\
& [\tau]_{F_c}\mapsto [\tau]_{F_b}
\end{align*}
\end{itemize}
\end{definition}
Let us stress the fact that until now we have built nothing else than a \emph{separated} presheaf.\\
Now we want to describe the stalk of $\F_\M$ at $G\in\St(\bool{B})$.
Translating the definition of stalk in our setting, we have that
\[
(\F_\M)_G:=\Bigl(\bigsqcup_{b\in G}\M/_{F_b}\Bigr)/_{\sim_G},
\]
 where \[
 [\sigma]_{F_b}\sim_G[\tau]_{F_c}\quad\textit{if and only if}\quad[\sigma]_{F_{b\wedge c}}=
 [\tau]_{F_{b\wedge c}}.
 \]
Now observe that for each $\sigma\in\M$ and $b\in G$
\begin{align*}
[\sigma]_{F_b}&=
\bp{\tau\in\M: \Qp{\sigma=\tau}\geq b}.
\end{align*}
In particular the map $\Theta_G:\sigma\mapsto [[\sigma]_{F_{1_{\bool{B}}}}]_{\sim_G}$
defines a surjection of $\M$ onto
$(\F_\M)_G$ with
\[
\begin{aligned}
\Theta_G(\sigma)=\Theta_G(\tau)&\Longleftrightarrow[[\sigma]_{F_{1_{\bool{B}}}}]_{\sim_G}=[[\tau]_{F_{1_{\bool{B}}}}]_{\sim_G}\\
&\Longleftrightarrow[\sigma]_{F_b}=[\tau]_{F_b}\textit{ for some }b\in G\\
&\Longleftrightarrow\Qp{\sigma=\tau}\geq b\textit{ for some }b\in G\\
&\Longleftrightarrow\Qp{\sigma=\tau}\in G.
\end{aligned}
\]
This shows that $\Theta_G(\sigma)=\Theta_G(\tau)$ if and only if $\M/_G\models [\sigma]_G=[\tau]_G$.\\
In particular we can identify (as sets) the stalk $(\F_\M)_G$ and the Tarski quotient $\M/_G$ of $\M$ at $G$.\\
Let us now analyze the \'etal\'e space $E_\M$ canonically associated to the presheaf $\F_\M$\footnote{$E_\M$ is exactly the space $\Lambda^0_{\F_\M}$ (or even $\Lambda^1_{\F_\M}$ if $\bool{B}$ is complete), considering $\F_\M$ as a presheaf on $\St(\bool{B})$, via the functor $\mathrm{ext}$ defined in Fact \ref{fac:extrestrpreshROX}.}.
It is the disjoint union of the fibers $(\F_\M)_G$ for $G\in\St(\bool{B})$, which by our observation above amounts to a disjoint union of the Tarski structures $\M/_G$ as $G$ varies in $\St(\bool{B})$, that is:
\[
E_\M=\bp{[\sigma]_G: \sigma\in M, G\in\St(\bool{B})}.
\]
Equivalently, we can say that
\[
E_\M=\bp{\ap{\sigma, G}: \sigma\in M\textit{ and }G\in\St(\bool{B})}/_{R_\M},
\]
where $R_\M$ is the equivalence relation such that $\ap{\sigma, G}R_\M\ap{\tau, H}$ if and only if
$G=H$ and $\Qp{\sigma=\tau}\in G$.\\
Moreover, the projection map $p:E_\M\to\St(\bool{B})$ sends each $\ap{\sigma, G}=[\sigma]_G$ to $G$.\\
A base for the topology of $E_\M$ is the family
\[
\mathcal{B}:=\bp{\dot{\sigma}[N_b]=\bp{[\ap{\sigma, G}]_{R_\M}: b\in G}: \sigma\in M, b\in\bool{B}}.
\]
This topology is readily Hausdorff. Indeed, if $\ap{\sigma, G}\neq\ap{\tau, H}$, either $G\neq H$ or $G=H$ and
$\neg\Qp{\sigma=\tau}\in G$. In the first case, being $\St(\bool{B})$ Hausdorff, there exists an open
neighborhood $N_b$ of $G$ and an open neighborhood $N_c$ of $H$ which are disjoint. Then the basic open
sets $\dot{\sigma}[N_b]$ and $\dot{\tau}[N_c]$ separate $\ap{\sigma, G}$ from $\ap{\tau, H}$.
Otherwise, if $G=H$, we have that $[\sigma]_G\neq[\tau]_G$.
Let $b:=\Qp{\sigma\neq\tau}=\neg\Qp{\sigma=\tau}\in G$.
Then, $\dot{\sigma}[N_b]$ and $\dot{\tau}[N_b]$ are disjoint open neighborhoods of
$\ap{\sigma, G}$ and $\ap{\tau, G}$, respectively.
Moreover, for any open $U\subseteq\St(\bool{B})$ and $\sigma\in M$, the local section
$\dot{\sigma}\restriction {U}$ is open and injective and so it is an homeomorphism on its image.\\

From now on, to simplify notation, we will forget the language and see $\F_\M$ as a presheaf of sets. Our arguments below can be immediately extended to cover the case in which we also consider the boolean valued structure on the objects and arrows of $\F_\M$.
 We have already defined the functor
\[
L:\modx\to\SPresh^{\textrm{bool}}(\dSet),
\]
where:
\begin{enumerate}
\item $\modx$ is the category of boolean valued models for the empty language $\bp{=}$ and morphisms between them, with the condition that, if $(\Phi, i):(\M, \bool{B})\to(\N, \bool{C})$ is a morphism, $i$ is an adjoint homomorphism, while the map $\Phi$ need not be injective;
\item\label{item:defmorphpreshboolvalmod}
 $\SPresh^{\textrm{bool}}(\dSet)$ is the category whose objects are \emph{separated} $\dSet$-valued presheaves on some boolean algebra and, if $\F_0:(\bool{B}^+)^{\textrm{op}}\to\dSet, \F_1:(\bool{C}^+)^{\textrm{op}}\to\dSet$ are objects, a morphism between them is a pair $(\gamma, i)$ where $i:\bool{B}\to\bool{C}$ is an adjoint homomorphism of boolean algebras and $\gamma=\{\gamma_b:\F_0(b)\to\F_1(i(b))\}_{b\in\bool{B}^+}$ is a family of maps such that, if $b_1\leq b_2$, the following diagram commutes:
\begin{equation}\label{eqn:diagmorphboolpresh}
\begin{CD}
\F_0(b_2) @>\gamma_{b_2}>>  \F_1(i(b_2))\\
@V{\F_0(b_1\leq b_2)}VV              @VV{\F_1(i(b_1)\leq i(b_2))}V\\
\F(b_1)@>>\gamma_{b_1}>  \F_1(i(b_1))\\
\end{CD};
\end{equation}
\item if $\M$ is an object in $\modx$, its image under $L$ is the presheaf $L(\M):=\F_\M$;
\item if $(\Phi, i):\M\to \N$ is a morphism in $\modx$ with $i:\bool{B}\to\bool{C}$, then its image under $L$ is the morphism $(L(\Phi), i)$ with
$L(\Phi)=\bp{L(\Phi)_b}_{b\in\bool{B}^+}$ such that
\[
\begin{aligned}
L(\Phi)_b:=\Phi/_{F_b}:&\M/_{F_b}\to\N/_{F_{i(b)}}\\
&[\tau]_{F_b}\mapsto[\Phi(\tau)]_{F_{i(b)}},
\end{aligned}
\]
where $F_b$ is the filter in $\bool{B}$ generated by $b$ and $F_{i(b)}$ is the filter in $\bool{C}$ generated by $i(b)$.
\end{enumerate}

It is left to the reader to check that $L(\Phi)$ is well-defined and that the required composition and commutativity laws
hold, making $L$ indeed a functor.

Conversely:
\begin{definition}
\[
R:\Presh^{\textrm{bool}}(\dSet)\to\modx
\]
is the functor defined by:
\begin{itemize}
\item if $\F$ is any\footnote{Note that $R$ can be defined on arbitrary $\bool{B}^+$-presheaves, however the pairs $\ap{L,R}$ will define an adjunction only when $R$ is restricted to the class of \emph{separated}
presheaves and boolean valued models for complete boolean algebras (see Theorem \ref{thm:adjbvmodpresh}).} presheaf $R(\F):=\M_\F$ is the $\RO(\St(\bool{B}))$-valued model whose domain is $\F(1_\bool{B})$ and such that, for $f, g\in \F(1_\bool{B})$,
\[
\Qp{f=g}^{\M_\F}:=\Reg{\bigcup\bp{N_b\in\CLOP(\St(\bool{B})): \F(b\leq 1_\bool{B})(f)=\F(b\leq1_\bool{B})(g)}};
\]
\item if $(\alpha, i):\F\to\G$ is a natural transformation of presheaves with $\F:(\bool{B}^+)^{\textrm{op}}\to\dSet, \G:(\bool{C}^+)^{\textrm{op}}\to\dSet$, and $i:\bool{B}\to\bool{C}$, $R(\alpha, i)=(R(\alpha), i)$, with $R(\alpha):=\alpha_{1_\bool{B}}$, where $\alpha_{1_\bool{B}}:\F(1_\bool{B})\to\G(1_\bool{B})$ is the map defined by
$\alpha$ at $1_\bool{B}$.
\end{itemize}
\end{definition}
We can identify the morphisms
of  $\SPresh^{\textrm{bool}}(\dSet)$ with those of Definition \ref{def:presh*morph} in view
of the following:

\begin{proposition}
Let
$\F_i:\mathcal{O}(X_i)^{\mathrm{op}}\to\dSet$ be separated presheaves for $i=0,1$ with each $X_i$ a Stone space.

$\iota=(i_\iota,\Theta_\iota)$ is a morphism from $\F_0\to \F_1$ according to Definition \ref{def:presh*morph}
if and only if $(i_\iota\restriction\CLOP(X_0), \bar{\Theta}_\iota)$ is a morphism of $\F_0\restriction\RO(X_0)$ to $\F_1\restriction\RO(X_1)$ for
$\SPresh^{\textrm{bool}}(\dSet)$ according to item \ref{item:defmorphpreshboolvalmod} above;
where for $U\in\CLOP(X_0)$ and $h\in \F_0(U)$ (noting that $(i_\iota)_*(\F_0)(i_\iota(U))=\F_0(U)$, by definition of $(i_\iota)_*$)
\begin{align*}
(\bar{\Theta}_\iota)_U:& \F_0(U))\to \F_1(i_\iota(U))\\
& h\mapsto (\Theta_\iota)_{i_\iota(U)}(h)
\end{align*}
Furthermore this identification of morphisms is surjective and depends only on the behaviour
of $\Theta_\iota$ on $(i_\iota)_*(\F_0)$.

\end{proposition}
Hence, up to a change of terminology, the type of morphism we are considering here on
$\SPresh^{\textrm{bool}}(\dSet)$ are exactly those considered in Section \ref{subsec:stsheafadj}.
\begin{proof}
We sketch one direction, which amounts to check the comutativity of Diagram \ref{eqn:diagmorphboolpresh}
for $\bar{\Theta}_\iota$.

Given $U\subseteq V$ both in $\CLOP(X_0)$ and $h\in \F_0(V)$ we have that
\begin{align*}
(\bar{\Theta}_\iota)_U(h\restriction U)&=(\Theta_\iota)_{i_\iota(U)}(h\restriction U)=\\
&=(\Theta_\iota)_{i_\iota(U)}(h\restriction i_{\iota}(U))=\\
&=(\Theta_\iota)_{i_\iota(V)}(h)\restriction i_{\iota}(U)=\\
&=(\bar{\Theta}_\iota)_V(h)\restriction U,
\end{align*}
where we use again that $(i_\iota)_*(\F_0)(i_\iota(U))=\F_0(U)$ (as sets), and the restriction map between
$(i_\iota)_*(\F_0)(i_\iota(V))=\F_0(V)$ and $(i_\iota)_*(\F_0)(i_\iota(U))=\F_0(U)$ for $U\subseteq V$ clopen of $X_0$ is the same as the one between $\F_0(V)$ and $\F_0(U)$.

The other checks are left to the reader.

\end{proof}

To discuss the relation between the functors $L$ and $R$, it is convenient to consider the subcategories $\Presh^{\textrm{cba}}(\dSet)\subseteq\Presh^{\textrm{bool}}(\dSet)$, $\SPresh^{\textrm{cba}}(\dSet)\subseteq\SPresh^{\textrm{bool}}(\dSet)$, and $\modxx\subseteq\modx$ where the boolean algebras are required to be complete.
The following result corresponds, in our setting, to \cite[Theorem 5.4]{MONRO86}.
\begin{theorem}\label{thm:adjbvmodpresh}
The pair $\ap{L, R}$ is an adjuction between the categories
$\SPresh^{\textrm{cba}}(\dSet)$ and $\modxx$ with $L$ being the
left adjoint.

\end{theorem}
\begin{proof}
We have only to find the unit $\eta$ and the counit $\varepsilon$ of the adjunction and then to verify the identities
\begin{equation}
\label{un:coun}
\Id_R=R\varepsilon\circ\eta R\textit{ and }\Id_L=\varepsilon L\circ L\eta.
\end{equation}
To define the unit $\eta: \Id_{\modxx}\to R\circ L$, we simply take, for $\M\in\modxx$ a $\bool{B}$-valued model, $(\eta_\M,\Id_{\bool{B}})$, where
\begin{align*}
\eta_\M:&\M\to\M/_{F_1}.\\
&\tau\mapsto[\tau]_{F_1}
\end{align*}
The fact that $\eta$ is a natural transformation is left to the reader. Notice that $\eta_\M$ for $\M$ extensional is the identity morphism.\\
We need now to define the counit $\varepsilon$. Here we need to use crucially the assumption that we restrict
$R$ to the family of \emph{separated} presheaves. Towards this aim
if $b\leq c$, we have
that the following diagram is commutative with horizontal lines being bijections:
\begin{equation}\label{comdgm:counitLXRX}
\begin{CD}
(\F(c\leq1))[\F(1)] @>\tau\restriction c\mapsto[\tau]_{c}>>  R(\F)/_{F_c}\\
@V{\tau\restriction c\mapsto\tau\restriction b}VV              @VV{[\tau]_{F_c}\mapsto [\tau]_{F_b}}V\\
(\F(b\leq 1))[\F(1)]@>>\tau\restriction b\mapsto[\tau]_{b}>  R(\F)/_{F_b}\\
\end{CD}
\end{equation}
where, by our convention, $\F(b\leq 1)(\tau)$ is equally denoted as $\tau\restriction b$.\\
The commutativity is automatic by definition of the various maps occurring in the diagram.
To see why the horizontal lines are bijections, observe that
$[\tau]_{F_b}=[\sigma]_{F_b}$ for $\tau,\sigma\in\F(1)$ and $b\in\bool{B}$
if and only if $b\leq\Qp{\tau=\sigma}^{R(\F)}$ if and only if\footnote{The left to right implication of this equivalence uses that
$\F$ is separated, otherwise we can only assert that the set of $d\leq b$ such that $\F(d\leq1)(\sigma)= \F(d\leq 1)(\tau)$
is a dense cover of $b$, but $b$ may not belong to this dense cover if $\F$ is not separated.}
\[
\F(b\leq1)(\sigma)= \F(b\leq 1)(\tau).
\]
In particular we conclude that:
\begin{equation}\label{eqn:LXCIRCRX0}
((L\circ R)(\F))(b):=R(\F)/_{F_b}\cong \F(b\leq 1)[\F(1)]\subseteq\F(b),
\end{equation}
and
\begin{align}\label{eqn:LXCIRCRX1}
((L\circ R)(\F))(b\leq c)&=
\bp{[\tau]_{c}\mapsto [\tau]_{b}: \tau \in \F(1)}\cong\\ \nonumber
&\cong \F(b\leq c)\restriction (\F(b\leq 1)[\F(1)])\\ \nonumber
&\subseteq \F(b\leq c).
\end{align}
Now we let $\varepsilon$ be the natural transformation which in each component $\F:(\bool{B}^+)^{\textrm{op}}\to\dSet$ is the morphism $(\epsilon(\F), \Id_{\bool{B}})$, where $\epsilon(\F)$ is defined in the following way:
\begin{itemize}
\item for any $b\in\bool{B}^+$
\begin{align*}
\varepsilon(\F)(b):\F(1)/_{F_b}&\to\F(b\leq 1)[\F(1)]\\
 [\tau]_b&\mapsto(\tau\restriction b);
\end{align*}
\item for any $b\leq c\in\bool{B}^+$,
$\varepsilon(\F)(b\leq c)$ transfers via the horizontal lines of diagram (\ref{comdgm:counitLXRX})
the mapping $\bp{[\tau]_c\mapsto[\tau]_b:\tau\in \F(1)}$ from $\F(1)/_{F_c}$ to $\F(1)/_{F_b}$ to the mapping $\F(b\leq c)\restriction \bp{\tau\restriction c: \tau\in \F(1)}$ (where the latter set is exactly $\F(c\leq 1)[\F(1)]$).
\end{itemize}
The morphism $\varepsilon_\F$ is a well defined natural transformation of $L\circ R$ with
$\Id_{\SPresh^{\textrm{cba}}(\dSet)}$ due to the commutativity of diagram (\ref{comdgm:counitLXRX}).\\
Equations \eqref{un:coun} characterizing the unit and counit properties of $\eta,\varepsilon$ with respect to $L,R$
are satisfied due to the following observations:
\begin{itemize}
\item
The unit $\eta$ restricted to the image of the functor $R$ is the identity:
the target of $R_\bool{B}$ is the class of $\bool{B}$-valued extensional models.
\item
The counit $\varepsilon$ restricted to the image of the functor
$L$ is an isomorphism with the identity functor on the image of $L$\footnote{Here considering complete boolean algebras is essential, otherwise $\F:(\bool{B}^+)^{\textrm{op}}\to\dSet$ and $(L\circ R)(\F):(\RO(\bool{B})^+)^{\textrm{op}}\to\dSet$ would be defined on differerent boolean algebras, and thus they could not be isomorphic.}: for any $\bool{B}$-valued model $\M$,
$L(\M)$ is a presheaf $\F_\M:(\bool{B}^+)^{\textrm{op}}\to\dSet$ in which $\F_\M(b)=\M/_{F_b}$ is the surjective image of $\F_\M(1)=\M/_{F_1}$ via
$\F_\M(b\leq 1):[\tau]_{F_1}\mapsto[\tau]_{F_b}$; in particular for $\F_\M$ the last inclusions of (\ref{eqn:LXCIRCRX0}) and (\ref{eqn:LXCIRCRX1}) are reinforced to equalities, and we can conclude that $\varepsilon$ is an isomorphism appealing to the fact that the horizontal lines of the commutative diagram (\ref{comdgm:counitLXRX}) are bijections\footnote{Here we use essentially that $R$ is applied to
a separated presheaf. Otherwise we could have different sections $f,g$ in
$\F(1)$ such that $\Qp{f=g}_{R_\bool{B}(\F)}=1$; in which case $[f]_{F_1}=[g]_{F_1}$, hence the horizontal lines in (\ref{comdgm:counitLXRX}) are not anymore bijections. It is not clear then how to select canonically the representatives in the equivalence classes of $[-]_{F_1}$ so to maintain the requested naturality properties for the counit given by (\ref{eqn:LXCIRCRX0}) and (\ref{eqn:LXCIRCRX1}).}.
\end{itemize}
\end{proof}
\begin{corollary}\label{cor:adjbvmodpresh}
\label{eq:ex}
Let
\begin{itemize}
\item $\exPresh^{\textrm{cba}}(\dSet)$ be the full subcategory of $\SPresh^{\textrm{cba}}(\dSet)$
given by the separated presheaves $\F$ such that $\F(b)=\F(b\leq 1)[\F(1)]$ for all $b\in\bool{B}^+$,
\item
$\exmodxx$ be the full subcategory of $\modxx$ generated by extensional models.
\end{itemize}
The adjunction
\[
\ap{L:\modxx\to\SPresh^{\textrm{cba}}( \dSet), R:\SPresh^{\textrm{cba}}(\dSet)\to\modxx}
\]
specializes to an equivalence of categories between
$\exmodxx$ and $\exPresh^{\textrm{cba}}(\dSet)$.
\end{corollary}

Note that every $\bool{B}$-valued model $\M$ is boolean isomorphic to the extensional
model $\M/_{F_1}$.
Hence the corollary amounts to say that $\bool{B}$-valued models  identify the class of separated
$\bool{B}^+$-presheaves in
which the local sections are always restrictions of global sections.\\
Note also that any $\bool{B}^+$-sheaf $\F$ is such that every local section is the restriction
of a global section: for each $b\in\bool{B}^+$ let $f_b$ be some section in $\F(b)$;
given any local section $g$ in $\F(c)$ the family $\bp{g,f_{\neg c}}$ is matching,
and a collation of this family is a global section whose restriction to $c$ is $g$.\\
The following characterization of boolean valued models with the mixing property is \cite[Proposition 5.6]{MONRO86}.
\begin{proposition}
\label{chr:mix}
Let $\bool{B}$ be a complete boolean algebra and
$\M$ be a $\bool{B}$-valued model.
Then $\M$ has the mixing property if and only if the separated presheaf
$\F_\M$
of Definition \ref{def:preshbvm} is a sheaf (according to the sup Grothendieck topology).
\end{proposition}
\begin{proof}
Assume that $\M$ has the mixing property.
Let $b\in\bool{B}$ and let $\bp{b_i: i\in I}$ be
such that $\bigvee_{i\in I}b_i=b$. From now on, fix a well-order $\leq$ on $I$.
We can assume that, for every $i\in I$,
 \[
 a_i=b_i\wedge\neg\bigvee_{j<i}b_j\neq0,
 \] otherwise we may omit $b_i$.
 Notice that $A:=\bp{a_i: i\in I}$ is an antichain and, for every $i\in I$, $a_i\leq b_i$.
 Let $f_i\in \F(b_i)=\M/_{F_{b_i}}$ for every $i\in I$ and suppose that, if
$i\neq j$, then
\begin{equation}
\label{cond:comp}
f_i\restriction b_i\wedge b_j=f_j\restriction b_i\wedge b_j.
\end{equation}
 Assume that that $f_i=[\sigma_i]_{F_{b_i}}$ for some $\sigma_i\in\M$.
 Thus, condition \eqref{cond:comp} can be rewritten as
\[
\Qp{\sigma_i=\sigma_j}\geq b_i\wedge b_j\quad\textit{for every $i, j\in I$}.
\]
 Let $g_i:=f_i\restriction a_i.$
In particular, $g_i=[\sigma_i]_{F_{a_i}}$.
Since $\M$ satisfies the mixing property, there exists $\tau\in\M$ such that $\Qp{\tau=\sigma_i}\geq a_i$ for every $i\in I$.
By induction on the well order of $I$, $\Qp{\tau=\sigma_i}\geq b_i$. Indeed, $\Qp{\tau=\sigma_{\min I}}\geq a_{\min I}=b_{\min I}$  and, if we assume that $\Qp{\tau=\sigma_j}\geq b_j$ for all $j<i$,
\[
\begin{aligned}
\Qp{\tau=\sigma_i}&\geq a_i\vee\bigvee_{j<i}\bigl(\Qp{\sigma_i=\sigma_j}\wedge\Qp{\tau=\sigma_j}\bigr)
\geq a_i\vee\bigvee_{j<i}((b_i\wedge b_j)\wedge b_j)\\
&= \bigl(b_i\wedge\neg\bigvee_{j<i}b_j\bigr)\vee\bigvee_{j<i}(b_i\wedge b_j)=b_i.
\end{aligned}
\]
Hence $[\tau]_{F_b}$ is the desired collation of $\bp{f_i:i\in I}$.\\
Conversely, suppose $\F_\M$ to be a sheaf.
 Let $A$ be an antichain in $\bool{B}$ and let $\sigma_a\in\M$ for every $a\in A$.
 In particular, if $a\neq a'$, since $A$ is an antichain, $a\wedge a'=0$, and so it is clear that
$\F_\M(a\wedge a'\leq a)([\sigma_a]_{F_a})=\F_\M(a\wedge a'\leq a')([\sigma_{a'}]_{F_{a'}}).$\\
Let $b:=\bigvee A.$
Being $\F_\M$ a sheaf, there exists $\tau\in\M$ such that $\F_\M(a\leq b)([\tau]_{F_b})=[\sigma_a]_{F_a}$ for all $a\in A.$ This is equivalent to say that $\Qp{\tau=\sigma_a}\geq a$ for every $a\in A$.
Hence $\M$ satisfies the mixing property.
\end{proof}
\begin{corollary}\label{char:Gamma0=Gamma1}
Let $\bool{B}$ be a complete boolean algebra.
A $\bool{B}$-valued model $\M$ has the mixing property if and only if every global section of the \'etal\'e space
$E_\M=\Lambda^0_{\F_\M}=\Lambda^1_{\F_\M}$ is a section induced by an element of $\M$.\\
In particular if $\M$ has the mixing property
 the presheaf $\F_\M=\Gamma^{1/2}_{p^1_{\F_\M}}$ is the $\bool{B}^+$-sheaf (for the sup Grothendieck topology) isomorphic to the restriction to $\bool{B}^+$ of the topological sheaf $\Gamma^0_{p^0_{\F_\M}}$ (which is actually in this specific case isomorphic to the stonean sheaf
 $\Gamma^1_{p^1_{\F_\M}}$).
\end{corollary}
\begin{example}
Let us recall the $\malg$-valued model $\analytic{\R}$ of analytic functions introduced in Example \ref{ex:ana}.
Let us show explicitly that its associated \'etal\'e space $\Lambda^0_{L(\analytic{\R})}$ does have global sections which are not induced by elements of
$\analytic{\R}$.
Consider $a:=[(-\infty, 0)]_\Null\in\malg$. It is clear that $\neg a=[(0, +\infty)]_\Null$.
Define $s:\St(\malg)\to \Lambda^0_{L(\analytic{\R})}$ by
\[
s(G):=
\begin{cases}
[c_0]_G \quad\text{if $a\in G$,}\\
[c_1]_G\quad\text{if $\neg a\in G$}
\end{cases}
\]
(recall that $c_r:\R\to\R$ is the constant function $\R\ni x\mapsto r$). It is immediate to see that $s$ is a global section,
and it is continuous from $\St(\malg)$ to $\Lambda^0_{L(\analytic{\R})}$.
However, there is no analytic function in $\analytic{\R}$ inducing $s$: the candidates to induce $s$ have to be constantly
$0$ on an open interval $I_0\subseteq(-\infty, 0)$ and have to be constantly $1$ on an open interval
$I_1\subseteq(0, +\infty)$, hence they are not analytic functions.
\end{example}

\begin{example}\label{ex:fullnotimplmix2}
In Example \ref{non:mix} we are just saying that the continuous section $h:\bigcup_{a\in A}N_a\to \Lambda^0_{L(M^{\bool{B}})}$ such that \[h(G)=[\check{a}]_G\textit{ if and only if }a\in G\]
is not induced by any element of $M^{\bool{B}}$.
\end{example}
Furthermore, by Corollary \ref{eq:ex} we can conclude the following.
\begin{corollary}
The equivalence of categories between $\exmodxx$ and $\exPresh^{\textrm{cba}}(\dSet)$ induces an equivalence of categories between the full subcategory of $\exmodxx$ generated by the models satisfying the mixing property and the full subcategory $\exSh^{\textrm{cba}}(\dSet)$ of $\exPresh^{\textrm{cba}}(\dSet)$ generated by the sheaves $\F:(\bool{B}^+)^{\textrm{op}}\to\dSet$ (according to the sup Grothendieck topology) such that $\F(b)=\F(b\leq 1_\bool{B})[\F(1_\bool{B})]$ for every $b\in\bool{B}$.
\end{corollary}
\begin{example}\label{exm:sheafLR}
Let us now outline why the $\bool{MALG}$-names for real numbers correspond to the stonean sheafification of the presheaf
$\F$ assigning to each $[A]\in\bool{MALG}$ the space $L^\infty(A)$, for $A$ a measurable subset of $\mathbb{R}$.\\
It is not hard to check that the boolean valued model
\[
\M=\bp{\tau\in V^\bool{MALG}: \Qp{\tau\in\mathbb{R}}_\bool{MALG}=1_\bool{MALG}}
\]
is a boolean valued model with the mixing property (for details see \cite{VIAVAC15}).
Then $L(\M)$ is a sheaf.
Let also $\beta_0(\mathbb{R})=\mathbb{R}\cup\{\infty\}$ be the one point compactification of $\mathbb{R}$ and let $X=\St(\malg)$.
By the results of \cite{MR779056,MR759416,VIAVAC15}
\[
L(\M)(1_\malg)\cong C^+(X)=\bp{f:X\to\beta_0(\mathbb{R}): \, f\text{continuous and }f^{-1}[\bp{\infty}]\text{ nowhere dense}}.
\]
It is also possible to see that the Gelfand transform of $L^\infty(\mathbb{R})$ extends to a natural isomorphism
\[
C^+(X)\cong L^{\infty+}(\mathbb{R})=\bp{f:\mathbb{R}\to\beta_0(\mathbb{R}):\,f\text{ is measurable and } \nu(f^{-1}[\bp{\infty}])=0},
\]
where $\nu$ is Lebesgue measure (for details see  \cite{VIAVAC15}, natural here means that it is a $\bool{MALG}$-isomorphism according to Definition \ref{def:boolvalmorph} when for $f,g\in C^+(X)$ we set $\Qp{f=g}=\Reg{\bp{G\in X: f(G)=g(G)}}$ and for
$f^*,g^*\in L^{\infty+}(\mathbb{R})$ $\Qp{f^*=g^*}=[\bp{a\in \mathbb{R}: f^*(a)=g^*(a)}]_{\mathsf{Null}}$).\\
In particular this isomorphism shows that for all $A\subseteq\mathbb{R}$ measurable
\[
L(\M)([A]_{\mathsf{Null}})\cong\bp{f:A\to\beta_0(\mathbb{R}): \, f\text{continuous and }f^{-1}[\bp{\infty}]\text{ nowhere dense}}
\]
and that $C^+(X)$ is naturally identified with $\Gamma^{1}_{p^1_{\F_\M}}$.
\end{example}

We also get the following standard canonical mixification of a boolean valued model:
\begin{corollary}\label{cor:mixbvm}
Let $\M$ be a $\bool{B}$-valued model. Then
$R\circ\Gamma^1\circ\Lambda^1\circ L(\M)$ is a boolean valued model with the mixing property and such that the map $\Phi_\M:\sigma\mapsto (\Gamma^1\circ\Lambda^1)_{\St(\RO(\bool{B}))}([\sigma]_{F_{1_\bool{B}}})$ coupled with the natural inclusion map $b\mapsto N_b$ of $\bool{B}$ into
$\RO(\St(\bool{B}))$ is an elementary embedding\footnote{Recall Def. \ref{def:elembvm}.} of $\M$ into a $\RO(\bool{B})$-valued model with the mixing property.
\end{corollary}
\begin{proof}
It is clear that $R\circ\Gamma^1\circ\Lambda^1\circ L(\M)$ is a $\RO(\bool{B})$-valued model with the mixing property. We leave to the reader to check the remaining items. In essence the key point is that given a  family $\bp{\sigma_i:i\in I}$ such that
\[
b=\Qp{\exists x \phi(x)}^{\M}_{\bool{B}}=\bigvee_{i\in I}\Qp{\phi(\sigma_i)}^{\M}_{\bool{B}},
\]
one can find $J\subseteq I$ and a maximal antichain $A=\bp{a_j:j\in J}$ below $b$ such that:
\begin{itemize}
\item
$\Qp{\phi(\sigma_j)}^{\M}_{\bool{B}}\geq a_j$ for all $j\in J$;
\item
$\bp{[\sigma_j]_{F_{a_j}}:j\in J}$ is a collating family in
$L(\M)$;
\item the collation $\sigma^*\restriction N_b$ of this family is obtained from a global section $\sigma^*$ of
$\Gamma^1\circ\Lambda^1\circ L(\M)$.
\end{itemize}
One has then to check that
\[
N_b=\Qp{\exists x\phi(x)}^{R\circ\Gamma^1\circ\Lambda^1\circ L(\M)}_{\RO(\St(\bool{B}))}=\Qp{\phi(\sigma^*)}^{R\circ\Gamma^1\circ\Lambda^1\circ L(\M)}_{\RO(\St(\bool{B}))}=\bigvee_{\RO(\St(\bool{B}))}
\bp{N_{\Qp{\phi(\sigma_j)}^{\M}_{\bool{B}}}:j\in J}
\]
 holds in $R\circ\Gamma^1\circ\Lambda^1\circ L(\M)$.
\end{proof}
In particular $R\circ\Gamma^1\circ\Lambda^1\circ L$ provides a canonical ``mixification'' of a boolean valued model; canonical in the sense that it preserves the boolean valued semantics.

\section{A characterization of the fullness property using \'etal\'e spaces}
\label{sec:charfulletalespace}

We are now interested to characterize the fullness property for boolean valued models as in Definition \ref{def:fullness-wellbehaved} in terms of sheaf theory, along the lines of what we did in Section \ref{sec:pres}. In doing so, we will use heavily the equivalence condition for the fullness property investigated in Theorem \ref{thm:charLosThm}.\\
The sheaf theoretic notion notion we found appropriate to characterize fullness is that of \'etal\'e space.
First of all we notice that a well behaved $\bool{B}$-valued model $\M$ for the language $\LL$ is full if and only if,
for every $\LL_\M$-formula $\nphi(x_1, \dots, x_n)$ with $n$ free variables $x_1, \dots, x_n$, there exists a finite number $m$ of $n$-tuples
$\ap{\sigma_1^{(1)}, \dots, \sigma_n^{(1)}}, \dots, \ap{\sigma_1^{(m)}, \dots, \sigma_n^{(m)}}\in M^n$ such that
\[
\Qp{\exists x_1, \dots, \exists x_n\nphi(x_1, \dots, x_n)}=\bigvee_{i=1}^m\Qp{\nphi(\sigma_1^{(i)}, \dots, \sigma_n^{(i)})}.
\]
Now fix an $\LL_\M$-formula $\nphi(x_1, \dots, x_n)$ with $n$-free variables and let:
\begin{itemize}
\item
 $b_\nphi:=\Qp{\exists x_1, \dots, x_n\nphi(x_1, \dots, x_n)}$.
 \item
 $D_\nphi:=\bp{N_c: \,\exists \sigma_1,\dots,\sigma_n\, 0_\bool{B}<c\leq
 \Qp{\nphi(\sigma_1, \dots, \sigma_n)}}$
 \item
 $A_\nphi:=\bigcup D_\nphi=\bigcup\bp{N_c:0_\bool{B}<c\leq\Qp{\nphi(\sigma_1, \dots, \sigma_n)},\, \sigma_1,\dots,\sigma_n\in\mathcal{M}}$.
 \end{itemize}
  We define an \'etal\'e space $E^\nphi_\M$ over

$N_{b_\nphi}$

by:
\[
E^\nphi_\M:=\bp{\ap{\sigma_1, \dots, \sigma_n, G}: \sigma_1, \dots, \sigma_n\in M, \Qp{\nphi(\sigma_1, \dots, \sigma_n)}\in G\in \St(\bool{B})}/_R,
\]
where $R$ is the equivalence relation such that $\ap{\sigma_1, \dots, \sigma_n, G}\mathrel{R}\ap{\tau_1, \dots, \tau_n, H}$ if and only if $G=H$ and $\Qp{\sigma_i=\tau_i}\in G$ for every $i=1, \dots, n$.\\
We can equivalently say that
\[
E^\nphi_\M=\bp{\ap{[\sigma_1]_G, \dots, [\sigma_n]_G}: \sigma_1, \dots, \sigma_n\in M, \Qp{\nphi(\sigma_1, \dots, \sigma_n)}\in G\in\St(\bool{B})}.
\]
This set is mapped into $N_{b_\nphi}$ by the function $p_\nphi:\ap{\sigma_1, \dots, \sigma_n, G}\mapsto G$ ( notice that, if there are some $\sigma_1, \dots, \sigma_n\in M$ such that $\Qp{\nphi(\sigma_1, \dots, \sigma_n)}\in G$, then $b_\nphi\in G$).\\
The important observation is that, in general, $p_\nphi$ is not surjective on $N_{b_\nphi}$;
its image is just the dense open subset $A_\nphi$
of\footnote{If $b_\nphi$ is a supremum but not a maximum of $\bp{\Qp{\nphi(\sigma_1, \dots, \sigma_n)}: \,\sigma_1,\dots,\sigma_n\in\M}$, there is
$G\in N_{b_\nphi}\setminus A_\nphi;$
this $G$ is not in the target of $p_\nphi$.}
 $N_{b_\nphi}$. \\
The topology of $E^\nphi_\M$ is the one obtained as a subspace of $(E_\M)^n$: a base for the topology of $E^\nphi_\M$ is
\[
\mathcal{B}^\nphi:=\bp{\bp{\ap{\sigma_1, \dots, \sigma_n, G}: \Qp{\nphi(\sigma_1, \dots, \sigma_n)}\in G\in N_c}: \sigma_1, \dots, \sigma_n\in M, N_c\subseteq N_{b_\nphi}}.
\]
It is easy to check that $E^\nphi_\M$ equipped with this topology renders continuous the map $p_\nphi$.
Moreover, $p_\nphi:E^\nphi_\M\to N_{b_\nphi}$ is the bundle (e.g induced by $\Lambda^0$ and according to \cite[II]{MacLMoer}) associated to the \'etal\'e space of the presheaf $\G^\nphi_\M:D_{\nphi}^{\textrm{op}}\to\dSet$ defined as follows:
\[
\G^\nphi_\M(c):=\bp{\ap{[\sigma_1]_{F_c}, \dots, [\sigma_n]_{F_c}}: \sigma_1, \dots, \sigma_n\in M\textit{ and }c\leq\Qp{\nphi(\sigma_1, \dots, \sigma_n)}}.
\]
Notice by the way that

 each $\ap{[\sigma_1]_{F_c}, \dots, [\sigma_n]_{F_c}}\in\G^\nphi_\M(N_c)$ defines a continuous open section
\[
(\dot{\sigma}_1\times\dots\times\dot{\sigma}_n): G\mapsto\ap{[\sigma_1]_G, \dots, [\sigma_n]_G, G}
\]
 of $p_{\nphi}$ over $N_c$.\\
 We can now give a local characterization (i.e. formula by formula) of the fullness property.
\begin{definition}
Given a $\bool{B}$-valued model $\mathcal{M}$ for $\mathcal{L}$, an
$\mathcal{L}$-formula $\nphi$ is \emph{$\M$-full} if $A_\nphi=N_{b_\nphi}$.
\end{definition}
\begin{theorem}
\label{chr:ful}
Let $\bool{B}$ be a boolean algebra and let $\M$ be a well behaved $\bool{B}$-valued model for the language $\LL$. The following are equivalent:
\begin{enumerate}
\item \label{chr:ful1} $\M$ is full;
\item\label{chr:ful2} $\nphi$ is $\M$-full

  for every $\LL_\M$-formula $\nphi$;
\item \label{chr:ful3} $A_\nphi$ is closed for every $\LL_\M$-formula $\nphi$;
\item\label{chr:ful4}  for every $\LL_\M$-formula $\nphi$ such that $E^\nphi_\M$ is non-empty, $E^\nphi_\M$ has at least one
global section.
\end{enumerate}
Moreover if $\M$ has the $<\omega$-mixing property the above are also equivalent to
\begin{enumerate}
\setcounter{enumi}{4}
\item\label{chr:ful5} for every $\LL_\M$-formula $\nphi(x_1, \dots, x_n)$ such that $E^\nphi_\M$ is non-empty, $E^\nphi_\M$ has at least one
global section of the form $\dot{\sigma}_1\times\dots\times\dot{\sigma}_n$.
\end{enumerate}
\end{theorem}
\begin{proof}
\ref{chr:ful1} implies \ref{chr:ful2}. Indeed, If $\M$ is full, for every $\LL_\M$-formula $\nphi(x_1, \dots, x_n)$ there exist $\sigma_1^{(1)}, \dots, \sigma_n^{(1)}, \dots, \sigma_1^{(m)}, \dots, \sigma_n^{(m)}\in M$ such that
\[
\bigvee_{i=1}^n\Qp{\nphi(\sigma_1^{(i)}, \dots, \sigma_n^{(i)})}=
\Qp{\exists x_1, \dots, x_n\,\nphi(x_1, \dots, x_n)},\quad\text{ i. e. }\quad N_{b_\nphi}=\bigcup_{i=1}^m\,N_{\Qp{\nphi(\sigma_1^{(i)}, \dots, \sigma_n^{(i)})}}\subseteq A_\nphi.
\]
Conversely, assume \ref{chr:ful2}. This means that
\[
A_\nphi=\bigcup_{\sigma_1, \dots, \sigma_n\in\M}N_{\Qp{\nphi(\sigma_1, \dots, \sigma_n)}}=N_{b_\nphi}.
\]
Thus $\{N_{\Qp{\nphi(\sigma_1, \dots, \sigma_n)}}:\sigma_1, \dots, \sigma_n\in\M\}$ is an open cover of the compact space $N_{b_\nphi}$. By compactness, \ref{chr:ful1} holds.\\
The equivalence between \ref{chr:ful2} and \ref{chr:ful3} is immediate. Now we prove that \ref{chr:ful1} implies \ref{chr:ful4}. We have that
\[
N_{b_\nphi}=\bigcup_{i=1}^m\,N_{\Qp{\nphi(\sigma_1^{(i)}, \dots, \sigma_n^{(i)})}}.
\]
Consider
\[
C_1:=N_{\Qp{\nphi(\sigma_1^{(1)}, \dots, \sigma_n^{(1)})}},\qquad C_i:=N_{\Qp{\nphi(\sigma_1^{(i)}, \dots, \sigma_n^{(i)})}}\setminus\bigcup_{j=1}^{i-1}C_j, \quad i=2, \dots, m.
\]
The sets just defined are clopen, pairwise disjoint and they cover $N_{b_\nphi}$. Define $s:N_{b_\nphi}\to E^\nphi_\M$ by
\[s\restriction C_i:=\dot{\sigma}^{(i)}_1\times\dots\times\dot{\sigma}^{(i)}_n.
\]
Thus $s$ is continuous and it is a global section of $p_\nphi$.\\
Finally, assume $s$ is a section as in \ref{chr:ful4}, which means that $p_\nphi\circ s=\Id_{N_{b_\nphi}}$. In particular, $p_\nphi$ has to be surjective, and so \ref{chr:ful2} holds.\\

The missing details are left to the reader.
\end{proof}
The mixing property is strictly stronger than the fullness property. Here is a reformulation of Proposition \ref{ful:mod} in the language of bundles and sheaves:
\begin{corollary}
Assume $\bool{B}$ is a complete boolean algebra and $\M$ is a $\bool{B}$-valued model with the mixing property.
Then, for every $\LL_\M$-formula $\nphi(x_1, \dots, x_n)$, $\G^\nphi_\M$ is a sheaf.
In particular, if $\M$ has the mixing property, every local section of $E^\nphi_\M$ can be extended to a global one. Moreover, each global section is induced by an $n$-tuple of elements of $\M$.
\end{corollary}

\bibliographystyle{plain}
	\bibliography{Biblio.bib}

\end{document}