diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index 20768bc..a171c7f 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/tex/.vscode/ltex.dictionary.en-US.txt @@ -37,3 +37,9 @@ monoids n-ary Cocartesian Yoneda +endofunctor +F-Coalgebras +Corecursion +Coinduction +Colimits +Colimit diff --git a/tex/.vscode/settings.json b/tex/.vscode/settings.json index 3659725..7116be1 100644 --- a/tex/.vscode/settings.json +++ b/tex/.vscode/settings.json @@ -27,6 +27,8 @@ "ltex.latex.commands": { "\\customlabel{}": "ignore", "\\setminted[]{}": "ignore", - "\\setmintedinline[]{}": "ignore" + "\\setmintedinline[]{}": "ignore", + "\\setmathfont[]{}": "ignore", + "\\setmathfont{}": "ignore" } } \ No newline at end of file diff --git a/tex/catprog.sty b/tex/catprog.sty new file mode 100644 index 0000000..ac3094d --- /dev/null +++ b/tex/catprog.sty @@ -0,0 +1,221 @@ +% +% Standard macros to typeset papers on category theory and semantics +% +% Unless \catname is defined, make it bold. +% So, call \providecommand{\catname}{\mathcal} +% or \reprovidecommand{\catname}{\mathcal} +% before calling this file if you prefer calligraphic names for categories. +% +% Same applies to other commands. +% +% COPIED FROM https://gitlab.cs.fau.de/i8/TexCommon/ AND THEN ADJUSTED. + +\RequirePackage{bm} % Needed for defbbname +\RequirePackage{mathtools} % Needed for coloneqq + +\providecommand{\catname}{\mathsf} +%\providecommand{\mndname}{\mathbbb} +\providecommand{\clsname}{\mathscr} +\providecommand{\oname}[1]{\operatorname{\mathsf{#1}}} + +%% Defining category names like \BA, \BB, etc +\def\defcatname#1{\expandafter\def\csname B#1\endcsname{\catname{#1}}} +\def\defcatnames#1{\ifx#1\defcatnames\else\defcatname#1\expandafter\defcatnames\fi} +\defcatnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defcatnames + +%% Defining \CA, \CB, etc +\def\defclsname#1{\expandafter\def\csname C#1\endcsname{\clsname{#1}}} +\def\defclsnames#1{\ifx#1\defclsnames\else\defclsname#1\expandafter\defclsnames\fi} +\defclsnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defclsnames + +%% Defining \BBA, \BBB, etc +\def\defbbname#1{\expandafter\def\csname BB#1\endcsname{{\bm{\mathsf{#1}}}}} +\def\defbbnames#1{\ifx#1\defbbnames\else\defbbname#1\expandafter\defbbnames\fi} +\defbbnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defbbnames + +%% Defining \BMA, \BMB, etc +\def\defbbname#1{\expandafter\def\csname BM#1\endcsname{{\bm{\mathsf{#1}}}}} +\def\defbbnames#1{\ifx#1\defbbnames\else\defbbname#1\expandafter\defbbnames\fi} +\defbbnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defbbnames + +%% Some standard categories +\def\Set{\ensuremath{\catname{Set}}} +\def\Par{\ensuremath{\catname{Par}}} +\def\Rel{\ensuremath{\catname{Rel}}} +\def\Cpo{\ensuremath{\catname{Cpo}}} +\def\Pos{\ensuremath{\catname{Pos}}} +\def\Mon{\ensuremath{\catname{Mon}}} +\def\Gra{\ensuremath{\catname{Gra}}} +\providecommand{\Alg}[1]{\ensuremath{\catname{Alg}(#1)}} +%% Objects of category +\providecommand{\obj}[1]{\ensuremath{\vert #1 \vert}} +%% Dual category +\providecommand{\dual}[1]{\ensuremath{#1^{op}}} + +% Misc +%% Commutation of diagrams +\providecommand{\comm}{\circlearrowleft} +%% Banana brackets for catamorphisms +\RequirePackage{stmaryrd} +\providecommand{\cata}[1]{\llparenthesis #1 \rrparenthesis} + + +\providecommand{\eps}{{\operatorname\epsilon}} +\providecommand{\amp}{\mathbin{\&}} + +\providecommand{\argument}{\operatorname{-\!-}} +\providecommand{\altargument}{\underline{\;\;}} + +\providecommand{\wave}[1]{\widetilde{#1}} % Overline wave +\providecommand{\ul}{\underline} % Underline + +\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} +\providecommand{\mplus}{{\scriptscriptstyle\bf+}} % Small '+' for indexing + +\providecommand{\smin}{\smallsetminus} + +\providecommand{\ass}{\mathrel{\coloneqq}} +\providecommand{\bnf}{\mathrel{\Coloneqq}} + +%% Some standard functors +\providecommand{\PSet}{{\mathcal P}} % Powerset +\providecommand{\FSet}{{\mathcal P}_{\omega}} % Finite powerset +\providecommand{\CSet}{{\mathcal P}_{\omega_1}} % Countable powerset +\providecommand{\NESet}{{\mathcal P}^{\mplus}} % Non-empty powerset +\providecommand{\Id}{\operatorname{Id}} + +%% General categorical notation +\providecommand{\Hom}{\mathsf{Hom}} +\providecommand{\id}{\mathsf{id}} +\providecommand{\op}{\mathsf{op}} +\providecommand{\comp}{\mathbin{\circ}} +\providecommand{\iso}{\mathbin{\cong}} +\providecommand{\tensor}{\mathbin{\otimes}} +\providecommand{\unit}{\star} +\providecommand{\bang}{\operatorname!} % Initial/final map + +%% Various arrows +\providecommand{\from}{\leftarrow} + +\providecommand{\ito}{\hookrightarrow} % Injection +\providecommand{\ifrom}{\hookleftarrow} + +\providecommand{\pto}{\mathrel{\rightharpoonup}} % Partial function +\providecommand{\pfrom}{\mathrel{\leftarpoonup}} % + +\providecommand{\tto}{\mathrel{\Rightarrow}} % Double arrow +\providecommand{\tfrom}{\mathrel{\Leftarrow}} % + +\providecommand{\mto}{\mapsto} + +\providecommand{\xto}[1]{\,\xrightarrow{#1}\,} +\providecommand{\xfrom}[1]{\,\xleftarrow{\;#1}\,} + +\providecommand{\To}{\mathrel{\Rightarrow}} % Double arrow +\providecommand{\From}{\mathrel{\Leftarrow}} + +\providecommand{\dar}{\kern-.75pt\operatorname{\downarrow}} +\providecommand{\uar}{\kern-.75pt\operatorname{\uparrow}} + +\providecommand{\Dar}{\kern-.75pt\operatorname{\Downarrow}} +\providecommand{\Uar}{\kern-.75pt\operatorname{\Uparrow}} + + +%% Logic +\providecommand{\True}{\top} +\providecommand{\False}{\bot} + +\providecommand{\bigor}{\bigvee} +\providecommand{\bigand}{\bigwedge} + +\providecommand{\impl}{\Rightarrow} +\providecommand{\equ}{\Longleftrightarrow} + +\providecommand{\entails}{\vdash} + +%% Order +\providecommand{\appr}{\sqsubseteq} +\providecommand{\join}{\sqcup} +\providecommand{\meet}{\sqcap} + +\providecommand{\bigjoin}{\bigsqcup} +\providecommand{\bigmeet}{\bigsqcap} + +%% Products +\providecommand{\fst}{\oname{fst}} +\providecommand{\snd}{\oname{snd}} +\providecommand{\pr}{\oname{pr}} + +\providecommand{\brks}[1]{\langle #1\rangle} +\providecommand{\Brks}[1]{\bigl\langle #1\bigr\rangle} + +%% Coproducts +\providecommand{\inl}{\oname{inl}} +\providecommand{\inr}{\oname{inr}} +\providecommand{\inj}{\oname{in}} + +\DeclareSymbolFont{Symbols}{OMS}{cmsy}{m}{n} +\DeclareMathSymbol{\iobj}{\mathord}{Symbols}{"3B} +%\DeclareRobustCommand{\iobj}{\emptyset} + +%% CCC +\providecommand{\curry}{\oname{curry}} +\providecommand{\uncurry}{\oname{uncurry}} +\providecommand{\ev}{\oname{ev}} + +% Semantic brackets +\RequirePackage{stmaryrd} + +\providecommand{\lsem}{\llbracket} +\providecommand{\rsem}{\rrbracket} +\providecommand{\sem}[1]{\lsem #1 \rsem} + +\providecommand{\Lsem}{\bigl\llbracket} +\providecommand{\Rsem}{\bigr\rrbracket} +\providecommand{\Sem}[1]{\Lsem #1 \Rsem} + +% Typographic +\providecommand{\comma}{,\operatorname{}\linebreak[1]} % possibly line-breaking comma +\providecommand{\dash}{\nobreakdash-\hspace{0pt}} % non-line-breaking hyphen +\providecommand{\erule}{\rule{0pt}{0pt}} % Empty object whose emptiness +% is not detected by LaTeX + +\providecommand{\by}[1]{\text{/\!\!/~#1}} % Comments in equations +\providecommand{\pacman}[1]{} % Hide a piece of text + +\newcommand{\undefine}[1]{\let #1\relax} % Make a command undefined + +\providecommand{\noqed}{\def\qed{}} % Undefine the QED symbol + +% -1 superscript for the inversion operator +\providecommand{\mone}{{\text{\kern.5pt\rmfamily-}\mathsf{\kern-.5pt1}}} + +\makeatletter +\@ifpackageloaded{enumitem}{}{ + \RequirePackage[loadonly]{enumitem} % without [loadonly] +} % conflicts with Beamer +\makeatother + +% Condensed list environments +\newlist{citemize}{itemize}{1} +\setlist[citemize]{label=\labelitemi,wide} +%leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left} + +\newlist{cenumerate}{enumerate}{1} +\setlist[cenumerate,1]{label=\arabic*.~,ref={\arabic*},wide} +%leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left} + +%\newenvironment{citemize}{\begin{itemize}[leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left]}{\end{itemize}} +%\newenvironment{cenumerate}{\begin{enumerate}[leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left]}{\end{enumerate}} + +%% A macro for defining mixfix operators +\makeatletter +\def\mfix#1{\oname{#1}\@ifnextchar\bgroup\@mfix{}} % processing odd arguments +\def\@mfix#1{#1\@ifnextchar\bgroup\mfix{}} % processing even arguments +\makeatother + +% %% Instances if mfix +% \providecommand{\ift}[3]{\mfix{if}{\mathbin{}#1}{then}{\mathbin{}#2}{else}{\mathbin{}#3}} +% \providecommand{\case}[3]{\mfix{case}{\mathbin{}#1}{of}{#2}{\kern-1pt;}{\mathbin{}#3}} + + diff --git a/tex/main.pdf b/tex/main.pdf index ea79009..bcb2b27 100644 Binary files a/tex/main.pdf and b/tex/main.pdf differ diff --git a/tex/main.tex b/tex/main.tex index eb1092a..f5ffd9d 100644 --- a/tex/main.tex +++ b/tex/main.tex @@ -6,9 +6,15 @@ \usepackage[ngerman, english]{babel} \babeltags{german=ngerman} \usepackage{anyfontsize} -\usepackage{unicode-math} +\usepackage{mathtools} +\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math} +\setmathfont[math-style=ISO,version=normal]{Latin Modern Math} +\setmathfont[version=bold,math-style=ISO,FakeBold = 3]{Latin Modern Math} +\setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{XITS Math} +\setmathfont[range=\mathscr]{XITS Math} \usepackage{amsmath} -\usepackage{mathrsfs} +\usepackage{stmaryrd} +% \usepackage{mathrsfs} \usepackage{booktabs} \usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font \usepackage[final]{hyperref} @@ -18,7 +24,7 @@ \renewcommand{\subsectionmark}[1]{\markright{\thesubsection\ #1}} \pagestyle{scrheadings} \newcounter{resumeenum} % for resuming enumerated lists, https://tex.stackexchange.com/a/1702 - +\usepackage{catprog} %%%% %%%% Metadata @@ -129,14 +135,8 @@ \makeatother %%% -%%% Notation -%% Categories -\newcommand{\C}{\ensuremath{\mathscr{C}}} -\newcommand{\D}{\ensuremath{\mathscr{D}}} -%% Objects of category -\newcommand{\obj}[1]{\ensuremath{\vert #1 \vert}} -%% Dual category -\newcommand{\dual}[1]{\ensuremath{#1^{op}}} +%%% Unicode substitutions +\def\circlearrowleft{↺} %%% %%%% diff --git a/tex/sections/01_introduction.tex b/tex/sections/01_introduction.tex index 11f2fc8..2138264 100644 --- a/tex/sections/01_introduction.tex +++ b/tex/sections/01_introduction.tex @@ -1,11 +1,11 @@ -\chapter{Introduction} +\chapter{Introduction}\label{chp:introduction} This is a summary of the course ``Algebra des Programmierens'' taught by Prof.\ Dr.\ Stefan Milius in the winter term 2023/2024 at the FAU~\footnote{Friedrich-Alexander-Universität Erlangen-Nürnberg}. The course is based on~\cite{poll1999algebra} with~\cite{adamek1990abstract} as a reference for category theory. Goal of the course is to develop a mathematical theory for semantics of data types and their accompanying proof principles. The chosen environment is the field of category theory. \section{Functions} -A function $f : X \rightarrow Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$). +A function $f : X \to Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$). More concretely $f$ is a relation $f \subseteq X \times Y$ which is \begin{itemize} \item \emph{left-total}, i.e.\ for all $x \in X$ exists some $y \in Y$ such that $(x,y) \in f$; @@ -14,24 +14,24 @@ More concretely $f$ is a relation $f \subseteq X \times Y$ which is Often, one is also interested in the symmetrical properties, a function is called \begin{itemize} - \item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \rightarrow x = x'$ holds; + \item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \to x = x'$ holds; \item \emph{surjective} or \emph{right-total} if for every $y \in Y$ there exists an $x \in X$ such that $f(x) = y$; \item \emph{bijective} if it is injective and surjective. \end{itemize} \begin{example} \begin{enumerate} - \item The identity function $id_A : A \rightarrow A$, $id_A(x) = x$ - \item The constant function $b! : A \rightarrow B$ for $b \in B$ defined by $b!(x) = b$ - \item The inclusion function $i_A : A \rightarrow B$ for $A \subseteq B$ defined by $i_A(x) = x$ - \item Constants $b : 1 \rightarrow B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$. - \item Composition of function $f : A \rightarrow B, g : B \rightarrow C$ called $g \circ f : A \rightarrow C$ defined by $(g \circ f)(x) = g(f(x))$. - \item The empty function $¡ : \emptyset \rightarrow B$ - \item The singleton function $! : A \rightarrow 1$ + \item The identity function $id_A : A \to A$, $id_A(x) = x$ + \item The constant function $b! : A \to B$ for $b \in B$ defined by $b!(x) = b$ + \item The inclusion function $i_A : A \to B$ for $A \subseteq B$ defined by $i_A(x) = x$ + \item Constants $b : 1 \to B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$. + \item Composition of function $f : A \to B, g : B \to C$ called $g \circ f : A \to C$ defined by $(g \circ f)(x) = g(f(x))$. + \item The empty function $¡ : \emptyset \to B$ + \item The singleton function $! : A \to 1$ \end{enumerate} \end{example} -\section{Data Types} +\section{Data Types}\label{sec:datatypes} Programs work with data that should ideally be organized in a useful manner. A useful representation for data in functional programming is by means of \emph{algebraic data types}. @@ -54,7 +54,7 @@ Such data types (parametric or non-parametric) usually come with a principle for Equivalently, every function defined by recursion can be defined via a \emph{fold}-function which satisfies an identity and fusion law, which replace the induction principle. Let us now consider two examples of data types and illustrate this. \subsection{Natural Numbers} -The type of natural numbers comes with a fold function $foldn : C \rightarrow (Nat \rightarrow C) \rightarrow Nat \rightarrow C$ for every $C$, defined by +The type of natural numbers comes with a fold function $foldn : C \to (Nat \to C) \to Nat \to C$ for every $C$, defined by \begin{alignat*}{2} & foldn\;c\;h\;zero & & = c \\ & foldn\;c\;h\;(suc\;n) & & = h\;(foldn\;c\;h\;n) @@ -63,11 +63,11 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N \begin{example} Let us now consider some functions defined in terms of $foldn$. \begin{itemize} - \item $iszero : Nat \rightarrow Bool$ is defined by + \item $iszero : Nat \to Bool$ is defined by \[iszero = foldn\;true\;false!\] - \item $plus : Nat \rightarrow Nat \rightarrow Nat$ is defined by + \item $plus : Nat \to Nat \to Nat$ is defined by \[plus = foldn\;id\;(succ \circ eval) \] - where $eval : (A \rightarrow B) \rightarrow A \rightarrow B$ is defined by + where $eval : (A \to B) \to A \to B$ is defined by \[eval\;f\;a = f\;a\] \end{itemize} @@ -78,7 +78,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N \begin{enumerate} \item \customlabel{law:natident}{\textbf{Identity}}: $foldn\;zero\;succ = id_{Nat}$ \item \customlabel{law:natfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat - \rightarrow C$ and $k : C \rightarrow C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically: + \to C$ and $k : C \to C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically: % https://q.uiver.app/#q=WzAsNSxbMiwwLCJDIl0sWzQsMCwiQyJdLFsyLDIsIkMnIl0sWzQsMiwiQyciXSxbMCwwLCIxIl0sWzQsMCwiYyJdLFswLDIsImsiXSxbNCwyLCJjJyIsMl0sWzAsMSwiaCIsMl0sWzIsMywiaCciLDJdLFsxLDMsImsiLDFdXQ== \[ \begin{tikzcd}[ampersand replacement=\&] @@ -139,7 +139,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N \begin{example} The identity and fusion laws can in turn be used to prove the following induction principle: - For any predicate $p : Nat \rightarrow Bool$, + For any predicate $p : Nat \to Bool$, \begin{enumerate} \item $p\;zero = true$ and \item $p \circ succ = p$ @@ -182,7 +182,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N trivially commutes. \end{example} \subsection{Lists}\label{subsec: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 +We will now look at the $List$ type and examine it for similar properties. Let us start with the fold function $foldr : C \to (A \to C \to C) \to List\;A \to 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) @@ -191,9 +191,9 @@ We will now look at the $List$ type and examine it for similar properties. Let u \begin{example} Again, let us define some functions using $foldr$. \begin{itemize} - \item $length : List\;A \rightarrow Nat$ is defined by + \item $length : List\;A \to 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 + \item For $f : A \to B$ we can define $List$-mapping function $List\;f : List\;A \to List\;B$ by \[List\;f = foldr\;nil\;(cons \circ f)\] \end{itemize} \end{example} diff --git a/tex/sections/02_categories.tex b/tex/sections/02_categories.tex index 2baf2e5..b6f7de1 100644 --- a/tex/sections/02_categories.tex +++ b/tex/sections/02_categories.tex @@ -1,29 +1,30 @@ +% chktex-file 1 \chapter{Category Theory} Categories consist of objects and morphisms between those objects, that can be composed in a coherent way. This yields a framework for abstraction of many mathematical concepts that enables us to reason on a very abstract level. -\begin{definition}[Category] A category \C consists of +\begin{definition}[Category] A category $\CC$ 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}$ + \item a class of objects denoted $\obj{\CC}$, + \item for every pair of objects $A,B \in \obj{\CC}$ a set of morphisms $\CC(A,B)$ called the hom-set, + \item a morphism $id_A : A \to A$ for every $A \in \obj{\CC}$ + \item a composition operator $(\argument) \comp (\argument) : \CC(B,C) \to \CC(A,B) \to \CC(A,C)$ for every $A,B,C \in \obj{\CC}$ \end{itemize} - additionally the composition must be associative and $f \circ id_A = f = id_B \circ f$ for any $f : A \rightarrow B$. + additionally the composition must be associative and $f \comp id_A = f = id_B \comp f$ for any $f : A \to 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$ + Category & Objects & Morphisms \\\midrule + \Set & Sets & Functions \\ + \Par & Sets & Partial functions \\ + \Rel & Sets & Binary relations \\ + \Gra & Directed Graphs & Graph homomorphisms \\ + \Pos & Partially ordered sets & Monotone mappings \\ + \Mon & Monoids & Monoid homomorphisms \\ + Monoid $(M, \cdot, e)$ & A single object $*$ & $x : * \to *$ for every $x \in M$ \\ + Poset $(X, \leq)$ & Elements of $X$ & $x \leq y \iff \exists! f : x \to y$ \end{tabular} \end{center} \end{example} @@ -35,17 +36,17 @@ In this chapter we will characterize (finite) products and coproducts, as well a \begin{definition}[Initial and Terminal Objects] 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$. + \item An object $0 \in \obj{\BC}$ is called initial if for every $B \in \obj{C}$ there is a unique morphism $¡ : 0 \to B$. + \item An object $1 \in \obj{\CC}$ is called terminal if for every $A \in \obj{C}$ there is a unique morphism $! : A \to 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 \\ + \Set & $\emptyset$ & ${*}$ \\ + \Pos & $\emptyset$ & ${*}$ \\ + \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} @@ -56,18 +57,18 @@ In this chapter we will characterize (finite) products and coproducts, as well a Now let us characterize special morphisms. \begin{definition}[Special Morphisms] - Let $f : A \rightarrow B$ be a morphism. $f$ is called + Let $f : A \to 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. + \item an \emph{isomorphism} (\emph{iso}), if there exists an inverse $f^{-1} : B \to A$ such that $f \comp g = id_B$ and $g \comp f = id_A$; + \item a \emph{monomorphism} (\emph{mono}), if for all $g, h : C \to A$ the implication $f \comp g = f \comp h \Rightarrow g = h$ holds; + \item an \emph{epimorphism} (\emph{epi}), if for all $g, h : B \to C$ the implication $g \comp f = h \comp 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 \\ + \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$ @@ -80,19 +81,19 @@ Now let us characterize special morphisms. \begin{proof} Let $f$ be an isomorphism. \begin{itemize} - \item $f \circ g = f \circ h$ implies $g = f^{-1} \circ f \circ g = f^{-1} \circ f \circ h = h$, thus $f$ is a monomorphism. - \item $g \circ f = h \circ f$ implies $g = g \circ f \circ f^{-1} = h \circ f \circ f^{-1} = h$, thus $f$ is an epimorphism. + \item $f \comp g = f \comp h$ implies $g = f^{-1} \comp f \comp g = f^{-1} \comp f \comp h = h$, thus $f$ is a monomorphism. + \item $g \comp f = h \comp f$ implies $g = g \comp f \comp f^{-1} = h \comp f \comp f^{-1} = h$, thus $f$ is an epimorphism. \end{itemize} \end{proof} -\begin{proposition}\label{prop:monosplitting} If $f \circ m$ is a monomorphism then $m$ is also a monomorphism. +\begin{proposition}\label{prop:monosplitting} If $f \comp m$ is a monomorphism then $m$ is also a monomorphism. \end{proposition} \begin{proof} - Let $m \circ g = m \circ h$. To show that $g = h$ it suffices to show that $f \circ m \circ g = f \circ m \circ h$, which indeed follows by assumption. + Let $m \comp g = m \comp h$. To show that $g = h$ it suffices to show that $f \comp m \comp g = f \comp m \comp h$, which indeed follows by assumption. \end{proof} -\begin{proposition}\label{prop:episplitting} If $e \circ f$ is an epimorphism then $e$ is also an epimorphism. +\begin{proposition}\label{prop:episplitting} If $e \comp f$ is an epimorphism then $e$ is also an epimorphism. \end{proposition} \begin{proof} - Let $g \circ e = h \circ e$. To show that $g = h$ it suffices to show that $g \circ e \circ f = h \circ e \circ f$, which again follows by assumption. + Let $g \comp e = h \comp e$. To show that $g = h$ it suffices to show that $g \comp e \comp f = h \comp e \comp f$, which again follows by assumption. \end{proof} Categorical structures like initial objects are usually not uniquely identified, there might be multiple initial objects in a category. However, all initial objects in a category are isomorphic, we call this ``unique up to isomorphism''. @@ -100,7 +101,7 @@ Categorical structures like initial objects are usually not uniquely identified, \begin{proposition}\label{prop:init_up_to} Initial objects are unique up to isomorphism. \end{proposition} \begin{proof} - Let $0, 0' \in \obj{\C}$ be two initial objects of $\C$ with the unique morphisms $¡_A : 0 \rightarrow A$ and ${¡'}_A : 0' \rightarrow A$. + Let $0, 0' \in \obj{\CC}$ be two initial objects of $\CC$ with the unique morphisms $¡_A : 0 \to A$ and ${¡'}_A : 0' \to A$. The isomorphism is: % https://q.uiver.app/#q=WzAsMixbMCwwLCIwIl0sWzIsMCwiMCciXSxbMSwwLCJ7wqEnfV8wIiwyLHsiY3VydmUiOi0yfV0sWzAsMSwiwqFfezAnfSIsMCx7ImN1cnZlIjotMn1dXQ== \[ @@ -110,12 +111,12 @@ Categorical structures like initial objects are usually not uniquely identified, \arrow["{¡_{0'}}", curve={height=-12pt}, from=1-1, to=1-3] \end{tikzcd} \] - Note that by uniqueness $¡_{0'} \circ {¡'}_0 = {¡'}_{0'} = id_{0'}$ and ${¡'}_0 \circ ¡_{0'} = ¡_0 = id_0$. + Note that by uniqueness $¡_{0'} \comp {¡'}_0 = {¡'}_{0'} = id_{0'}$ and ${¡'}_0 \comp ¡_{0'} = ¡_0 = id_0$. \end{proof} \begin{proposition}\label{prop:term_up_to} Terminal objects are unique up to isomorphism. \end{proposition} \begin{proof} - Let $1, 1' \in \obj{\C}$ be two terminal objects of $\C$ with the unique morphisms $!_A : A \rightarrow 1$ and ${!'}_A : A \rightarrow 1'$. + Let $1, 1' \in \obj{\CC}$ be two terminal objects of $\CC$ with the unique morphisms $!_A : A \to 1$ and ${!'}_A : A \to 1'$. The isomorphism is: % https://q.uiver.app/#q=WzAsMixbMCwwLCIxIl0sWzIsMCwiMSciXSxbMCwxLCJ7ISd9XzEiLDAseyJjdXJ2ZSI6LTJ9XSxbMSwwLCIhX3sxJ30iLDAseyJjdXJ2ZSI6LTJ9XV0= \[ @@ -125,7 +126,7 @@ Categorical structures like initial objects are usually not uniquely identified, \arrow["{!_{1'}}", curve={height=-12pt}, from=1-3, to=1-1] \end{tikzcd} \] - Note that by uniqueness ${!'}_1 \circ !_{1'} = {!'}_{1'} = id_{1'}$ and $!_{1'} \circ {!'}_1 = !_1 = id_1$. + Note that by uniqueness ${!'}_1 \comp !_{1'} = {!'}_{1'} = id_{1'}$ and $!_{1'} \comp {!'}_1 = !_1 = id_1$. \end{proof} \section{Duality} @@ -134,17 +135,17 @@ It seems that we should somehow be able to construct one proof from the other, s This is actually the case, we can for example say that \autoref{prop:episplitting} follows from \autoref{prop:monosplitting} by \emph{duality}. \begin{definition}[Dual Category] - Every category $\C$ has a \emph{dual category} $\dual{\C}$ defined by + Every category $\CC$ has a \emph{dual category} $\dual{\CC}$ defined by \begin{itemize} - \item $\obj{\dual{\C}} = \obj{\C}$ - \item $\dual{\C}(A,B) = \C(B,A)$ + \item $\obj{\dual{\CC}} = \obj{\CC}$ + \item $\dual{\CC}(A,B) = \CC(B,A)$ \end{itemize} \end{definition} \begin{example} Examples are: \begin{enumerate} \item In a poset the order relation gets reversed. - \item \emph{\dual{Rel}} is isomorphic to \emph{Rel}, since subsets of $A \times B$ are in bijection with subsets of $B \times A$ - \item $\dual{(\dual{\C})} = \C$ + \item \emph{\dual{Rel}} is isomorphic to $\Rel$, since subsets of $A \times B$ are in bijection with subsets of $B \times A$ + \item $\dual{(\dual{\CC})} = \CC$ \end{enumerate} \end{example} @@ -163,7 +164,7 @@ This yields a proof principle ``by duality'', where every theorem yields another \section{Products and Coproducts} The categorical abstraction of Cartesian products is: \begin{definition}[Product] - The \emph{product} of two objects $A, B \in \obj{\C}$ is an object that we call $A \times B$ together with morphisms $\pi_1 : A \times B \rightarrow A$ and $\pi_2 : A \times B \rightarrow B$ (the projections), where the following property holds: + The \emph{product} of two objects $A, B \in \obj{\CC}$ is an object that we call $A \times B$ together with morphisms $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$ (the projections), where the following property holds: % https://q.uiver.app/#q=WzAsNCxbMiwyLCJBIFxcdGltZXMgQiJdLFs0LDIsIkIiXSxbMCwyLCJBIl0sWzIsMCwiQyJdLFswLDIsIlxccGlfMSJdLFswLDEsIlxccGlfMiIsMl0sWzMsMiwiZiIsMl0sWzMsMSwiZyJdLFszLDAsIlxcZXhpc3RzIVxcbGFuZ2xlIGYsIGcgXFxyYW5nbGUiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0= \[ \begin{tikzcd} @@ -180,15 +181,15 @@ The categorical abstraction of Cartesian products is: \end{definition} \begin{example} Some examples include: \begin{enumerate} - \item \emph{Set}: The product of two sets $A$ and $B$ is the Cartesian product $A \times B = \{ (a,b)\;\vert\;a \in A, b \in B\}$. - \item \emph{Gra}: The product of two graphs has as vertices the Cartesian product of the vertices of both graphs and an edge $(v_1, u_1) \rightarrow (v_2, u_2)$ iff there exists edges $v_1 \rightarrow v_2$ and $u_1 \rightarrow u_2$. - \item \emph{Pos}: Given two posets $(A, \leq), (B, \leq)$, the product is the Cartesian product of $A$ and $B$ where $(a,b) \leq (a', b') \iff a \leq a' \land b \leq b'$. + \item $\Set$: The product of two sets $A$ and $B$ is the Cartesian product $A \times B = \{ (a,b)\;\vert\;a \in A, b \in B\}$. + \item $\Gra$: The product of two graphs has as vertices the Cartesian product of the vertices of both graphs and an edge $(v_1, u_1) \to (v_2, u_2)$ iff there exists edges $v_1 \to v_2$ and $u_1 \to u_2$. + \item $\Pos$: Given two posets $(A, \leq), (B, \leq)$, the product is the Cartesian product of $A$ and $B$ where $(a,b) \leq (a', b') \iff a \leq a' \land b \leq b'$. \item Let $(X, \leq)$ be a poset, the product of $a, b \in X$ is the greatest lower bound of $a$ and $b$. \end{enumerate} \end{example} Dual to products are: \begin{definition}[Coproduct] - The \emph{coproduct} of two objects $A, B \in \obj{\C}$ is an object that we call $A + B$ together with morphisms $i_1 : A \rightarrow A + B$ and $i_2 : B \rightarrow A + B$ (the injections), where the following property holds: + The \emph{coproduct} of two objects $A, B \in \obj{\CC}$ is an object that we call $A + B$ together with morphisms $i_1 : A \to A + B$ and $i_2 : B \to A + B$ (the injections), where the following property holds: % https://q.uiver.app/#q=WzAsNCxbMiwwLCJBK0IiXSxbMCwwLCJBIl0sWzQsMCwiQiJdLFsyLDIsIkMiXSxbMSwwLCJpXzEiXSxbMiwwLCJpXzIiLDJdLFsxLDMsImYiLDJdLFsyLDMsImciXSxbMCwzLCJcXGV4aXN0cyFbZixnXSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== \[ \begin{tikzcd} @@ -205,11 +206,11 @@ Dual to products are: \end{definition} \begin{example} Examples include: \begin{enumerate} - \item \emph{Set}: The coproduct of two sets $A$ and $B$ is the disjoint union $A + B = \{ (a,0)\;\vert\;a \in A \} \cup \{ (b, 1) \vert b \in B \}$. - \item \emph{Pos}: The coproduct of ordered sets $(A, \leq)$ and $(B, \leq)$ is the disjoint union $A+B$ where $z \leq z'$ iff $z, z' \in A$ and $z \leq z'$ or $z, z' \in B$ and $z \leq z'$. - \item \emph{Gra}: Analogous to \emph{Pos}. + \item $\Set$: The coproduct of two sets $A$ and $B$ is the disjoint union $A + B = \{ (a,0)\;\vert\;a \in A \} \cup \{ (b, 1) \vert b \in B \}$. + \item $\Pos$: The coproduct of ordered sets $(A, \leq)$ and $(B, \leq)$ is the disjoint union $A+B$ where $z \leq z'$ iff $z, z' \in A$ and $z \leq z'$ or $z, z' \in B$ and $z \leq z'$. + \item $\Gra$: Analogous to $\Pos$. \item Let $(X, \leq)$ be a poset, the coproduct of $a,b \in X$ is the least upper bound of $a$ and $b$. - \item \emph{Rel}: Analogous to \emph{Set} the coproduct is the disjoint union. Since $\emph{Rel} \cong \dual{\emph{Rel}}$ we know that the product is also the disjoint union. + \item $\Rel$: Analogous to $\Set$ the coproduct is the disjoint union. Since $\Rel \iso \dual{\Rel}$ we know that the product is also the disjoint union. \end{enumerate} \end{example} @@ -219,7 +220,7 @@ Dual to products are: \begin{proof} The usual proof is somewhat analogous to the proof of \autoref{prop:term_up_to}. Instead, we will prove it like this: - Consider the category $\emph{span}_{\C}(A,B)$ where objects are triples $A \overset{f}{\leftarrow} C \overset{g}{\rightarrow} B$ and morphisms $(C, f, g) \rightarrow (C', f', g')$ are morphisms $k : C \rightarrow C'$ in $\C$ such that + Consider the category $\emph{span}_{\CC}(A,B)$ where objects are triples $A \overset{f}{\leftarrow} C \overset{g}{\to} B$ and morphisms $(C, f, g) \to (C', f', g')$ are morphisms $k : C \to C'$ in $\CC$ such that % https://q.uiver.app/#q=WzAsNCxbMiwwLCJDIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJDJyJdLFswLDEsImYiLDJdLFswLDIsImciXSxbMywxLCJmJyJdLFszLDIsImcnIiwyXSxbMCwzLCJrIl1d \[ \begin{tikzcd} @@ -235,7 +236,7 @@ Dual to products are: \arrow["k", from=1-3, to=5-3] \end{tikzcd} \] - commutes. Products of $A$ and $B$ are the final objects in $\emph{span}_{\C}(A,B)$ and are thus unique up to isomorphism. + commutes. Products of $A$ and $B$ are the final objects in $\emph{span}_{\CC}(A,B)$ and are thus unique up to isomorphism. \end{proof} By duality, we get: \begin{proposition} @@ -245,41 +246,41 @@ By duality, we get: We can now characterize products (and later dually coproducts) as a commutative monoid: \begin{proposition} - $1$ is a unit of $\times$, i.e.\ $A \cong A \times 1$ for any $A \in \obj{\C}$. + $1$ is a unit of $\times$, i.e.\ $A \iso A \times 1$ for any $A \in \obj{\CC}$. \end{proposition} \begin{proof} - Take $\langle id_A , !_A \rangle : A \rightarrow A \times 1$ and $\pi_1 : A \times 1 \rightarrow A$, this indeed constitutes an isomorphism, since - \[\pi_1 \circ \langle id_A , !_A \rangle = id_A \] + Take $\langle id_A , !_A \rangle : A \to A \times 1$ and $\pi_1 : A \times 1 \to A$, this indeed constitutes an isomorphism, since + \[\pi_1 \comp \langle id_A , !_A \rangle = id_A \] by definition and - \[\langle id_A , !_A \rangle \circ \pi_1 = \langle \pi_1 , !_A \rangle = \langle \pi_1 , \pi_2 \rangle = id_{A \times 1},\] - because $\pi_2 = !_A : A \times 1 \rightarrow 1$ by uniqueness of $!_A$. + \[\langle id_A , !_A \rangle \comp \pi_1 = \langle \pi_1 , !_A \rangle = \langle \pi_1 , \pi_2 \rangle = id_{A \times 1},\] + because $\pi_2 = !_A : A \times 1 \to 1$ by uniqueness of $!_A$. \end{proof} \begin{proposition} - $\times$ is associative, i.e.\ $A \times (B \times C) \cong (A \times B) \times C$ for any $A,B,C \in \obj{\C}$. + $\times$ is associative, i.e.\ $A \times (B \times C) \iso (A \times B) \times C$ for any $A,B,C \in \obj{\CC}$. \end{proposition} \begin{proof} - Take \[\alpha = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : A \times (B \times C) \rightarrow (A \times B) \times C\] - and \[\alpha^{-1} = \langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle : (A \times B) \times C \rightarrow A \times (B \times C).\] + Take \[\alpha = \langle \langle \pi_1 , \pi_1 \comp \pi_2 \rangle , \pi_2 \comp \pi_2 \rangle : A \times (B \times C) \to (A \times B) \times C\] + and \[\alpha^{-1} = \langle \pi_1 \comp \pi_1 , \langle \pi_2 \comp \pi_1 , \pi_2 \rangle \rangle : (A \times B) \times C \to A \times (B \times C).\] The rest of the proof then amounts to simply rewriting. \end{proof} \begin{proposition} - $\times$ is commutative, i.e.\ $A \times B \cong B \times A$ for any $A, B \in \obj{\C}$. + $\times$ is commutative, i.e.\ $A \times B \iso B \times A$ for any $A, B \in \obj{\CC}$. \end{proposition} \begin{proof} - Take \[\langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A\] - and \[\langle \pi_2 , \pi_1 \rangle : B \times A \rightarrow A \times B.\] - Indeed, $\langle \pi_2 , \pi_1 \rangle \circ \langle \pi_2 , \pi_1 \rangle = \langle \pi_2 \circ \langle \pi_2 , \pi_1 \rangle , \pi_1 \circ \langle \pi_2 , \pi_1 \rangle \rangle = \langle \pi_1 , \pi_2 \rangle = id$. + Take \[\langle \pi_2 , \pi_1 \rangle : A \times B \to B \times A\] + and \[\langle \pi_2 , \pi_1 \rangle : B \times A \to A \times B.\] + Indeed, $\langle \pi_2 , \pi_1 \rangle \comp \langle \pi_2 , \pi_1 \rangle = \langle \pi_2 \comp \langle \pi_2 , \pi_1 \rangle , \pi_1 \comp \langle \pi_2 , \pi_1 \rangle \rangle = \langle \pi_1 , \pi_2 \rangle = id$. \end{proof} Duality instantly yields the commutative monoid structure of coproducts: \begin{proposition} - $0$ is the unit of $+$, i.e.\ $A \cong A + 0$ for any $A \in \obj{\C}$. + $0$ is the unit of $+$, i.e.\ $A \iso A + 0$ for any $A \in \obj{\CC}$. \end{proposition} \begin{proposition} - $+$ is associative, i.e.\ $A + (B + C) \cong (A + B) + C$ for any $A,B,C \in \obj{\C}$. + $+$ is associative, i.e.\ $A + (B + C) \iso (A + B) + C$ for any $A,B,C \in \obj{\CC}$. \end{proposition} \begin{proposition} - $+$ is commutative, i.e.\ $A + B \cong B + A$ for any $A, B \in \obj{\C}$. + $+$ is commutative, i.e.\ $A + B \iso B + A$ for any $A, B \in \obj{\CC}$. \end{proposition} \begin{remark} @@ -289,36 +290,36 @@ Duality instantly yields the commutative monoid structure of coproducts: \section{Functors} Functors are morphisms between categories, concretely: \begin{definition}[Functor] - A functor $F : \C \rightarrow \D$ consists of + A functor $F : \CC \to \CD$ consists of \begin{itemize} - \item a mapping $F : \obj{\C} \rightarrow \obj{\D}$ on objects and - \item a mapping $F : \C(A,B) \rightarrow \C(FA,FB)$ on morphisms, + \item a mapping $F : \obj{\CC} \to \obj{\CD}$ on objects and + \item a mapping $F : \CC(A,B) \to \CC(FA,FB)$ on morphisms, \end{itemize} - such that $F(id_A) = id_{FA}$ and $F(g \circ f) = Fg \circ Ff$. + such that $F(id_A) = id_{FA}$ and $F(g \comp f) = Fg \comp Ff$. \end{definition} \begin{example} Usual examples of functors include \begin{enumerate} - \item Constant functors mapping to a single object: $D! : \C \rightarrow \D, D \in \obj{\D}$ with + \item Constant functors mapping to a single object: $D! : \CC \to \CD, D \in \obj{\CD}$ with \[D!(C) = D, \qquad D!(f) = id_D.\] - \item Identity functor: $Id_\C : \C \rightarrow \C$ with - \[Id_\C(C) = C, \qquad Id_\C(f) = f.\] + \item Identity functor: $\Id{}_{\CC} : \CC \to \CC$ with + \[\Id{}_{\CC} (C) = C, \qquad \Id{}_{\CC} (f) = f.\] \item Composition of functors: $(FG)(X) = F(GX), (FG)(f) = F(Gf)$ - \item Square functor on $\emph{Set}$: $Q : \emph{Set} \rightarrow \emph{Set}$ with + \item Square functor on $\Set$: $Q : \Set \to \Set$ with \[QX = X \times X, \qquad Qf = f \times f.\] - \item $list : Set \rightarrow Set$, see \autoref{subsec:lists}. - \item For $A \in \obj{\C}$ there is the hom-functor $\C(A,-) : \C \rightarrow Set$ given by - \[ \C(A,B), \qquad \C(A,f : B \rightarrow B')(h : A \rightarrow B) = f \circ h : \C(A,B').\] - \item Functors between posets are monotonous maps, which in turn are the morphisms in $\emph{Pos}$. - \item Functors between monoids are monoid homomorphisms, which in turn are the morphisms in $\emph{Mon}$. - \item The power set functor $\mathscr{P} : \emph{Set} \rightarrow \emph{Set}$ defined by + \item $list : Set \to Set$, see \autoref{subsec:lists}. + \item For $A \in \obj{\CC}$ there is the hom-functor $\CC(A,\argument) : \CC \to Set$ given by + \[ \CC(A,B), \qquad \CC(A,f : B \to B')(h : A \to B) = f \comp h : \CC(A,B').\] + \item Functors between posets are monotonous maps, which in turn are the morphisms in $\Pos$. + \item Functors between monoids are monoid homomorphisms, which in turn are the morphisms in $\Mon$. + \item The power set functor $\PSet{} : \Set \to \Set$ defined by \begin{alignat*}{2} - & \mathscr{P}X & & = \{ Y\;\vert\; Y \subseteq X \} \\ - & (\mathscr{P}f)Y & & = f[Y] \subseteq X', \text{ for } Y \subseteq X. + & \PSet{}X & & = \{ Y\;\vert\; Y \subseteq X \} \\ + & (\PSet{}f)Y & & = f[Y] \subseteq X', \text{ for } Y \subseteq X. \end{alignat*} - \item If $\C$ is a category that adds some structure to sets (like \emph{Mon} or \emph{Pos}) one usually can construct a \emph{forgetful functor} $U : \C \rightarrow \emph{Set}$, e.g. + \item If $\CC$ is a category that adds some structure to sets (like $\Mon$ or $\Pos$) one usually can construct a \emph{forgetful functor} $U : \CC \to \Set$, e.g. \begin{alignat*}{4} - & U_{\emph{Pos}} : \emph{Pos} & & \rightarrow \emph{Set}; \qquad & & (X, \leq) & & \mapsto X \\ - & U_{\emph{Mon}} : \emph{Mon} & & \rightarrow \emph{Set}; \qquad & & (M, \cdot, e) & & \mapsto M + & U_{\Pos} : \Pos & & \to \Set; \qquad & & (X, \leq) & & \mapsto X \\ + & U_{\Mon} : \Mon & & \to \Set; \qquad & & (M, \cdot, e) & & \mapsto M \end{alignat*} \setcounter{resumeenum}{\value{enumi}} \end{enumerate} @@ -328,34 +329,34 @@ Using functors as morphisms, one can \emph{almost} build a category $\emph{CAT}$ We can however consider structures like products and isomorphisms in the quasi-category $\emph{CAT}$: \begin{definition}[Products of Categories] - The product of two categories $\C, \D$ consists of + The product of two categories $\CC, \CD$ consists of \begin{itemize} - \item $\obj{\C \times \D} = \obj{\C} \times \obj{\D}$, - \item $(\C \times \D)((A_1, A_2),(B_1,B_2)) = \C(A_1, B_1) \times D(A_2, B_2)$, + \item $\obj{\CC \times \CD} = \obj{\CC} \times \obj{\CD}$, + \item $(\CC \times \CD)((A_1, A_2),(B_1,B_2)) = \CC(A_1, B_1) \times D(A_2, B_2)$, \end{itemize} - with projection functors $\pi_1 : \C \times \D \rightarrow \C, \pi_2 : \C \times \D \rightarrow \D$. + with projection functors $\pi_1 : \CC \times \CD \to \CC, \pi_2 : \CC \times \CD \to \CD$. \end{definition} \begin{example} More examples of functors include: \begin{enumerate} \setcounter{enumi}{\value{resumeenum}} - \item The Cartesian product functor: $-\times- : \emph{Set} \times \emph{Set} \rightarrow \emph{Set}$. - \item The binary hom-functor $\C(-,-) : \dual{\C} \times \C \rightarrow \emph{Set}$ with - \[\C(A,B), \qquad \C(g : X' \rightarrow X, f : Y \rightarrow Y')(h : X \rightarrow Y) = f \circ h \circ g : \C(X',Y').\] + \item The Cartesian product functor: $-\times- : \Set \times \Set \to \Set$. + \item The binary hom-functor $\CC(\argument,\argument) : \dual{\CC} \times \CC \to \Set$ with + \[\CC(A,B), \qquad \CC(g : X' \to X, f : Y \to Y')(h : X \to Y) = f \comp h \comp g : \CC(X',Y').\] \setcounter{resumeenum}{\value{enumi}} \end{enumerate} \end{example} \begin{definition}[Covariant and Contravariant Functors] - A functor $F : \dual{\C} \rightarrow \D$ is called a \emph{contravariant} functor $\C \rightarrow \D$. For differentiation, we call `normal' functors $\C \rightarrow \D$ \emph{covariant}. + A functor $F : \dual{\CC} \to \CD$ is called a \emph{contravariant} functor $\CC \to \CD$. For differentiation, we call `normal' functors $\CC \to \CD$ \emph{covariant}. \end{definition} \begin{example} Examples of contravariant functors include: \begin{enumerate} \setcounter{enumi}{\value{resumeenum}} - \item For every $Y \in \obj{\C}$ there is a contravariant hom-functor $\C(-,Y) : \dual{\C} \rightarrow \emph{Set}$ given by - \[\C(X,Y), \qquad \C(f : X' \rightarrow X, Y)(h : X \rightarrow Y) = h \circ f : \C(X', Y).\] - \item $2^{(-)} : \dual{\emph{Set}} \rightarrow \emph{Set}$ where - \[2^X = \{ f : X \rightarrow 2 \} \cong \mathscr{P}X\] + \item For every $Y \in \obj{\CC}$ there is a contravariant hom-functor $\CC(\argument,Y) : \dual{\CC} \to \Set$ given by + \[\CC(X,Y), \qquad \CC(f : X' \to X, Y)(h : X \to Y) = h \comp f : \CC(X', Y).\] + \item $2^{(\argument)} : \dual{\Set} \to \Set$ where + \[2^X = \{ f : X \to 2 \} \iso \PSet{}X\] and - \[2^{(f : X \rightarrow Y)} : 2^Y \rightarrow 2^X \cong \mathscr{P}Y \rightarrow \mathscr{P}X, \qquad Z \mapsto \{ x \;\vert\; fx \in Z \} = f^{-1}[Z] \subseteq X.\] - \item For every functor $F : \C \rightarrow \D$ the identical functor $\dual{F} : \dual{\C} \rightarrow \dual{\D}$, given by + \[2^{(f : X \to Y)} : 2^Y \to 2^X \iso \PSet{}Y \to \PSet{}X, \qquad Z \mapsto \{ x \;\vert\; fx \in Z \} = f^{-1}[Z] \subseteq X.\] + \item For every functor $F : \CC \to \CD$ the identical functor $\dual{F} : \dual{\CC} \to \dual{\CD}$, given by \[\dual{F}C = FC, \qquad \dual{F}f = Ff.\] \end{enumerate} \end{example} @@ -363,26 +364,26 @@ We can however consider structures like products and isomorphisms in the quasi-c Isomorphisms of categories are the isomorphisms in the quasi-category $\emph{CAT}$, thus a functor is an isomorphism iff he is bijective on both objects and morphisms. However, oftentimes categories are not isomorphic but instead \emph{equivalent} in the following sense: \begin{definition}[Equivalence Functors] - A functor $F : \C \rightarrow \D$ is called + A functor $F : \CC \to \CD$ is called \begin{itemize} - \item \emph{full} if every $F : \C(A,B) \rightarrow \D(FA,FB)$ is surjective, - \item \emph{faithful} if every $F : \C(A,B) \rightarrow \D(FA,FB)$ is injective, - \item \emph{essentially surjective (dense)} if for every $D \in \D$ there exists a $C \in \C$ such that $D \cong FC$, + \item \emph{full} if every $F : \CC(A,B) \to \CD(FA,FB)$ is surjective, + \item \emph{faithful} if every $F : \CC(A,B) \to \CD(FA,FB)$ is injective, + \item \emph{essentially surjective (dense)} if for every $D \in \CD$ there exists a $C \in \CC$ such that $D \iso FC$, \item an \emph{equivalence} if $F$ is full, faithful and dense. \end{itemize} \end{definition} \begin{example} Let us consider two examples of equivalent categories: \begin{enumerate} - \item The category $\emph{Par}$ is equivalent to $\emph{Set}_p$, which is the category of pointed sets, where objects are tuples $(X,p), p \in X$ and morphisms are point-preserving. - \item The product category $\emph{Set} \times \emph{Set}$ is equivalent to the \emph{slice category} $\emph{Set}/2$, where objects are maps $X \rightarrow 2$ and morphisms $h : (X \overset{f}{\rightarrow} 2) \rightarrow (Y \overset{g}{\rightarrow} 2)$ are maps $h : X \rightarrow Y$ such that $g \circ h = f$. + \item The category $\Par$ is equivalent to $\Set_p$, which is the category of pointed sets, where objects are tuples $(X,p), p \in X$ and morphisms are point-preserving. + \item The product category $\Set \times \Set$ is equivalent to the \emph{slice category} $\Set/2$, where objects are maps $X \to 2$ and morphisms $h : (X \overset{f}{\to} 2) \to (Y \overset{g}{\to} 2)$ are maps $h : X \to Y$ such that $g \comp h = f$. \end{enumerate} \end{example} \section{Natural Transformations} Natural transformation are morphisms between functors. The definition of ``naturality'' was one of the original goals of category theory. \begin{definition}[Natural Transformation] - Given two functors $F, G : \C \rightarrow \D$. - A natural transformation $\alpha : F \rightarrow G$ between these functors is a family of morphisms $(\alpha_C : FC \rightarrow GC)_{C\in\obj{\C}}$, such that for any $f : A \rightarrow B$ the diagram + Given two functors $F, G : \CC \to \CD$. + A natural transformation $\alpha : F \to G$ between these functors is a family of morphisms \[{(\alpha_C : FC \to GC)}_{C\in\obj{\CC}},\] such that for any $f : A \to B$ the diagram % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFsyLDAsIkZCIl0sWzAsMiwiR0EiXSxbMiwyLCJHQiJdLFswLDEsIkZmIl0sWzIsMywiR2YiXSxbMCwyLCJcXGFscGhhX0EiLDJdLFsxLDMsIlxcYWxwaGFfQiJdXQ== \[ \begin{tikzcd} @@ -400,7 +401,7 @@ Natural transformation are morphisms between functors. The definition of ``natur \begin{example} Examples of natural transformations include: \begin{enumerate} - \item The obvious function $flatten : Tree\;A \rightarrow List\;A$: + \item The obvious function $flatten : Tree\;A \to List\;A$: % https://q.uiver.app/#q=WzAsNCxbMCwwLCJUcmVlXFw7QSJdLFsyLDAsIlRyZWVcXDtCIl0sWzAsMiwiTGlzdFxcO0EiXSxbMiwyLCJMaXN0XFw7QiJdLFswLDIsImZsYXR0ZW5fQSIsMl0sWzEsMywiZmxhdHRlbl9CIl0sWzIsMywibGlzdFxcO2YiXSxbMCwxLCJ0cmVlXFw7ZiJdXQ== \[ \begin{tikzcd} @@ -413,18 +414,18 @@ Natural transformation are morphisms between functors. The definition of ``natur \arrow["{tree\;f}", from=1-1, to=1-3] \end{tikzcd} \] - \item For $Id, Q : Set \rightarrow Set$ we have $\delta : Id \rightarrow Q$ given by $\delta_X (x) = (x,x)$. - \item On $\mathcal{P}$ we can define natural transformations $\eta : Id \rightarrow \mathcal{P}$ and $\mu : \mathcal{P}\mathcal{P} \rightarrow \mathcal{P}$ by: + \item For $\Id{}, Q : Set \to Set$ we have $\delta : \Id{} \to Q$ given by $\delta_X (x) = (x,x)$. + \item On $\mathcal{P}$ we can define natural transformations $\eta : \Id{} \to \mathcal{P}$ and $\mu : \mathcal{P}\mathcal{P} \to \mathcal{P}$ by: \begin{alignat*}{1} - \eta_X : X & \rightarrow \mathcal{P}X \\ + \eta_X : X & \to \mathcal{P}X \\ x & \mapsto \{x\} \end{alignat*} and \begin{alignat*}{1} - \mu_X : \mathcal{P}\mathcal{P}X & \rightarrow \mathcal{P}X \\ + \mu_X : \mathcal{P}\mathcal{P}X & \to \mathcal{P}X \\ Z & \mapsto \bigcup Z. \end{alignat*} - \item Between $Q$ and $\mathcal{P}$ we can consider $\alpha,\beta : Q \rightarrow \mathcal{P}$ given by + \item Between $Q$ and $\mathcal{P}$ we can consider $\alpha,\beta : Q \to \mathcal{P}$ given by \begin{alignat*}{2} & \alpha_X(x,y) & & = \{x,y\} \\ & \beta_X(x,y) & & = \{x\}. @@ -432,12 +433,12 @@ Natural transformation are morphisms between functors. The definition of ``natur \end{enumerate} \end{example} -Functors $\C \rightarrow \D$ together with natural transformations as morphisms form a quasi-category $[\C,\D]$, that is called the functor category. If $\C$ is small, then $[\C,\D]$ is a category, where identity and composition are defined component wise. +Functors $\CC \to \CD$ together with natural transformations as morphisms form a quasi-category $[\CC,\CD]$, that is called the functor category. If $\CC$ is small, then $[\CC,\CD]$ is a category, where identity and composition are defined component wise. \begin{example} Let us examine concrete examples of functor categories: \begin{enumerate} - \item $[2, \C] \cong \C \times \C$, where $2$ is the \emph{discrete} category with two objects, i.e.\ $2$ has no morphisms besides the identities. - \item Let $\rightarrow$ be the category with 2 objects and a single non-trivial morphism $m$. $[\rightarrow, \C$ is the \emph{category of morphisms} of $\C$, where morphisms $Fm \rightarrow Gm$ are pairs of morphisms $(f,g)$ where + \item $[2, \CC] \iso \CC \times \CC$, where $2$ is the \emph{discrete} category with two objects, i.e.\ $2$ has no morphisms besides the identities. + \item Let $\to$ be the category with 2 objects and a single non-trivial morphism $m$. $[\to, \CC]$ is the \emph{category of morphisms} of $\CC$, where morphisms $Fm \to Gm$ are pairs of morphisms $(f,g)$ where % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGMCJdLFsyLDAsIkYxIl0sWzAsMiwiRzAiXSxbMiwyLCJHMSJdLFswLDEsIkZtIl0sWzIsMywiR20iXSxbMCwyLCJmIiwyXSxbMSwzLCJnIl1d \[ \begin{tikzcd} @@ -455,46 +456,305 @@ Functors $\C \rightarrow \D$ together with natural transformations as morphisms \end{example} \begin{definition}[Natural Isomorphism] - Isomorphisms in $[\C,\D]$ are called \emph{natural isomorphisms}. + Isomorphisms in $[\CC,\CD]$ are called \emph{natural isomorphisms}. \end{definition} \begin{proposition} - $\alpha : F \rightarrow G$ is a natural isomorphism \emph{iff} every $\alpha_C$ is an isomorphism. + $\alpha : F \to G$ is a natural isomorphism \emph{iff} every $\alpha_C$ is an isomorphism. \end{proposition} \begin{example} Let us consider some examples of natural isomorphisms: \begin{enumerate} - \item In $[\emph{Set},\emph{Set}]$ is $Id \cong \emph{Set}(1,-)$, since of course $Id\;X = X \cong X^1 = \emph{Set}(1,X)$. - \item Also in $[\emph{Set},\emph{Set}]$ is $Q \cong \emph{Set}(2,-)$, similarly is $\lambda X.2\times X \cong \lambda X. X + X$. - \item The forgetful functor $U : \emph{Pos} \rightarrow \emph{Set}$ is naturally isomorphic to $\emph{Pos}(1,-)$, because the constant mapping $x : 1 \rightarrow X$ is monotonous for every element $x$ of a poset. + \item In $[\Set,\Set]$ is $\Id{} \iso \Set(1,\argument)$, since of course $\Id{}\;X = X \iso X^1 = \Set(1,X)$. + \item Also in $[\Set,\Set]$ is $Q \iso \Set(2,\argument)$, similarly is $\lambda X.2\times X \iso \lambda X. X + X$. + \item The forgetful functor $U : \Pos \to \Set$ is naturally isomorphic to $\Pos(1,\argument)$, because the constant mapping $x : 1 \to X$ is monotonous for every element $x$ of a poset. \end{enumerate} \end{example} \begin{proposition}[Yoneda Lemma] - Let $A \in \obj{\C}$ and $G : \C \rightarrow \emph{Set}$. Then the natural transformations - \[\C(A,-) \rightarrow G\] + Let $A \in \obj{\CC}$ and $G : \CC \to \Set$. Then the natural transformations + \[\CC(A,\argument) \to G\] are in bijection with the elements of the set $GA$. + In other words + \[[\CC , \Set ](\CC(A,\argument), G) \iso GA \] \end{proposition} \begin{proof} The mappings are \begin{alignat*}{1} - & Z : GA \rightarrow [\C , \emph{Set}](\C(A,-), G) \\ + & Z : GA \to [\CC , \Set](\CC(A,\argument), G) \\ & Z\;x\;h = G\;h\;x \end{alignat*} and \begin{alignat*}{1} - & Y : [\C , \emph{Set}](\C(A,-), G) \rightarrow GA \\ - & Y\;\alpha = \alpha_A\;id_A + & Y : [\CC , \Set](\CC(A,\argument), G) \to GA \\ + & Y\;\alpha = \alpha_A\;id_A. \end{alignat*} + + We are left to check naturality of $Z\;x$ and that indeed $Z$ and $Y$ are inverse to each other, all of which follows by routine rewriting. \end{proof} \begin{example} - Let us consider an application of the Yoneda Lemma: how many natural transformations $Id \rightarrow Q$ are there? - Recall that $Id \cong \emph{Set}(1,-)$, and by Yoneda there is exactly $\vert Q1 \vert = 1$ natural transformation $\emph{Set}(1,-) \rightarrow Q$, thus the number of natural transformations $Id \rightarrow Q$ is $1$. + Let us consider an application of the Yoneda Lemma: how many natural transformations $\Id{} \to Q$ are there? + Recall that $\Id{} \iso \Set(1,\argument)$, and by Yoneda there is exactly $\vert Q1 \vert = 1$ natural transformation $\Set(1,\argument) \to Q$, thus the number of natural transformations $\Id{} \to Q$ is $1$. - Furthermore, consider the number of natural transformations $Q \rightarrow Q$. Recall that $Q \cong \emph{Set}(2, -)$, and by Yoneda there are $\vert Q2 \vert = 4$ natural transformations $\emph{Set}(2, -) \rightarrow Q$, thus the number of natural transformations $Q \rightarrow Q$ is $4$. + Furthermore, consider the number of natural transformations $Q \to Q$. Recall that $Q \iso \Set(2, \argument)$, and by Yoneda there are $\vert Q2 \vert = 4$ natural transformations $\Set(2, \argument) \to Q$, thus the number of natural transformations $Q \to Q$ is $4$. \end{example} \section{Functor Algebras} +Recall the fold functions that we introduced in \autoref{chp:introduction} in the category $\Set$: +\begin{alignat*}{5} + & & foldn : \; & (1 \to C) \to (C \to C) & & \to Nat & & \to C \\ + & & foldr : \; & (1 \to C) \to (A \times C \to C) & & \to List\;A & & \to C +\end{alignat*} +These are examples of special \emph{F-algebras} in $\Set$. In this section we will introduce this notion and examine what makes the fold functions special. + +\begin{definition}[F-Algebras] + Let $F : \CC \to \CC$ be an endofunctor on $\CC$. An \emph{F-algebra} is a pair $(A \in \obj{\CC}, a : FA \to a)$. Homomorphisms between F-algebras $(A,a)$ and $(B,b)$ are morphisms $f : A \to B$ such that + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFswLDIsIkZCIl0sWzIsMCwiQSJdLFsyLDIsIkIiXSxbMSwzLCJiIl0sWzAsMiwiYSJdLFswLDEsIkZmIiwyXSxbMiwzLCJmIl1d + \[ + \begin{tikzcd} + FA && A \\ + \\ + FB && B + \arrow["b", from=3-1, to=3-3] + \arrow["a", from=1-1, to=1-3] + \arrow["Ff"', from=1-1, to=3-1] + \arrow["f", from=1-3, to=3-3] + \end{tikzcd} + \] + commutes. +\end{definition} + +\begin{proposition} + F-algebras together with their homomorphisms form a category that we call $\Alg{F}$. +\end{proposition} +\begin{proof} + Identities and composition are inherited by the underlying category $\CC$. We are left to show that the identities are homomorphisms: + % https://q.uiver.app/#q=WzAsNSxbMCwwLCJGQSJdLFswLDIsIkZBIl0sWzIsMCwiQSJdLFsyLDIsIkEiXSxbMSwxLCJcXGNvbW0iXSxbMSwzLCJhIl0sWzAsMiwiYSJdLFswLDEsIkZpZCIsMl0sWzIsMywiaWQiXV0= + \[ + \begin{tikzcd} + FA && A \\ + & \comm \\ + FA && A + \arrow["a", from=3-1, to=3-3] + \arrow["a", from=1-1, to=1-3] + \arrow["Fid"', from=1-1, to=3-1] + \arrow["id", from=1-3, to=3-3] + \end{tikzcd} + \] + and that homomorphisms are closed under composition: + % https://q.uiver.app/#q=WzAsOCxbMCwwLCJGQSJdLFswLDIsIkZCIl0sWzIsMCwiQSJdLFsyLDIsIkIiXSxbMSwxLCJcXGNvbW0iXSxbMCw0LCJGQyJdLFsyLDQsIkMiXSxbMSwzLCJcXGNvbW0iXSxbMSwzLCJiIl0sWzAsMiwiYSJdLFswLDEsIkZmIiwyXSxbMiwzLCJmIl0sWzUsNiwiYyJdLFsxLDUsIkZnIiwyXSxbMyw2LCJnIl0sWzAsNSwiRihnIFxcY2lyYyBmKSIsMix7ImN1cnZlIjo0fV0sWzIsNiwiZyBcXGNpcmMgZiIsMCx7ImN1cnZlIjotNH1dXQ== + \[ + \begin{tikzcd} + FA && A \\ + & \comm \\ + FB && B \\ + & \comm \\ + FC && C + \arrow["b", from=3-1, to=3-3] + \arrow["a", from=1-1, to=1-3] + \arrow["Ff"', from=1-1, to=3-1] + \arrow["f", from=1-3, to=3-3] + \arrow["c", from=5-1, to=5-3] + \arrow["Fg"', from=3-1, to=5-1] + \arrow["g", from=3-3, to=5-3] + \arrow["{F(g \circ f)}"', curve={height=24pt}, from=1-1, to=5-1] + \arrow["{g \circ f}", curve={height=-24pt}, from=1-3, to=5-3] + \end{tikzcd} + \] +\end{proof} + +\begin{example}\label{ex:Falg} Let us now consider the structure of the data types Nat and List as F-algebras: + \begin{enumerate} + \item \textbf{Nat}: Take $\CC = \Set$ and $FX = 1 + X$, the F-algebras and their morphisms have the following form: + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgQSJdLFsyLDAsIkEiXSxbMCwyLCIxICsgQiJdLFsyLDIsIkIiXSxbMCwxLCJbYyxoXSJdLFsyLDMsIltjJywgaCddIl0sWzAsMiwiXFxiYW5nICsgZiIsMl0sWzEsMywiZiJdXQ== + \[ + \begin{tikzcd} + {1 + A} && A \\ + \\ + {1 + B} && B + \arrow["{[c,h]}", from=1-1, to=1-3] + \arrow["{[c', h']}", from=3-1, to=3-3] + \arrow["{\bang + f}"', from=1-1, to=3-1] + \arrow["f", from=1-3, to=3-3] + \end{tikzcd} + \] + Which is equivalent to: + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJBIl0sWzQsMCwiQSJdLFsyLDIsIkIiXSxbNCwyLCJCIl0sWzAsMCwiMSJdLFs0LDAsImMiXSxbMCwxLCJoIl0sWzIsMywiaCciXSxbNCwyLCJjJyIsMl0sWzAsMiwiZiIsMl0sWzEsMywiZiJdXQ== + \[ + \begin{tikzcd} + 1 && A && A \\ + \\ + && B && B + \arrow["c", from=1-1, to=1-3] + \arrow["h", from=1-3, to=1-5] + \arrow["{h'}", from=3-3, to=3-5] + \arrow["{c'}"', from=1-1, to=3-3] + \arrow["f"', from=1-3, to=3-3] + \arrow["f", from=1-5, to=3-5] + \end{tikzcd} + \] + \item \textbf{List\;A}: Take $\CC = \Set$ and $FX = 1 + A \times X$, where $A \in \obj{\Set}$. The F-algebras and their morphisms take the following form: + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgQSBcXHRpbWVzIFgiXSxbMCwyLCIxICsgQSBcXHRpbWVzIFkiXSxbMiwwLCJYIl0sWzIsMiwiWSJdLFswLDIsIltjLGhdIl0sWzEsMywiW2MsaF0iXSxbMiwzLCJmIl0sWzAsMSwiXFxiYW5nICsgaWQgXFx0aW1lcyBmIiwyXV0= + \[ + \begin{tikzcd} + {1 + A \times X} && X \\ + \\ + {1 + A \times Y} && Y + \arrow["{[c,h]}", from=1-1, to=1-3] + \arrow["{[c,h]}", from=3-1, to=3-3] + \arrow["f", from=1-3, to=3-3] + \arrow["{\bang + id \times f}"', from=1-1, to=3-1] + \end{tikzcd} + \] + Which again is equivalent to + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJBIFxcdGltZXMgWCJdLFsyLDIsIkEgXFx0aW1lcyBZIl0sWzQsMCwiWCJdLFs0LDIsIlkiXSxbMCwwLCIxIl0sWzAsMiwiaCJdLFsxLDMsImgiXSxbMiwzLCJmIl0sWzAsMSwiaWQgXFx0aW1lcyBmIiwyXSxbNCwwLCJjIl0sWzQsMSwiYyciLDJdXQ== + \[ + \begin{tikzcd} + 1 && {A \times X} && X \\ + \\ + && {A \times Y} && Y + \arrow["h", from=1-3, to=1-5] + \arrow["h", from=3-3, to=3-5] + \arrow["f", from=1-5, to=3-5] + \arrow["{id \times f}"', from=1-3, to=3-3] + \arrow["c", from=1-1, to=1-3] + \arrow["{c'}"', from=1-1, to=3-3] + \end{tikzcd} + \] + \end{enumerate} +\end{example} + +\subsection{Initial F-algebras} + +\emph{Initial F-algebras} (i.e.\ the initial object in $\Alg{F}$) are of special interest to us. More concretely an F-algebra $(I, i)$ is initial if for every $(A, a)$ there exists a unique $\cata{a} : I \to A$ such that +% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGSSJdLFsyLDAsIkkiXSxbMCwyLCJGQSJdLFsyLDIsIkEiXSxbMCwxLCJpIl0sWzAsMiwiRlxcY2F0YXthfSIsMl0sWzEsMywiXFxleGlzdHMhXFxjYXRhe2F9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiYSIsMl1d +\[ + \begin{tikzcd} + FI && I \\ + \\ + FA && A + \arrow["i", from=1-1, to=1-3] + \arrow["{F\cata{a}}"', from=1-1, to=3-1] + \arrow["{\exists!\cata{a}}", dashed, from=1-3, to=3-3] + \arrow["a"', from=3-1, to=3-3] + \end{tikzcd} +\] +commutes. + +The dual notion of \emph{terminal F-algebra} is usually not of interested, since it is just inherited from $\CC$: +% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFsyLDAsIkEiXSxbMCwyLCJGMSJdLFsyLDIsIjEiXSxbMiwzLCIhIl0sWzAsMSwiYSJdLFswLDIsIkYhIiwyXSxbMSwzLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d +\[ + \begin{tikzcd} + FA && A \\ + \\ + F1 && 1 + \arrow["{!}", from=3-1, to=3-3] + \arrow["a", from=1-1, to=1-3] + \arrow["{F!}"', from=1-1, to=3-1] + \arrow["{!}", dashed, from=1-3, to=3-3] + \end{tikzcd} +\] + +\begin{example} + Important examples of initial F-algebras include: + \begin{enumerate} + \item In \autoref{ex:Falg} (1) the data type $Nat$ is the initial algebra together with the function $foldn$ that we defined in the introduction. Where the following diagram expresses the defining equations for $foldn$: + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgTmF0Il0sWzAsMiwiMSArIEMiXSxbMiwwLCJOYXQiXSxbMiwyLCJDIl0sWzAsMSwiISArZm9sZG4oYyxoKSIsMl0sWzAsMiwiW3plcm8sIHN1Y2NdIl0sWzIsMywiZm9sZG4oYyxoKSJdLFsxLDMsIltjLGhdIiwyXV0= + \[ + \begin{tikzcd} + {1 + Nat} && Nat \\ + \\ + {1 + C} && C + \arrow["{id +foldn(c,h)}"', from=1-1, to=3-1] + \arrow["{[zero, succ]}", from=1-1, to=1-3] + \arrow["{foldn(c,h)}", from=1-3, to=3-3] + \arrow["{[c,h]}"', from=3-1, to=3-3] + \end{tikzcd} + \] + \item Similarly, in \autoref{ex:Falg} (2) the data type $List\;A$ is the initial algebra: + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgQSBcXHRpbWVzIExpc3RcXDtBIl0sWzIsMCwiTGlzdFxcO0EiXSxbMCwyLCIxICsgQSBcXHRpbWVzIEMiXSxbMiwyLCJDIl0sWzAsMSwiW25pbCxjb25zXSJdLFsyLDMsIltjLGhdIl0sWzEsMywiZm9sZHIoYyxoKSJdLFswLDIsImlkICsgZm9sZHIoYyxoKSIsMl1d + \[ + \begin{tikzcd} + {1 + A \times List\;A} && {List\;A} \\ + \\ + {1 + A \times C} && C + \arrow["{[nil,cons]}", from=1-1, to=1-3] + \arrow["{[c,h]}", from=3-1, to=3-3] + \arrow["{foldr(c,h)}", from=1-3, to=3-3] + \arrow["{id + foldr(c,h)}"', from=1-1, to=3-1] + \end{tikzcd} + \] + % TODO add other examples + \end{enumerate} +\end{example} + +We can now abstract the fusion and identity laws that we defined for each data type in \autoref{sec:datatypes}: + +\begin{proposition} + Let $(I,i)$ be an initial F-algebra. The following holds: + \begin{enumerate} + \item \customlabel{law:ident}{\textbf{Identity}}: $\cata{i} = id_I : I \to I$, + \item \customlabel{law:fusion}{\textbf{Fusion}}: Let $f : (A,a) \to (B,b)$ be a homomorphism between F-algebras, then + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJJIl0sWzIsMCwiQSJdLFsyLDIsIkIiXSxbMCwxLCJcXGNhdGF7YX0iXSxbMSwyLCJmIl0sWzAsMiwiXFxjYXRhe2J9IiwyXV0= + \[ + \begin{tikzcd} + I && A \\ + \\ + && B + \arrow["{\cata{a}}", from=1-1, to=1-3] + \arrow["f", from=1-3, to=3-3] + \arrow["{\cata{b}}"', from=1-1, to=3-3] + \end{tikzcd} + \] + commutes. + \end{enumerate} +\end{proposition} +\begin{proof} Both follow by uniqueness of homomorphisms out of the initial object: + \begin{enumerate} + \item By uniqueness of homomorphisms $(I,i) \to (I,i)$ + \item By uniqueness of homomorphisms $(I,i) \to (B,b)$ + \end{enumerate} +\end{proof} + +\begin{proposition}[Lambeks Lemma] + Let $(I,i)$ be an initial F-algebra. The F-algebra structure $i$ is an isomorphism. +\end{proposition} +\begin{proof} + Applying $F$ on $i$ yields another F-algebra $(FI, Fi)$, which induces a homomorphism $\cata{Fi} : I \rightarrow FI$. $\cata{FI}$ is the inverse to $i$. Consider + % https://q.uiver.app/#q=WzAsOCxbMCwwLCJGSSJdLFsyLDAsIkkiXSxbMiwyLCJGSSJdLFswLDIsIkZGSSJdLFsxLDEsIlxcY29tbSJdLFswLDQsIkZJIl0sWzIsNCwiSSJdLFsxLDMsIlxcY29tbSJdLFswLDEsImkiXSxbMywyLCJGaSJdLFswLDMsIkZcXGNhdGF7Rml9Il0sWzEsMiwiXFxjYXRhe0ZpfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDYsImkiXSxbMyw1LCJGaSJdLFsyLDYsImkiLDJdLFswLDUsIkYoaSBcXGNvbXAgXFxjYXRhe0ZpfSkiLDIseyJjdXJ2ZSI6M31dLFsxLDYsImkgXFxjb21wIFxcY2F0YXtGaX0iLDAseyJjdXJ2ZSI6LTN9XV0= + \[ + \begin{tikzcd} + FI && I \\ + & \comm \\ + FFI && FI \\ + & \comm \\ + FI && I + \arrow["i", from=1-1, to=1-3] + \arrow["Fi", from=3-1, to=3-3] + \arrow["{F\cata{Fi}}", from=1-1, to=3-1] + \arrow["{\cata{Fi}}"', dashed, from=1-3, to=3-3] + \arrow["i", from=5-1, to=5-3] + \arrow["Fi", from=3-1, to=5-1] + \arrow["i"', from=3-3, to=5-3] + \arrow["{F(i \comp \cata{Fi})}"', curve={height=18pt}, from=1-1, to=5-1] + \arrow["{i \comp \cata{Fi}}", curve={height=-18pt}, from=1-3, to=5-3] + \end{tikzcd} + \] + from which we can follow that $i \comp \cata{Fi} = id_I : (I,i) \to (I,i)$ by uniqueness of the homomorphisms and thus also + \[\cata{Fi} \comp i = Fi \comp F\cata{Fi} = F(i \comp \cata{Fi}) = F {id}_I = {id}_{FI}.\] +\end{proof} + +\subsection{Term Algebras} +% TODO + +\subsection{Parametric Data Types} +% TODO + \section{Functor Coalgebras} -\section{(co)Limits} % chktex 36 \ No newline at end of file +% TODO coalgebras + +\subsection{Terminal F-Coalgebras} +\subsection{Corecursion and Coinduction} +\section{Limits} +\section{Colimits} \ No newline at end of file