\documentclass{article}
\input{packages}
\input{def}

\homework{Topoi}

\begin{document}
\maketitle

\begin{definition}
Given an object $\ob{C}$ and subobjects $\mo{m}_1 : \ob{S}_1 \mono \ob{C}$ and $\mo{m}_2 : \ob{S}_2 \mono \ob{C}$, define $\mo{m}_1 \subseteq_\ob{C} \mo{m}_2$ to be $\exists \mo{f} : \ob{S}_1 \mto \ob{S}_2.\; \mo{m}_1 = \mo{f} \cocomp \mo{m}_2$.
\end{definition}

\begin{theorem}
$\subseteq_\ob{C}$ is a preorder on the subobjects of $\ob{C}$.
\end{theorem}

\begin{definition}
Given an object $\ob{C}$ of a topos, define $\mathbf{true}_\ob{C} : \ob{C} \mto \Omega$ to be $\langle \rangle_\ob{C} \cocomp \mathbf{true}$.
\end{definition}

\begin{exercise}
Given an object $\ob{C}$ of a topos and subobjects $\mo{m}_1 : \ob{S}_1 \mono \ob{C}$ and $\mo{m}_2 : \ob{S}_2 \mono \ob{C}$, prove that $\mo{m}_1 \subseteq_\ob{C} \mo{m}_2$ holds if and only if $\mo{m}_1 \cocomp \chi_{\mo{m}_2}$ equals $\mathbf{true}_{\ob{S}_1}$.
\end{exercise}

\begin{proof}
Suppose $\mo{m}_1 \subseteq_\ob{C} \mo{m}_2$ holds.
Let $\mo{f} : \ob{S}_1 \mto \ob{S}_2$ be a morphism proving this property.
Then $\mo{m}_1 \cocomp \chi_{\mo{m}_2}$ equals $\mo{f} \cocomp \mo{m}_2 \cocomp \chi_{\mo{m}_2}$, which equals $\mo{f} \cocomp \langle \rangle_{\ob{S}_1} \cocomp \mathbf{true}$, which equals $\langle \rangle_{\ob{S}_2} \cocomp \mathbf{true}$, which is the definition of $\mathbf{true}_{\ob{S}_1}$.

Suppose $\mo{m}_1 \cocomp \chi_{\mo{m}_2}$ equals $\mathbf{true}_{\ob{S}_1}$.
Then the fact that $\mo{m}_2$ is a pullback of $\chi_{\mo{m}_2}$ and $\mathbf{true}$ implies there exists a morphism $\mo{f} : \ob{S}_1 \mto \ob{S}_2$ such that $\mo{m}$ equals $\mo{f} \cocomp \mo{m}_2$.
Thus, $\mo{f}$ demonstrates that $\mo{m}_1 \subseteq_\ob{C} \mo{m}_2$ holds.
\end{proof}

\begin{definition}
Given an object $\ob{C}$ and a morphism $\mo{p} : \ob{C} \mto \Omega$, let $\mo{m}_p : \ob{S}_\mo{p} \mono \ob{C}$ be the (unique up to isomorphism) subobject produced by the pullback of $\mathbf{true}$ and $\mo{p}$.
\end{definition}

\begin{exercise}
Given an object $\ob{C}$ of a topos and subobjects $\mo{m}_1 : \ob{S}_1 \mono \ob{C}$ and $\mo{m}_2 : \ob{S}_2 \mono \ob{C}$, let $\mo{p} : \ob{C} \mto \Omega$ be defined as $\langle \chi_{\mo{m}_1}, \chi_{\mo{m}_2} \rangle \cocomp \wedge$.
Prove that $\mo{m}_\mo{p}$ is the meet of $\mo{m}_1$ and $\mo{m}_2$ with respect to the preorder $\ob{C}$.
Hint: take advantage of the following theorem.
\end{exercise}

