You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
\emph{Category theory} is a mathematical area of endeavour and language developed to reconcile and unify mathematical phenomena from different disciplines.
291
291
It was developed from the 1940s on, in particular by Samuel Eilenberg and Saunders Mac Lane.
292
292
Category theory studies objects by studying the way they interact with other objects of the same kind.
@@ -300,7 +300,7 @@ \section{Introduction}
300
300
We also study infinite datatypes (see \cref{sec:coinductive}).
301
301
302
302
303
-
\subsection{Learning Material on Category Theory}
303
+
\section{Learning Material on Category Theory}
304
304
\label{sec:material}
305
305
306
306
@@ -317,16 +317,19 @@ \subsection{Learning Material on Category Theory}
317
317
\item The rather substantial textbook by Barr and Wells \cite{barr-wells} (available for free online) covers a lot more than we are going to discuss in these notes.
318
318
319
319
\item The Catsters \cite{catsters} provide a lecture series on category theory on YouTube.
320
+
321
+
\item A list of resources on category theory is maintained at \url{https://www.logicmatters.net/categories/}.
320
322
\end{itemize}
321
323
322
324
Throughout these notes, pointers to further sources, such as textbooks and research articles, are given.
323
325
324
-
\subsection{Notations}
326
+
\chapter{Brief Summary of Logical Foundations}
325
327
\label{sec:notation}
326
328
327
-
A list of notations which we use throughout these lectures notes.
329
+
328
330
\begin{itemize}
329
331
\item If $X$ is a set and $x$ is an element of $X$, we write $x \in X$.
332
+
\item If $X$ and $Y$ are sets
330
333
\item If $X$ is a set and $P$ and $Q$ are properties dependent over the elements of $X$, we write $P\implies Q$ to express that if $P(x)$ holds for an element $x\in X$, then also $Q(x)$ should hold for the element $x$. Moreover, we write $P \iff Q$ if $P\implies Q$ and $Q\implies P$.
331
334
\item If $X$ is a set and $P$ is a property dependent over the elements of $X$, we write:
332
335
\begin{itemize}
@@ -343,7 +346,7 @@ \subsection{Notations}
343
346
344
347
345
348
346
-
\section{Categories}
349
+
\chapter{Categories}
347
350
\label{sec:categories}
348
351
349
352
\begin{reading*}
@@ -357,7 +360,7 @@ \section{Categories}
357
360
\end{reading*}
358
361
359
362
360
-
\subsection{Categories and Examples}
363
+
\section{Categories and Examples}
361
364
362
365
\begin{dfn}\label{dfn:category}
363
366
A \textbf{category} $\CC$ consists of the following data:
@@ -798,7 +801,9 @@ \subsection{Categories and Examples}
798
801
Define a category $\REL$ of sets and binary relations. Recall that given sets $X$ and $Y$ a binary relation $R$ is a subset of the cartesian product $X \times Y$ of the sets.
799
802
\end{exer}
800
803
801
-
\subsection{Isomorphisms}
804
+
\chapter{Special Morphisms in a Category}
805
+
806
+
\section{Isomorphisms}
802
807
\label{sec:isos}
803
808
804
809
\begin{reading*}
@@ -872,7 +877,7 @@ \subsection{Isomorphisms}
872
877
Can you characterize/describe the isomorphisms in $\POS(\NN,\leq)$, $\SKELFINSET$ and $\MAT$?
873
878
\end{exer}
874
879
875
-
\subsection{Sections and Retractions}
880
+
\section{Sections and Retractions}
876
881
\label{sec:sections}
877
882
878
883
@@ -902,7 +907,7 @@ \subsection{Sections and Retractions}
902
907
\end{exer}
903
908
904
909
905
-
\subsection{Monomorphisms and Epimorphisms}
910
+
\section{Monomorphisms and Epimorphisms}
906
911
\label{sec:mono-epi}
907
912
908
913
\begin{reading*}
@@ -1002,7 +1007,7 @@ \subsection{Monomorphisms and Epimorphisms}
An important aspect in computer programming is the transformation of data. For example, if you have a data type $X$, then one can consider also the data type $\List(X)$ of lists with values in $X$. If one thinks of the objects in a category to be data types, then we can ask even more. If $f:X\to Y$ is a function (between the data types), then this also induces a function from the $X$-valued lists to the $Y$-valued lists as follows:
1558
1563
\begin{align}\label{eqn:function_on_list}
1559
1564
\List(f) : \List(X)&\to\List(Y)
@@ -1798,7 +1803,7 @@ \subsection{Categories as Objects of a Category?}
1798
1803
1799
1804
1800
1805
1801
-
\section{Natural Transformations}
1806
+
\chapter{Natural Transformations}
1802
1807
\label{sec:nat-trans}
1803
1808
1804
1809
\begin{dfn} Let $F,G: \CC\to\DD$ be functors. A \textbf{natural transformation} $\alpha$ from $F$ to $G$ consists of the following data:
@@ -2000,7 +2005,7 @@ \subsection{Equivalence of Categories}
2000
2005
\input{data}
2001
2006
2002
2007
2003
-
\section{Conclusions and Further Reading}
2008
+
\chapter{Conclusions and Further Reading}
2004
2009
2005
2010
We have given a brief, and necessarily incomplete, introduction to category theory.
2006
2011
The choice of topics was guided by the applications to programming we considered.
Copy file name to clipboardExpand all lines: tex/adjunctions.tex
+1-1Lines changed: 1 addition & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -1,4 +1,4 @@
1
-
\section{Adjunctions}
1
+
\chapter{Adjunctions}
2
2
\label{sec:adjunctions}
3
3
4
4
\begin{dfn} A pair $(F,G)$ of functors $F : \CC\to\DD, G:\DD\to\CC$ is called an \textbf{adjoint pair} if for every objects $X\in\Ob{\CC}$ and $Y\in\Ob{\DD}$, there exists a bijection
Copy file name to clipboardExpand all lines: tex/forget-free.tex
+1-1Lines changed: 1 addition & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -1,5 +1,5 @@
1
1
2
-
\section{Forgetful and Free Functors}
2
+
\chapter{Forgetful and Free Functors}
3
3
A lot of (mathematical) structures are defined as some other kind of mathematical structure, but where extra structure is added. An example of this is the following:\\
4
4
Recall that a monoid is a set $M$ together with a binary operation $m:M\to M\to M$ which is associative and such that there is an identity element $e$ (see \cref{monoidcategory}). In particular, any monoid has an underlying set and any morphism of monoids has an underlying function (between those sets). So forgetting the binary operation and identity element defines a functor from $\MON$ to $\SET$ which is called a \textit{forgetful functor}:
5
5
\begin{exa}\label{example:forgetful_montoset} The \textbf{forgetful functor from $\MON$ to $\SET$} is the functor specified by the following data:
0 commit comments