===== Subobject classifier =====
==== Collection ====
| @#55CCEE: context     | @#55CCEE: ${\bf C}$ ... category with terminal object $*$ and all pullbacks |
| @#FFBB00: definiendum | @#FFBB00: $\top$ in it |
| @#AAFFAA: inclusion   | @#AAFFAA: $\top:{\bf C}[*,\Omega]$ |
| @#FFFDDD: for all     | @#FFFDDD: $m_S:{\bf C}[S,X]$ ... monomorphism |
| @#55EE55: postulate   | @#55EE55: There is a unique arrow $\chi_S$, so that the mono $m_S$ is the pullback of $\top$ along $\chi_S$ |

-----
=== Elaboration ===
The postulate says that for any given mono $m_S$ from $S$ to $X$, there is a unique arrow $\chi_S$ from $X$ to the domain $\Omega$ of $\top$, such that the following completes to a [[pullback . category theory|pullback]] diagram

$$
\require{AMScd}

\begin{CD}          
S  @>{!_S}>>      *                   
\\ 
@V{m_S}VV      @VV{\top}V   
\\                
X  @.      \Omega
\end{CD}
$$

I.e. $S$ is a the pullback object $(X\times_\Omega *)$ associated with the unique arrow $\chi_S$, which $S$ "knows everything about".

=== Theorems ===
Consider a locally small category ${\bf C}$, i.e. one where hom-classes are sets. 

The hom-functor 

${\mathrm{Hom}}(-,\Omega):{\bf C}\longrightarrow{\bf{Set}}$ 

maps objects $X$ to the set ${\mathrm{Hom}}(X,\Omega)$, which by construction is in bijection with the subobjects of $X$.

=== Example ===
In ${\bf{Set}}$, monos are injections and a subset $S\subset X$ exactly corresponds to the inverse image of the characteristic function. Hence, $\Omega$ is given by a two-element set.

For example, we may choose $*=\{0\}$, $\Omega=\{0,1\}$ and $\top(0):=1$.

$$
\require{AMScd}

\begin{CD}          
S  @>{!_S}>>      \{0\}                   
\\ 
@V{m_S}VV      @VV{\top}V   
\\                
X  @>{\chi_S}>>      \{0,1\}
\end{CD}
$$

Going further: The information of the inclusion of elements in a subset $S\subseteq X$ constitutes a relation $\varepsilon_X$ via

$x\in S\leftrightarrow \langle S,x\rangle\in \varepsilon_X$, 

where $\varepsilon_X \subseteq {\mathcal P}(X)\times X$. As a power set ${\mathcal P}(X)$ is in bijection with the space of characteristic functions ${\mathrm{Hom}}(X,\{0,1\})=\{0,1\}^X$, the "is element of"-relation can be defined as the following pullback:

$$
\require{AMScd}

\begin{CD}          
\varepsilon_X  @>{!}>>      \{0\}                   
\\ 
@VVV      @VV{\top}V   
\\                
\{0,1\}^X\times X  @>{\mathrm{eval}}>>      \{0,1\}
\end{CD}
$$

=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Subobject_classifier|Subobject classifier]]

-----
=== Requirements ===
[[Terminal morphism]],
[[Monomorphism]]