\begin{theorem}
Given any commuting diagram of the following form (minus the dashed line), if the outer $[\ob{A}, \ob{B}, \ob{E}, \ob{F}]$ is a pullback square and the lower $[\ob{C}, \ob{D}, \ob{E}, \ob{F}]$ is a pullback square, then the upper $[\ob{A}, \ob{B}, \ob{C}, \ob{D}]$ using the uniquely induced dashed line is also a pullback square:
\begin{center}
\begin{tikzpicture}
\node(a) at (0,1) {$\ob{A}$};
\node(b) at (1,1) {$\ob{B}$};
\node(c) at (0,0) {$\ob{C}$};
\node(d) at (1,0) {$\ob{D}$};
\node(e) at (0,-1) {$\ob{E}$};
\node(f) at (1,-1) {$\ob{F}$};
\draw[->] (a) -- (b);
\draw[->] (c) -- (d);
\draw[->] (e) -- (f);
\draw[->,dashed] (a) -- (c);
\draw[->] (c) -- (e);
\draw[->] (b) -- (d);
\draw[->] (d) -- (f);
\draw[->] (a) to[bend right=30] (e);
\end{tikzpicture}
\end{center}
\end{theorem}

\begin{proof}
Apply the above theorem to the following diagram:
\begin{center}
\begin{tikzpicture}[xscale=3]
\node(a) at (0,1) {$\ob{S}_\mo{p}$};
\node(b) at (1,1) {$\ob{C}$};
\node(c) at (0,0) {$\top$};
\node(d) at (1,0) {$\Omega \with \Omega$};
\node(e) at (0,-1) {$\top$};
\node(f) at (1,-1) {$\Omega$};
\draw[->] (a) -- node[above]{$\mo{m}_\mo{p}$} (b);
\draw[->] (c) -- node[above]{$\langle \mathbf{true}, \mathbf{true} \rangle$} (d);
\draw[->] (e) -- node[below]{$\mathbf{true}$} (f);
\draw[->,dashed] (a) -- node[left]{$\langle \rangle$} (c);
\draw[->] (c) -- node[right]{$\id_\top$} (e);
\draw[->] (b) -- node[right]{$\langle \chi_{\mo{m}_1}, \chi_{\mo{m}_2} \rangle$} (d);
\draw[->] (d) -- node[right]{$\wedge$} (f);
\draw[->] (a) to[bend right=30] node[left]{$\langle \rangle$} (e);
\end{tikzpicture}
\end{center}

Because the upper square commutes, we have $\mo{m}_\mo{p} \cocomp \chi_{\mo{m}_1} = \mo{m}_\mo{p} \cocomp \langle \chi_{\mo{m}_1}, \chi_{\mo{m}_2} \rangle \cocomp \pi_1 = \langle \rangle \cocomp \langle \mathbf{true}, \mathbf{true} \rangle \cocomp \pi_1 = \mathbf{true}_{\mo{S}_\mo{p}}$, so by the prior exercise $\mo{m}_\mo{p} \subseteq_\ob{C} \mo{m}_1$ holds.
Similarly, $\mo{m}_\mo{p} \subseteq_\ob{C} \mo{m}_2$ holds.
Thus $\mo{m}_\mo{p}$ is a subset of both $\mo{m}_1$ and $\mo{m}_2$.

Next, suppose there is some subobject $\mo{m} : \ob{S} \mono \ob{C}$ such that $\mo{m} \subseteq_\ob{C} \mo{m}_1$ and $\mo{m} \subseteq_\ob{C} \mo{m}_2$ hold.
Then, by the prior exercise, $\mo{m} \cocomp \langle \chi_{\mo{m}_1}, \chi_{\mo{m}_2} \rangle \cocomp \pi_i = \mo{m} \cocomp \chi_{\mo{m}_i} = \langle \rangle \cocomp \mathbf{true} = \langle \rangle \cocomp \langle \mathbf{true}, \mathbf{true} \rangle \cocomp \pi_i$ for both $i \in \{1, 2\}$, which implies $\mo{m} \cocomp \langle \chi_{\mo{m}_1}, \chi_{\mo{m}_2} \rangle$ equals $\langle \rangle \cocomp \langle \mathbf{true}, \mathbf{true} \rangle$ by property of products.
Because the upper square is a pullback, this implies there exists a morphism $\mo{f} : \ob{S} \mto \ob{S}_\mo{p}$ with the property that $\mo{m}$ equals $\mo{f} \cocomp \mo{m}_\mo{p}$, proving that $\mo{m} \subseteq_\ob{C} \mo{m}_\mo{p}$ holds.
\end{proof}

\end{document}