diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index 555561b..ba9cbdd 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/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 diff --git a/tex/main.pdf b/tex/main.pdf index b5b59d4..dcf70af 100644 Binary files a/tex/main.pdf and b/tex/main.pdf differ diff --git a/tex/main.tex b/tex/main.tex index f01707b..fe024de 100644 --- a/tex/main.tex +++ b/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 diff --git a/tex/sections/01_introduction.tex b/tex/sections/01_introduction.tex index 77cd775..6c76159 100644 --- a/tex/sections/01_introduction.tex +++ b/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} \ No newline at end of file +\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... \ No newline at end of file diff --git a/tex/sections/02_categories.tex b/tex/sections/02_categories.tex index b9aebd7..8dffa83 100644 --- a/tex/sections/02_categories.tex +++ b/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}