context | C … category with terminal object ∗ and all pullbacks |
definiendum | ⊤ in it |
inclusion | ⊤:C[∗,Ω] |
for all | mS:C[S,X] … monomorphism |
postulate | There is a unique arrow χS, so that the mono mS is the pullback of ⊤ along χS |
The postulate says that for any given mono mS from S to X, there is a unique arrow χS from X to the domain Ω of ⊤, such that the following completes to a 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”.
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.
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}
Wikipedia: Subobject classifier