adjunctions

This commit is contained in:
Leon Vatthauer 2024-02-23 20:46:47 +01:00
parent a1046d16e1
commit 0eafb889a2
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 105 additions and 3 deletions

1
.gitignore vendored
View file

@ -55,3 +55,4 @@ slides/_minted-main/
thesis/main.bbl-SAVE-ERROR
thesis/main.bcf-SAVE-ERROR
thesis/main.tdo
main.synctex(busy)

View file

@ -47,3 +47,6 @@ Quotienting
bisimilarity
corecursively
coproduct
adjunction
counit
epi

View file

@ -114,14 +114,30 @@ The internal logic of cartesian closed categories is the simply typed $\lambda$-
\section{Coalgebras}
\todo[inline]{Maybe introduce (co-)induction here via (co-)algebras}
\todo[inline]{Introduce (terminal) coalgebras, proof Lambek's lemma}
\todo[inline]{Introduce (terminal) coalgebras, prove Lambek's lemma}
\section{Adjunctions and Free Objects}
\todo[inline]{Introduce adjunctions}
\todo[inline]{Add text}
\begin{definition}[Adjoint Functors]\label{def:adjoint}
Let $\C$ and $\D$ be two categories. Two functors $L : \C \rightarrow \D$ and $R : \D \rightarrow \C$ are called adjoint to each other if there exist natural transformations $\eta : Id \rightarrow R \circ L$ (called unit) and $\epsilon : L \circ R \rightarrow Id$ (called counit) such that the following diagrams commute:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJMWCJdLFsyLDAsIkxSTFgiXSxbMiwxLCJMWCJdLFszLDAsIlJYIl0sWzUsMCwiUkxSWCJdLFs1LDEsIlJYIl0sWzAsMSwiTFxcZXRhIl0sWzEsMiwiXFxlcHNpbG9uIl0sWzAsMiwiaWQiLDJdLFs0LDUsIlJcXGVwc2lsb24iXSxbMyw0LCJcXGV0YSJdLFszLDUsImlkIiwyXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
LX \&\& LRLX \& RX \&\& RLRX \\
\&\& LX \&\&\& RX
\arrow["L\eta", from=1-1, to=1-3]
\arrow["\epsilon", from=1-3, to=2-3]
\arrow["id"', from=1-1, to=2-3]
\arrow["R\epsilon", from=1-6, to=2-6]
\arrow["\eta", from=1-4, to=1-6]
\arrow["id"', from=1-4, to=2-6]
\end{tikzcd}\]
We write $L \dashv R$ and call $L$ the left adjoint of $R$.
\end{definition}
Free objects are constructions capturing the essence of structures in a minimal way, we will rely on free structures in chapter~\ref{chp:iteration} to define a monad in a general setting. We recall the definition to establish some notation:
\begin{definition}[Free Object]
\begin{definition}[Free Object]\label{def:free}
Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \obj{\D}$ is an object $FX \in \obj{\C}$ together with a morphism $\eta : X \rightarrow UFX$ such that the following universal property holds for any $Y \in \obj{\C}$ and $f : X \rightarrow UY$:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d
\[\begin{tikzcd}
@ -133,6 +149,70 @@ Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (w
\end{tikzcd}\]
\end{definition}
\begin{theorem}\label{thm:foladj}
Let $\C$ and $\D$ be two categories and let $U : \C \rightarrow \D$ be a forgetful functor between these categories.
Existence of all free objects on $\D$ yields a left adjoint to the forgetful functor that is called the free functor.
\end{theorem}
\begin{proof}
First we define the free functor $F : \D \rightarrow \C$. $F$ maps objects of $\D$ to the corresponding $FX$ in $\C$ (where $FX$ is the underlying object in Definition~\ref{def:free}).
For any morphism $f : X \rightarrow Y$ in $\D$ we take $Ff = \llbracket\eta \circ f\rrbracket$.
This is a functor because:
\begin{enumerate}
\item The identity law:
\[Fid = \llbracket \eta \circ id \rrbracket = \llbracket \eta \rrbracket = id\]
follows by uniqueness of $\llbracket \eta \rrbracket$ since $id$ satisfies $id \circ \eta = \eta$.
\item Let $f : X \rightarrow Y$ and $g : Y \rightarrow Z$. The compositional law:
\[F(g \circ f) = \llbracket \eta \circ g \circ f \rrbracket = \llbracket \eta \circ g \rrbracket \circ \llbracket \eta \circ f \rrbracket = Fg \circ Ff \]
follows by uniqueness of $\llbracket \eta \circ g \circ f \rrbracket$ since:
\[\llbracket \eta \circ g \rrbracket \circ \llbracket \eta \circ f \rrbracket \circ \eta = \llbracket \eta \circ g \rrbracket \circ \eta \circ f = \eta \circ g \circ f\]
\end{enumerate}
We are left to show that $F$ is left adjoint to $U$. The free object $\eta$ extends to a family of morphisms $(\eta_X : X \rightarrow UFX)_{X \in \obj{D}}$ yielding the unit of the adjunction. For naturality of $\eta$ we need to check:
\[\eta \circ f = \llbracket \eta \circ f \rrbracket \circ \eta = UFf \circ \eta\]
which follows by the universal property of free objects.
As the counit take $\epsilon = \llbracket id \rrbracket : FU \rightarrow Id$. For naturality of $\epsilon$ we show:
\[\llbracket id \rrbracket \circ FU f = \llbracket Uf \rrbracket = f \circ \llbracket id \rrbracket\]
where $f : X \rightarrow Y$.
Using uniqueness of $\llbracket Uf \rrbracket$ we are done by:
\begin{alignat*}{1}
&U (\llbracket id \rrbracket \circ FUf) \circ \eta\\
=\;&U \llbracket id \rrbracket \circ UFUf \circ \eta\\
=\;&U \llbracket id \rrbracket \circ \eta \circ Uf\\
=\;&id \circ Uf\\
=\;&Uf
\end{alignat*}
% \[U (\llbracket id \rrbracket \circ FUf) \circ \eta = U \llbracket id \rrbracket \circ UFUf \circ \eta = U \llbracket id \rrbracket \circ \eta \circ Uf = id \circ Uf = Uf\]
and
\begin{alignat*}{1}
&U (f \circ \llbracket id \rrbracket) \circ \eta\\
=\;&Uf \circ U\llbracket id \rrbracket \circ \eta\\
=\;&Uf \circ id\\
=\;&Uf
\end{alignat*}
% \[U (f \circ \llbracket id \rrbracket) \circ \eta = Uf \circ U\llbracket id \rrbracket \circ \eta = Uf \circ id = Uf \]
Let us finally check the triangle identities. The first one can be proven via:
\[\epsilon \circ F\eta = \llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket = \llbracket \eta \rrbracket = id \]
where the only step missing is $\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket = \llbracket \eta \rrbracket$ which holds since:
\begin{alignat*}{1}
&\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket \circ \eta\\
=\;&\llbracket id \rrbracket \circ \eta \circ \eta\\
=\;&id \circ \eta\\
=\;&\eta
\end{alignat*}
% \[\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket \circ \eta = \llbracket id \rrbracket \circ \eta \circ \eta = id \circ \eta = \eta\]
The second triangle identity is a direct consequence of the universal property of free objects:
\[U\epsilon \circ \eta = U \llbracket id \rrbracket \circ \eta = id\]
We have thereby proven that indeed $F \dashv U$.
\end{proof}
\section{Monads}
Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
@ -163,6 +243,24 @@ Monads are widely known among programmers as a way of modelling effects in pure
\end{tikzcd}\]
\end{definition}
The following theorem makes the relationship of monads and adjoint functors apparent:
\begin{theorem}\label{thm:adjmon}
For every adjunction $L \dashv R$ the triple $(R \circ L, \eta, R\epsilon L)$ is a monad.
\end{theorem}
\begin{proof}
We check the monad laws:
\begin{itemize}
\item[\ref{M1}]
Follows by naturality of $\epsilon$:
\[ R\epsilon L \circ RLR\epsilon L = R(\epsilon L \circ LR\epsilon L) = R (\epsilon L \circ \epsilon L) = R\epsilon L \circ R\epsilon L\]
\item[\ref{M2}]
Follows by the second diagram in Definition~\ref{def:adjoint}:
\[R\epsilon L \circ \eta = id\]
\item[\ref{M3}] Follows by the first diagram in Definition~\ref{def:adjoint}:
\[R\epsilon L \circ RL\eta = R(\epsilon L \circ L\eta) = R(id) = id\]
\end{itemize}
\end{proof}
Morphisms between monads are natural transformations that respect the monad operations:
\change[inline]{