Monday, April 14, 2014

The fork condition as a 2-valued bimodule

Given the situation (in any category) \[ \leftcat {E' \buildrel \textstyle u \over \rightarrow E \mathrel{\mathop\rightrightarrows\limits^{\textstyle\partial_0}_{\textstyle\partial_1}} {}} X \rightcat{{} \buildrel \textstyle f \over \rightarrow Y \buildrel \textstyle v \over \rightarrow Y'}\\ \] we have \[\begin{array}{} \leftcat{\langle\partial_0,\partial_1\rangle} \mathrel\forktwoone \rightcat f & \buildrel \text{defn} \over \iff && \leftcat{\partial_0}\rightcat f = \leftcat{\partial_1}\rightcat f \\ &&& \Big\Downarrow\rlap{\;\text{substitution}}\\ && \leftcat u (\leftcat{\partial_0}\rightcat f) \rightcat v & = & \leftcat u (\leftcat{\partial_1}\rightcat f) \rightcat v\\ && \llap{\text{assoc}}\Big\Vert & \Big\Updownarrow & \Big\Vert\rlap{\text{assoc}}\\ \leftcat{\langle u\partial_0, u\partial_1\rangle} \mathrel\forktwoone \rightcat{fv} & \buildrel \text{defn} \over \iff & \leftcat{(u \partial_0)}\rightcat{(f \rightcat v)} & =& \leftcat{(u \partial_1)}\rightcat{(f \rightcat v)}\\ \end{array}\] This means that the fork condition is in fact a $\cattwo$-valued bimodule,
a bimodule taking values in the category $\cattwo = \{\bot \lt \top\} = \{0 \lt 1\}$,
i.e., a functor \[ \leftcat(\graphsoverx\leftcat{)\op} \times \rightcat(\setsunderx\rightcat) \buildrel \textstyle\forktwoone \over {\class{fork}\rightarrow} \cattwo \]
The kernel $K$ and quotient $Q$ functors provide representations of the $\forktwoone$ bimodule: \[\begin{array}{} \leftcat(\graphsoverx\leftcat{)\op} \mathrel{\leftcat\times} \leftcat(\graphsoverx\leftcat) & \xleftarrow{\textstyle \leftcat 1_\graphsoverx \times \rightadj K} & \leftcat(\graphsoverx\leftcat{)\op} \times \rightcat(\setsunderx\rightcat) & \xrightarrow{\textstyle \leftadj{Q\op} \times \rightcat 1_\setsunderx} & \rightcat(\setsunderx\rightcat{)\op} \mathrel{\rightcat\times} \rightcat(\setsunderx\rightcat)\\ \llap{\hom {\mathrel-} {\leftcat(\graphsoverx\leftcat)} \sim} \leftcat{\Bigg\downarrow} & \cong & \class{fork}{\Bigg\downarrow}\rlap\forktwoone & \cong & \rightcat{\Bigg\downarrow} \rlap{\hom {\mathrel-} {\rightcat(\setsunderx\rightcat)} \sim}\\ \Set & \xleftarrow{} & \cattwo & \xrightarrow{} & \Set\\ \end{array}\]
Each of the two bottom arrows in the above diagram is the functor which takes
the arrow $\bot\lt\top$ in the category $\cattwo$ to
the function $\emptyset \to 1=\{\emptyset\}$ in $\Set$.

No comments:

Post a Comment