chap-disjoint.tex

\chapter{Disjoint product}

I remind that
$\coprod X = \bigcup_{i\in\dom X} (i,X_i)$
for every indexed family~$X$ of sets.

\begin{obvious}
$\coprod X\in\mathbf{Set}(\dom X,\im X)$.
\end{obvious}

\begin{defn}
I will call disjoint join of an indexed family~$\mathcal{X}$ of filters the following reloid: $\coprod\mathcal{X} = \bigsqcup_{i\in\dom f}(\{i\}\times^{\mathsf{RLD}}\mathcal{X}_i)$.
\end{defn}

\section{Some funcoids}

\begin{prop}
$\supfun{x\mapsto(i,x)}\mathcal{X}=\{i\}\times^{\mathsf{RLD}}\mathcal{X}$ for every filter~$\mathcal{X}$.
\end{prop}

\begin{proof}
$\supfun{x\mapsto(i,x)}\mathcal{X}=\bigsqcap\setcond{\rsupfun{x\mapsto(i,x)}X}{X\in\up\mathcal{X}}=\bigsqcap\setcond{\{i\}\times X}{X\in\up\mathcal{X}}=\{i\}\times^{\mathsf{RLD}}\mathcal{X}$.
\end{proof}

\begin{prop}
$\supfun{(x\mapsto(i,x))^{-1}}\mathcal{X}=\im(\mathcal{X}|_{\{i\}})$ for a filter~$\mathcal{X}$ on the set $\mathscr{U}\cup\{{\mathscr{U}}\}$ where $\mathscr{U}$~is
a Grothendieck universe.
\end{prop}

\begin{proof}
$\supfun{(x\mapsto(i,x))^{-1}}\mathcal{X}=\bigsqcap\setcond{\rsupfun{(x\mapsto(i,x))^{-1}}X}{X\in\up\mathcal{X}}=\bigsqcap\setcond{\setcond{x}{(i,x)\in X}}{X\in\up\mathcal{X}}=\bigsqcap\setcond{x\in\im X|_{\{i\}}}{X\in\up\mathcal{X}}=\im\bigsqcap\setcond{x\in X|_{\{i\}}}{X\in\up\mathcal{X}}=\im(\mathcal{X}|_{\{i\}})$.
\end{proof}

\section{Cartesian product of funcoids}

\subsection{Definition and basic properties}

