$ \Newextarrow{\xRightarrow}{5,5}{0x21D2}
\begin{array}{}
\relationR & \xrightarrow{} & 1 \\
\downarrow & \mkern-4em\raise1ex\lrcorner & \downarrow\rlap\top \\
\setsX\times\settY & \xrightarrow[\displaystyle \relationR]{\smash{\mkern3em}} & \cattwo \\
\end{array}
$
[1.1] Here we give (a simple, basic, and ubiquitous example) of (a Galois connection). This example arises whenever we have (two sets $\setsX$ and $\settY$) with (a relation $\relationR$ between them),
so that we have in (the category $\Set$) (the pullback diagram at right),
where we use (the same letter “$\relationR$”) to denote both (the predicate on $\setsX\times\settY$, viz. $\relationR : \setsX\times\settY \to \cattwo$)
and (the corresponding subset of $\setsX\times\settY$, viz. $\relationR \subseteq \setsX\times\settY$) (the classical definition of “relation”).
| $ \begin{array}{} \setsA & \xrightarrow{} & 1 \\ \downarrow & \mkern-2em\raise1ex\lrcorner & \downarrow\rlap\top \\ \setsX& \xrightarrow[\displaystyle \setsA]{\smash{\mkern2em}} & \cattwo \\ \end{array} $ | $ \begin{array}{} \settB & \xrightarrow{} & 1 \\ \downarrow & \mkern-2em\raise1ex\lrcorner & \downarrow\rlap\top \\ \settY& \xrightarrow[\displaystyle \settB]{\smash{\mkern2em}} & \cattwo \\ \end{array} $ |
as in (the pullback diagrams in $\Set$ at right).
($\setsA$ and $\settB$) are elements of (the power sets of $\setsX$ and $\settY$), ($\source{\setX\calP \cong [\setX,\cattwo] \equiv [\setX\backslash \cattwo]}$ and $\target{\setY\calP \cong [\setY,\cattwo] \equiv [\setY\backslash \cattwo]}$).
(Each power set) is partially ordered by (inclusion of subsets).
[2.1] In this situation (the following nine statements) are (logically equivalent):
| $\setsA \mathrel{\source\subseteq} [\relationR{/}\settB]$ | subset inclusion in $\source{\setX\cal P}$ | |
| definition of subset inclusion in $\source{\setX\cal P}$ | ||
| $\source{(\forall\eltx\in\setX)}\big[{_\eltsx\setsA} \Rightarrow {_\eltsx[}\relationR{/}\settB]\big]$ | ||
| definition of predicate ${_\eltsx[}\relationR{/}\settB]$ on $\setsX$ | ||
| $\source{(\forall\eltx\in\setX)}\big[{_\eltsx\setsA} \Rightarrow \target{(\forall\elty\in\setY)}[\homst\eltx\relationR\elty{/}\settB_\eltty]\big]$ | using relative quantification: $\source{(\forall\eltx\in\setA)} \target{(\forall\elty\in\setB)} \homst \eltx\relationR\elty$ : {everything in $\setsA$} is $\relationR$-related to {everything in $\settB$} | |
| universal property of $\target{(\forall\elty\in\setY)}$ | ||
| $\source{(\forall\eltx\in\setX)}\target{(\forall\elty\in\setY)}\big[{_\eltsx\setsA} \Rightarrow [\homst\eltx\relationR\elty{/}\settB_\eltty]\big]$ | ||
| (Fubini for universal quantification) and (right closed adjunctions ($-\land\target{\setB_\elty} \dashv [-{/}\target{\setB_\elty}]$) for $\cattwo$) | ||
| $\big(\forall\langle\eltsx,\eltty\rangle \in \setsX\times\settY\big)\big[{_\eltsx\setsA} \land \settB_\eltty \Rightarrow \homst\eltx\relationR\elty\big]$ | central, symmetric version of the equivalent statements | |
| version using relative quantification: $\big(\forall \langle\eltsx,\eltty\rangle \in \setsA\times\settB\big) \homst \eltx \relationR \elty$ | ||
| (Fubini for universal quantification) and (left closed adjunctions ($\source{_\eltx\setA}\land- \dashv [\source{_\eltx\setA}\backslash-]$) for $\cattwo$) | ||
| $\target{(\forall\elty\in\setY)}\source{(\forall\eltx\in\setX)}\big[\settB_\eltty \Rightarrow [{_\eltsx\setsA}\backslash\homst\eltx\relationR\elty]\big]$ | ||
| universal property of $\source{(\forall\eltx\in\setX)}$ | ||
| $\target{(\forall\elty\in\setY)}\big[\settB_\eltty \Rightarrow \source{(\forall\eltx\in\setX)}[{_\eltsx\setsA}\backslash\homst\eltx\relationR\elty]\big]$ | using relative quantification: $\target{(\forall\elty\in\setB)} \source{(\forall\eltx\in\setA)} \homst \eltx\relationR\elty$ : {everything in $\settB$} is $\relationR$-related to {everything in $\setsA$} | |
| definition of predicate $[\setsA\backslash\relationR]_\eltty$ on $\settY$ | ||
| $\target{(\forall\elty\in\setY)}\big[\settB_\eltty \Rightarrow [\setsA\backslash\relationR]_\eltty\big]$ | ||
| definition of subset inclusion in $\target{\setY\cal P}$ | ||
| $\settB \mathrel{\target\subseteq} [\setsA\backslash\relationR]$ | subset inclusion in $\target{\setY\cal P}$ |
| $[\setsA\backslash\relationR]_\eltty$ | predicate $[\setsA\backslash\relationR]_\eltty$ on $\settY$ | |
| definition of predicate $[\setsA\backslash\relationR]_\eltty$ on $\settY$ | ||
| $\source{(\forall\eltx\in\setX)}[{_\eltsx\setsA}\backslash\homst\eltx\relationR\elty]$ | ||
| alternative notations for (the internal hom in $\cattwo$) | ||
| $\source{(\forall\eltx\in\setX)}[{_\eltsx\setsA} \Rightarrow \homst\eltx\relationR\elty]$ | ||
| definition of relative quantifier $\source{(\forall\eltx\in\setA})$ | ||
| $\source{(\forall\eltx\in\setA}) \homst \eltx \relationR \elty$ | $\eltty$ is $\relationR$-related to {everything in $\setA$} |
and $\settB \mapsto \boxed{\relationR{/}\settB} \equiv \source\{\source{\eltx\in\setX} \mathrel{\source\mid} \target{(\forall\elty\in\setB}) \homst \eltx \relationR \elty \source\} \equiv \boxed{\overleftarrow{\settB}}$
between $\source{\setX\calP}$ and $\target\setY\calP{}$ are called
(the Galois connection between $\source{\setX\calP}$ and $\target\setY\calP{}$ induced by $\relationR$).
(Note: At the right are several equivalent formulations for (the predicate $[\setsA\backslash\relationR]_\eltty$ on $\settY$);
similarly, there are equivalent formulations for (the predicate ${_\eltsx[}\relationR{/}\settB]$ on $\setsX$).)
[2.3] These functions are order-reversing
(e.g., $\source{\setA\subseteq\setA'} \Rightarrow \source{\setA'}\backslash\relationR \mathrel{\target\subseteq} \setsA\backslash\relationR$),
thus, (viewing the partially-ordered sets $\source{\setX\calP}$ and $\target\setY\calP{}$ as categories),
(the functions are contravariant functors).
(The logical equivalence of the two outer statements) then proves, in fact is the very definition, that
($\ $($\ $ the contravariant functors $\source-\backslash\relationR = \overrightarrow{()}$ and $\relationR/\target- = \overleftarrow{()}\ $) are adjoint on the right$\ $).
| $\settB$ | $\setA\backslash\relationR$ | ||
| $\relationR{/}\setB$ | |||
| $\setsA$ |
To do so, print (this web page) on (a sheet of paper).
Consider (the cross-like figure at right),
composed of (fully intersecting horizontal and vertical rectangles) (called, informally, “bars”).
Consider [(the top and bottom edges) of (the vertical bar)];
also [(the left and right edges) of (the horizontal bar)], (i.e., the thicker edges.)
Draw (a simple closed curve) around (i.e., outside of) it,
which touches (each of (those four edges) at (at least one point)).
[3.2] Now suppose (the sets $\setsX$ and $\settY$) are ((the bottom and left edges) of (the sheet of paper));
henceforth in this section ($\setsX$ and $\settY$) will denote (those edges).
Then $\setsX\times\settY$ is {the set of all points on (the sheet of paper)}.
Define (the relation $\relationR$) by $\boxed{\homst \eltx \relationR \elty} \iff \langle\eltx,\elty\rangle$ is inside of the curve, i.e. in its interior,
so ($\relationR$ as a subset of $\setsX\times\settY$) is just (the interior of the curve).
(Writing an “$\relationR$” inside the curve clarifies this point.)
[3.3] Let $\setsA$ be [the projection of (the vertical bar of the cross) onto ($\setsX$, the bottom edge)],
and $\settB$ be [the projection of (the horizontal bar of the cross) onto ($\settY$, the left edge)].
Then $\boxed{\relationR{/}\settB} \equiv \source\{\source{\eltx\in\setX} \mathrel{\source\mid} \target{(\forall\elty\in\setB}) \homst \eltx \relationR \elty \source\}$ is [the projection of (the horizontal bar of the cross) onto ($\setsX$, the bottom edge)],
and $\boxed{\setsA\backslash\relationR} \equiv \target\{\target{\elty\in\setY} \mathrel{\target\mid} \source{(\forall\eltx\in\setsA}) \homst \eltx \relationR \elty \target\}$ is [the projection of (the vertical bar of the cross) onto ($\settY$, the left edge)].
References
@nLab[KKR] Kasangian, S.; Kelly, G. M.; Rossi, F. (1983). "Cofibrations and the realization of non-deterministic automata". CTGD. 24 (1): 23–46. MR 0702718.
Section 2 of this paper discusses ($\calV$-modules) with (the base $\calV$) (a not-necessarily symmetric monoidal biclosed category);
for the example KKR consider ($\calV= M\calP$ for $M$ a monoid) see their Section 4.
{WAR], R.F.C. Walters, "Categorical Algebras of Relations" (blog post at Walters’ blog)
The following is incomplete work under development.
$
\begin{array}{}
&& \Set \\
\hline \\
\setsA & \cong & \setsA & \xrightarrow{} & 1 \\
\downarrow && \downarrow & \mkern-2em\raise1ex\lrcorner & \downarrow\rlap\top \\
\setsX\times 1 & \cong & \setsX & \xrightarrow[\smash{\displaystyle \setsA}]{\smash{\mkern2em}} & \cattwo \\
\Vert &&&& \Vert \\
\setsX\times 1 & {}\rlap{\mkern0em\xrightarrow[\textstyle\setsA]{\mkern8em}} &&& \cattwo \\
\end{array}
$
[4.1] In (the basic example in section 1) we had two sets, ($\setsX$ and $\settY$), and (a relation $\relationR$ between them),
i.e., (an arrow $\boxed{\relationR:\setsX\to\settY}$ in the bicategory $\boxed\Rel$ of sets, relations, and inclusions of relations; see reference [WAR]).
[4.2] We also had subsets $\source{\setA\subseteq\setX}$ and $\target{\setB\subseteq\setY}$.
These subsets may be considered as relations $\source{\setA:\setX\to1}$ and $\target{\setB:1\to\setY}$
($1$ the one-element set $1=\{0\} = \{\emptyset\} =\{\ast\}$; the arrows in $\Rel$)
by considering ($\source{\setA\subseteq\setX\cong\setX\times1}$) and ($\target{\setB\subseteq\setY\cong 1\times\setY}$), as in the diagram (in $\Set$, for $\setsA$) at right,
where (the same letter “$\setsA$”) has (four different meanings, as shown below (where typical usage is also shown)):
| a subset of $\setsX$, viz. $\source{\setA\subseteq\setX}$; | a predicate on $\setsX$, viz. $\setsA \mathrel{\source:} \setsX \mathrel{\source\to} \cattwo$; | |
| $\source{\eltx\in\setA}$ | $\source{_\eltx\setA}$ | |
| a subset of $\setsX\times 1$, viz. $\setsA \subseteq \setsX\times 1$; | a predicate on $\setsX\times 1$, viz. $\setA \mathrel{\source:} \setsX\times 1 \mathrel{\source\to} \cattwo$ | |
| $\source{\langle\eltx,0\rangle \in \setA}$ | $\source{\hom \eltx \setA 0}\rlap{\;.}$ |
thus which establishes that the subsets and predicates so defined are in bijection with each other. $ \begin{array}{} && \Rel \\ \hline \\ && 1 \\ & \llap\setsA\source\nearrow & \Downarrow & \target\searrow\rlap\settB \\ \setsX & {}\mkern-1em\rlap{\xrightarrow[\textstyle\relationR]{\smash{\mkern8em}}} &&& \settY \\ \end{array} $ [4.3] Then (the central, symmetric statement considered in section 2)
may be expressed as [(the gamut diagram) in (the bicategory $\Rel$)] at right, the 2-cell being $$\setA\circ\setB = \{\langle\eltsx,\eltty\rangle\in\setsX\times\settY \mid {_\eltsx\setsA}\land\settB_\eltty\} \subseteq \relationR = \{\langle\eltsx,\eltty\rangle\in\setsX\times\settY \mid \homst \eltx \relationR \elty \} \rlap{\;.}$$
| $\Rel \subset \cattwo$-$\Mod$ | $\calV$-$\Mod$ | |
| $\setX,\setY,\setZ\in\Set$ | $\calA,\calB,\calC \in \calV$-$\Cat$ | |
| $\relationR,\relationS,\relationT\ $ (relations ($\cattwo$-modules)) between sets | $\phi,\psi,\theta\ $ ($\ \calV$-modules) between $\calV$-categories | |
| $\begin{array}{} && \setY \\ & \llap\relationR \nearrow & \Downarrow\rlap{a} & \searrow \rlap\relationS \\ \setsX & {}\rlap{\mkern-1em\xrightarrow[\textstyle \relationT]{\smash{\mkern8em}}} &&& \settZ \\ \end{array}$ | $\begin{array}{} && \calB \\ & \llap\phi \nearrow & \Downarrow\rlap{a} & \searrow \rlap\psi \\ \calA & {}\rlap{\mkern-1em\xrightarrow[\smash{\textstyle \theta}]{\smash{\mkern8em}}} &&& \calC \\ \end{array}$ |
| $\begin{array}{l} \relationR \mathop\Rightarrow\limits^{a''} [\relationT{/}\relationS] \\ \big(\forall\langle\eltx,\elty\rangle\in\setX\times\setY\big) \big[ \hom \eltsx \relationR \elty \Rightarrow \hom \eltsx {[\relationT{/}\relationS]} \elty \big] \\ \big(\forall\langle\eltx,\elty\rangle\in\setX\times\setY\big) \big[ \hom \eltsx \relationR \elty \Rightarrow (\forall\eltz\in\setZ) [\hom\eltsx\relationT\eltz {/} \hom\elty\relationS\eltz] \big] \\ \big(\forall\langle\eltx,\elty\rangle\in\setX\times\setY\big) (\forall\eltz\in\setZ) \big[ \hom \eltsx \relationR \elty \Rightarrow [\hom\eltsx\relationT\eltz {/} \hom\elty\relationS\eltz] \big] \\ \end{array}$ | $\setY$ | $\begin{array}{l} \relationS \mathop\Rightarrow\limits^{a'} [\relationR\backslash\relationT] \\ \big(\forall\langle\elty,\eltz\rangle\in\setY\times\setZ\big) \big[ \hom \elty \relationS \eltz \Rightarrow \hom \elty {[\relationR\backslash\relationT]} \eltz \big] \\ \big(\forall\langle\elty,\eltz\rangle\in\setY\times\setZ\big) \big[ \hom \elty \relationS \eltz \Rightarrow (\forall\eltsx\in\setsX) [\hom\eltsx\relationR\elty \backslash \hom\eltx\relationT\eltz] \big] \\ \big(\forall\langle\elty,\eltz\rangle\in\setY\times\setZ\big) (\forall\eltx\in\setX) \big[ \hom \elty \relationS \eltz \Rightarrow [\hom\eltsx\relationR\elty \backslash \hom\eltx\relationT\eltz] \big] \\ \end{array}$ | |
| $\llap\relationR \nearrow$ | $\boxed{\big(\forall\langle\eltx,\elty,\eltz\rangle \in \setX\times\setY\times\setZ\big) \big[ \hom\eltx\relationR\elty \land \hom\elty\relationS\eltz \Rightarrow \hom\eltx\relationT\eltz \big]}$ | $\searrow \rlap\relationS$ | |
| $\setsX$ | $\mkern-3em {}\rlap{\xrightarrow[\smash{\textstyle \relationT}]{\smash{\mkern35em}}}$ | $\settZ$ | |
| $\begin{array}{l} \big(\forall\langle\eltx,\eltz\rangle\in\setX\times\setZ\big) (\forall\elty\in\setY) \big[ \hom\eltx\relationR\elty \land \hom\elty\relationS\eltz \Rightarrow \hom\eltx\relationT\eltz \big] \\ \big(\forall\langle\eltx,\eltz\rangle\in\setX\times\setZ\big) \big[(\exists\elty\in\setY)(\hom\eltx\relationR\elty \land \hom\elty\relationS\eltz) \Rightarrow \hom\eltx\relationT\eltz \big] \\ \big(\forall\langle\eltx,\eltz\rangle\in\setX\times\setZ\big) \big[ \homst \eltx {(\relationR\circ\relationS)} \eltz \Rightarrow \hom\eltx\relationT\eltz \big] \\ \relationR\circ\relationS \mathop\Rightarrow\limits_{a} \relationT \\ \end{array}$ | |||
[Monad-Unit-Condition]
The following seven statements are logically equivalent:
| $\smash{ \source{_\eltx\setA} \Rightarrow \raise1ex{\lower2ex{\scriptstyle\eltsx}{\Big(}} \overleftarrow{\overrightarrow\setA}\raise1ex\Big) }$ | |
| definition $\smash{ \raise1ex{\lower2ex{\scriptstyle\eltsx}{\Big(}} \overleftarrow{\overrightarrow\setA}\raise1ex\Big) }$ | |
| $\source{_\eltx\setA} \Rightarrow \target{(\forall\elty\in\setY)} \bigg[ \homst\eltx\relationR\elty {\bigg/} \raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} \bigg]$ | |
| universal property of $\target{(\forall\elty\in\setY)}$, or: the right adjoint $[\source{_\eltx\setA} \Rightarrow - ]$ preserves limits | |
| $\smash{ \target{(\forall\elty\in\setY)} \Bigg[ \source{_\eltx\setA} \Rightarrow \bigg[ \homst\eltx\relationR\elty {\bigg/} \raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} \bigg] \Bigg] }$ | |
| $\smash{ - \land \raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} \dashv \Big[ - {\bigg/} \raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} \Big] }$ | |
| $\target{(\forall\elty\in\setY)} \bigg[ \source{_\eltx\setA} \land \raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} \Rightarrow \homst\eltx\relationR\elty \bigg]$ | |
| $\source{_\eltx\setA} \land - \dashv [ \source{_\eltx\setA} \backslash - ]$ | |
| $\target{(\forall\elty\in\setY)} \bigg[ \smash{\raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} } \Rightarrow [ \source{_\eltx\setA} \backslash \homst\eltx\relationR\elty] \bigg]$ | |
| definition $\smash{ \raise1ex{\Big(}\overrightarrow\setA\raise1ex{\Big)_\eltty} }$ | |
| $\target{(\forall\elty\in\setY)} \Big[ \source{(\forall\eltxp\in\setX)} [\source{_\eltxp\setA} \backslash\homst\eltxp\relationR\elty] \Rightarrow [ \source{_\eltx\setA} \backslash \homst\eltx\relationR\elty] \Big]$ | |
| universal instantiation, or: counit of ${\source{!_X}}^* \dashv \source{ (\forall \eltxp\in\setX) = \Ran_{!_\setsX} = \forall_{!_\setsX} }$ | |
| $\radjtop$ References; Carboni-Street 1986 "Order Ideals in Categories" https://doi.org/10.2140%2Fpjm.1986.124.275 |
No comments:
Post a Comment