Introduction to categories, also some work on introduction

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

@@ -7,3 +7,23 @@ FAU
 codomain
 surjective
 haskell
+hom-set
+Gra
+Pos
+Poset
+Monoid
+homomorphisms
+Monoids
+coproducts
+monomorphisms
+epimorphisms
+isomorphisms
+iso
+monomorphism
+epimorphism
+epi
+Monomorphisms
+Epimorphisms
+Isomorphisms
+cancellative
+Coproducts

tex/main.tex

@@ -9,6 +9,8 @@
 \usepackage{anyfontsize}
 \usepackage{unicode-math}
 \usepackage{amsmath}
+\usepackage{mathrsfs}
+\usepackage{booktabs}
 \usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font
 \usepackage[final]{hyperref}
 \pagestyle{fancy}
@@ -121,8 +123,14 @@
 }
 \makeatother
 %%%
-%%%%
 
+%%% Notation
+%% Category C
+\newcommand{\C}{\ensuremath{\mathscr{C}}}
+\newcommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
+
+%%%
+%%%%
 
 \begin{document}
 %% Titlepage

tex/sections/01_introduction.tex

@@ -67,7 +67,10 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
     \item $iszero : Nat \rightarrow Bool$ is defined by
           \[iszero = foldn\;true\;false!\]
     \item $plus : Nat \rightarrow Nat \rightarrow Nat$ is defined by
-          \[plus = foldn\;id (\lambda f\;n. succ (f\;n)) \]
+          \[plus = foldn\;id\;(succ \circ eval) \]
+          where $eval : (A \rightarrow B) \rightarrow A \rightarrow B$ is defined by
+          \[eval\;f\;a = f\;a\]
+
   \end{itemize}
 \end{example}
 
@@ -179,4 +182,29 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
     \end{tikzcd}\]
   trivially commutes.
 \end{example}