\begin{defn}
\emph{Cartesian product} of an indexed family~$f$ of funcoids is
a funcoid \[ \prod^{(J)} f=\bigsqcup_{i\in\dom f}((x\mapsto(i,x))\circ f_i\circ(x\mapsto(i,x)^{-1}). \]
\end{defn}

\begin{prop}
$\supfun{\prod^{(J)}f}\mathcal{X}=\coprod_{i\in\dom f}\supfun{f_i\circ(x\mapsto(i,x)^{-1}}\mathcal{X}$.
\end{prop}

\begin{proof}
\begin{multline*}
\coprod_{i\in\dom f}\supfun{f_i\circ(x\mapsto(i,x)^{-1}}\mathcal{X}=\\
\bigsqcup_{i\in\dom f}(\{i\}\times^{\mathsf{RLD}}\supfun{f_i\circ(x\mapsto(i,x)^{-1}}\mathcal{X})=\\
\bigsqcup_{i\in\dom f}(\supfun{x\mapsto(i,x)}\supfun{f_i\circ(x\mapsto(i,x)^{-1}}\mathcal{X})=\\
\supfun{\prod^{(J)}f}\mathcal{X}.
\end{multline*}
\end{proof}

\subsection{Projections}

\begin{thm}
$f_i$~can be restored from the value of $\prod^{(J)}f=f_i$.
\end{thm}

\begin{proof}
$f_i = (x\mapsto(i,x)^{-1})\circ\prod^{(J)}f\circ(x\mapsto(i,x)^{-1})$
(taken into account that $x\mapsto(i,x)^{-1}$ is a principal funcoid).
\end{proof}

\section{Arrow product of funcoids}

\begin{defn}
\emph{Arrow product} of an indexed family~$f$ of funcoids is
a funcoid \[ \prod^{\rightarrow} f=\bigsqcup_{i\in\dom f}((x\mapsto(i,x))\circ f_i. \]
\end{defn}

\begin{prop}
$\supfun{\prod^{\rightarrow}f}\mathcal{X}=\coprod_{i\in\dom f}\supfun{f_i}\mathcal{X}$.
\end{prop}

\begin{proof}
\begin{multline*}
\coprod_{i\in\dom f}\supfun{f_i}\mathcal{X}=\\
\bigsqcup_{i\in\dom f}(\{i\}\times^{\mathsf{RLD}}\supfun{f_i}\mathcal{X})=\\
\bigsqcup_{i\in\dom f}(\supfun{x\mapsto(i,x)}\supfun{f_i}\mathcal{X})=\\
\supfun{\prod^{\rightarrow}f}\mathcal{X}.
\end{multline*}
\end{proof}

\subsection{Projections}

\begin{defn}
\emph{Arrow projections}
$\pi^{\rightarrow}_i = (x\mapsto(i,x))^{-1}$.
\end{defn}

\begin{thm}
$\pi^{\rightarrow}_i\circ\prod^{\rightarrow}f=f_i$
\end{thm}

\begin{proof}
Because $\pi^{\rightarrow}_i$ is a principal funcoid, we have
\[ \pi^{\rightarrow}_i\circ\prod^{\rightarrow}f=
\bigsqcup_{j\in\dom f}((x\mapsto(i,x))^{-1}\circ(x\mapsto(j,x))\circ f_j). \]
But $(x\mapsto(i,x))^{-1}\circ(x\mapsto(j,x))$ is the idenitity if $i=j$ or
empty otherwise. So
$\pi^{\rightarrow}_i\circ\prod^{\rightarrow}f=f_i$.
\end{proof}

\section{Cartesian product of reloids}

\subsection{Definition and basic properties}

\begin{defn}
\emph{Cartesian product} of an indexed family~$f$ of reloids is
a reloid \[ \prod^{(J)} f=\bigsqcup_{i\in\dom f}((x\mapsto(i,x))\circ f_i\circ(x\mapsto(i,x)^{-1}). \]
\end{defn}

\begin{conjecture}
$\prod^{(J)}(g\circ f)=\prod^{(J)}g\circ\prod^{(J)}f$.
\end{conjecture}

\subsection{Projections}

\begin{thm}
$f_i$~can be restored from the value of $\prod^{(J)}f=f_i$.
\end{thm}

\begin{proof}
$f_i = (x\mapsto(i,x)^{-1})\circ\prod^{(J)}f\circ(x\mapsto(i,x)^{-1})$.
\end{proof}

\section{Arrow product of reloids}

\begin{defn}
\emph{Arrow product} of an indexed family~$f$ of reloids is
a reloid \[ \prod^{\rightarrow} f=\bigsqcup_{i\in\dom f}((x\mapsto(i,x))\circ f_i. \]
\end{defn}

\subsection{Projections}

\begin{defn}
\emph{Arrow projections}
$\pi^{\rightarrow}_i = (x\mapsto(i,x))^{-1}$.
\end{defn}

\begin{prop}
$\pi^{\rightarrow}_i\circ\prod^{\rightarrow}f=f_i$.
\end{prop}

\begin{proof}
Because $x\mapsto(i,x)$ is a pricipal funcoid, we have
$\pi^{\rightarrow}_i\circ\prod^{\rightarrow}f=
\pi^{\rightarrow}_i\circ\bigsqcup_{i\in\dom f}((x\mapsto(i,x))\circ f_i=
\bigsqcup_{j\in\dom f}((x\mapsto(i,x))^{-1}\circ(x\mapsto(j,x))\circ f_i$.

But $(x\mapsto(i,x))^{-1}\circ(x\mapsto(j,x)$ is the identity if $i=j$ or empty otherwise. So $\pi^{\rightarrow}_i\circ\prod^{\rightarrow}f=f_i$.
\end{proof}