Work on coalgebras

.gitignore

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

thesis/.vscode/ltex.dictionary.en-US.txt

@@ -47,3 +47,8 @@ Quotienting
 bisimilarity
 corecursively
 coproduct
+adjunction
+counit
+epi
+F-coalgebra
+F-coalgebras

thesis/bib.bib

@@ -98,6 +98,13 @@
   keywords   = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
 }
 
+@book{inductive,
+  title     = {Categorical programming with inductive and coinductive types},
+  author    = {Vene, Varmo},
+  year      = {2000},
+  publisher = {Citeseer}
+}
+
 @inproceedings{Lane1971,
   title  = {Categories for the Working Mathematician},
   author = {Saunders Mac Lane},
@@ -123,6 +130,13 @@
   numpages   = {38}
 }
 
+@online{nad-delay,
+  author  = {Nils Anders Danielsson},
+  title   = {The delay monad, defined coinductively},
+  url     = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
+  urldate = {2024-15-02}
+}
+
 @article{param-corec,
   title    = {Parametric corecursion},
   journal  = {Theoretical Computer Science},
@@ -240,10 +254,3 @@
   biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
   bibsource  = {dblp computer science bibliography, https://dblp.org}
 }
-
-@online{nad-delay,
-  author = {Nils Anders Danielsson},
-  title = {The delay monad, defined coinductively},
-  url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
-  urldate = {2024-15-02}
-}

thesis/src/01_preliminaries.tex

@@ -112,16 +112,81 @@ Categories with finite products (i.e. binary products and a terminal object) are
 A cartesian closed category is a cartesian category $\C$ that also has an exponential object $X^Y$ for any $X, Y \in \C$.
 The internal logic of cartesian closed categories is the simply typed $\lambda$-calculus, which makes them a suitable target for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however does not have to be cartesian closed as to be more general.
 
-\section{Coalgebras}
-\todo[inline]{Maybe introduce (co-)induction here via (co-)algebras}
-\todo[inline]{Introduce (terminal) coalgebras, proof Lambek's lemma}
+\section{Functor Coalgebras}
+Let $F : \C \rightarrow \C$ be an endofunctor. Recall that F-algebras are tuples $(X, \alpha : FX \rightarrow X)$ consisting of an object of $\C$ and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modelling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras let us formally introduce them now.
+
+\begin{definition}[F-Coalgebra]
+  A tuple $(X \in \obj{\C}, \alpha : X \rightarrow FX)$ is called a terminal F-coalgebra.
+\end{definition}
+
+\begin{definition}[Morphisms between Coalgebras]\label{def:coalgmorph}
+  Let $(X \in \obj{\C} , \alpha : X \rightarrow FX)$ and $(Y \in \obj{\C} , \beta : Y \rightarrow FY)$ be two F-coalgebras. A morphism between these coalgebras is a morphism $f : X \rightarrow Y$ such that the following diagram commutes:
+  % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMiwiWSJdLFsyLDAsIkZYIl0sWzIsMiwiRlkiXSxbMSwzLCJcXGJldGEiXSxbMCwyLCJcXGFscGhhIl0sWzAsMSwiZiIsMl0sWzIsMywiRmYiXV0=
+  \[\begin{tikzcd}[ampersand replacement=\&]
+    X \&\& FX \\
+    \\
+    Y \&\& FY
+    \arrow["\beta", from=3-1, to=3-3]
+    \arrow["\alpha", from=1-1, to=1-3]
+    \arrow["f"', from=1-1, to=3-1]
+    \arrow["Ff", from=1-3, to=3-3]
+  \end{tikzcd}\]
+  
+\end{definition}
+
+\begin{proposition}
+  F-coalgebras together with their morphisms form a category that we call $Coalg(F)$.
+\end{proposition}
+\begin{proof}
+  Let $(X , \alpha : X \rightarrow FX)$ be an F-coalgebra. The identity morphism on $(X , \alpha)$ is the identity morphism of $\C$ that trivially satisfies $\alpha \circ id = Fid \circ \alpha$.
+
+  Let $(X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)$ and $(Z , \gamma : Z \rightarrow FZ)$ be F-coalgebras.
+  Composition of $f : (X, \alpha) \rightarrow (Y, \beta)$ and $g : (Y, \beta) \rightarrow (Z, \gamma)$ is composition of the underlying morphisms in $\C$ where:
+  \begin{alignat*}{1}
+    &\gamma \circ g \circ f\\
+    =\;&Fg \circ \beta \circ f\\
+    =\;&Fg \circ Ff \circ \alpha\\
+    =\;&F(g \circ f) \circ \alpha 
+  \end{alignat*}
+\end{proof}
+
+The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling the semantics of coinductive data types. Another special property arises:
+
+\todo[inline]{Characterize final coalgebra first, introduce notation with double bracket}
+
+\begin{theorem}[Lambek's Lemma]
+  Let $(T, t : T \rightarrow FT)$ be a terminal F-coalgebra. Then $t$ is an isomorphism.
+\end{theorem}
+\begin{proof}
+  
+\end{proof}
+
+\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]
+\todo[inline]{Change free object notation from llbracket to something else (llbracket is better for terminal coalg)}
+
+\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 +198,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 +292,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]{