-\subsubsection{Lists}
+\subsubsection{Lists}
+We will now look at the $List$ type and examine it for similar properties. Let us start with the fold function $foldr : C \rightarrow (A \rightarrow C \rightarrow C) \rightarrow List\;A \rightarrow C$, which is defined by
+\begin{alignat*}{2}
+   & foldr\;c\;h\;nil           &  & = c                       \\
+   & foldr\;c\;h\;(cons\;x\;xs) &  & = h\;a\;(foldr\;c\;h\;xs)
+\end{alignat*}
+
+\begin{example}
+  Again, let us define some functions using $foldr$.
+  \begin{itemize}
+    \item $length : List\;A \rightarrow Nat$ is defined by
+          \[length = foldr\;zero\;(succ !)\]
+    \item For $f : A \rightarrow B$ we can define $List$-mapping function $List\;f : List\;A \rightarrow List\;B$ by
+          \[List\;f = foldr\;nil\;(cons \circ f)\]
+  \end{itemize}
+\end{example}
+
+\begin{proposition}
+  $foldr$ satisfies the following two rules
+  \begin{enumerate}
+    \item \customlabel{law:listident}{\textbf{Identity}}: $foldr\;nil\;cons = id_{List\;A}$
+    \item \customlabel{law:listfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat$
+  \end{enumerate}
+\end{proposition}
+
+% TODO Use curried version of data types...

tex/sections/02_categories.tex

@@ -1,6 +1,109 @@
+% chktex-file 46
 \section{Category Theory}
 
+Categories consist of objects and morphisms between those objects, that can be composed in a coherent way.
+This yields a framework for abstracting many mathematical concepts for reasoning on a very abstract level.
+
+\begin{definition} A category \C consists of
+  \begin{itemize}
+    \item a class of objects denoted $\obj{\C}$,
+    \item for every pair of objects $A,B \in \obj{\C}$ a set of morphisms $\C(A,B)$ called the hom-set,
+    \item a morphism $id_A : A \rightarrow A$ for every $A \in \obj{\C}$
+    \item a composition operator $(-) \circ (-) : \C(B,C) \rightarrow \C(A,B) \rightarrow \C(A,C)$ for every $A,B,C \in \obj{\C}$
+  \end{itemize}
+  additionally the composition must be associative and $f \circ id_A = f = id_B \circ f$ for any $f : A \rightarrow B$.
+\end{definition}
+\begin{example} Some standard examples of categories and their objects and morphisms include:
+  \begin{center}
+    \begin{tabular}{l l l}
+      Category               & Objects                & Morphisms                                    \\\midrule
+      \emph{Set}             & Sets                   & Functions                                    \\
+      \emph{Par}             & Sets                   & Partial functions                            \\
+      \emph{Rel}             & Sets                   & Binary relations                             \\
+      \emph{Gra}             & Directed Graphs        & Graph homomorphisms                          \\
+      \emph{Pos}             & Partially ordered sets & Monotone mappings                            \\
+      \emph{Mon}             & Monoids                & Monoid homomorphisms                         \\
+      Monoid $(M, \cdot, e)$ & A single object $*$    & $x : * \rightarrow *$ for every $x \in M$    \\
+      Poset $(X, \leq)$      & Elements of $X$        & $x \leq y \iff \exists! f : x \rightarrow y$
+    \end{tabular}
+  \end{center}
+\end{example}
 \subsection{Special Objects}
+Special objects play an important role in category theory.
+In this chapter we will characterize (finite) products and coproducts, as well as special morphisms such as isomorphisms, monomorphisms and epimorphisms.
+
+\subsubsection{Initial and Terminal Objects}
+
+\begin{definition} The following is the categorical abstraction of ``empty set'' and ``singleton set'' respectively.
+  \begin{enumerate}
+    \item An object $0 \in \obj{\C}$ is called initial if for every $B \in \obj{C}$ there is a unique morphism $¡ : 0 \rightarrow B$.
+    \item An object $1 \in \obj{\C}$ is called terminal if for every $A \in \obj{C}$ there is a unique morphism $! : A \rightarrow 1$.
+  \end{enumerate}
+\end{definition}
+\begin{example} Oftentimes the initial object is an empty structure and the terminal object a singleton structure, some examples are:
+  \begin{center}
+    \begin{tabular}{l l l}
+      Category          & Initial Object                                        & Terminal Object                                       \\\midrule
+      \emph{Set}        & $\emptyset$                                           & ${*}$                                                 \\
+      \emph{Pos}        & $\emptyset$                                           & ${*}$                                                 \\
+      \emph{Gra}        & Empty graph                                           & Singleton graph                                       \\
+      Poset $(X, \leq)$ & $\bot \in X$ such that $\forall x \in X. \bot \leq x$ & $\top \in X$ such that $\forall x \in X. x \leq \top$
+    \end{tabular}
+  \end{center}
+\end{example}
+
+
+\subsubsection{Special Morphisms}
+Now let us characterize special morphisms.
+
+\begin{definition}
+  Let $f : A \rightarrow B$ be a morphism. $f$ is called
+  \begin{itemize}
+    \item an \emph{isomorphism} (\emph{iso}), if there exists an inverse $f^{-1} : B \rightarrow A$ such that $f \circ g = id_B$ and $g \circ f = id_A$;
+    \item a \emph{monomorphism} (\emph{mono}), if for all $g, h : C \rightarrow A$ the implication $f \circ g = f \circ h \Rightarrow g = h$ holds;
+    \item an \emph{epimorphism} (\emph{epi}), if for all $g, h : B \rightarrow C$ the implication $g \circ f = h \circ f \Rightarrow g = h$ holds.
+  \end{itemize}
+\end{definition}
+\begin{example} Let us consider what these notions instantiate to in concrete categories.
+  \begin{center}
+    \begin{tabular}{l l l l}
+      Category               & Monomorphisms               & Epimorphisms                 & Isomorphisms         \\\midrule
+      \emph{Set}             & injective functions         & surjective functions         & bijective functions  \\
+      \emph{Pos, Gra}        & injective morphisms         & surjective morphisms         & bijective morphisms  \\
+      Poset $(X, \leq)$      & all                         & all                          & all                  \\
+      Monoid $(M, \cdot, e)$ & left cancellative $a \in M$ & right cancellative $a \in M$ & invertible $a \in M$
+    \end{tabular}
+  \end{center}
+\end{example}
+
+\begin{proposition}
+  % TODO
+  iso is mono and epi
+\end{proposition}
+
+\begin{proposition}
+  % TODO
+  $f \circ m$ mono then $m$ mono.
+\end{proposition}
+\begin{proposition}
+  % TODO
+  $e \circ f$ epi then $e$ epi.
+\end{proposition}
+% TODO explain up to iso
+
+\begin{proposition}
+  % TODO
+  Initial object up to iso
+\end{proposition}
+\begin{proposition}
+  % TODO
+  Terminal object up to iso
+\end{proposition}
+
+
+\subsubsection{Products and Coproducts}
+% TODO
+
 \subsection{Duality}
 \subsection{Functors}
 \subsection{Natural Transformations}