Work on limits

tex/sections/02_categories.tex

@@ -980,4 +980,138 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
 \end{example}
 
 \section{Limits}
-\section{Colimits}
+Limits are an abstraction of products and many other categorical concepts.
+\begin{definition}[Limit] We will need to introduce some related notions first.
+  \begin{enumerate}
+    \item A \emph{diagram} in $\CC$ is a functor $D : \CD \to \CC$, where $\CD$ is small.
+    \item A \emph{cone} of a diagram $D : \CD \to \CC$ consists of
+          \begin{itemize}
+            \item an object $C \in \obj{\CC}$ called the \emph{apex} and
+            \item a family of morphisms ${(f_d : C \to Dd)}_{d\in\obj{\CD}}$ such that
+                  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJDIl0sWzAsMiwiRGQiXSxbMiwyLCJEZCciXSxbMCwxLCJmX2QiLDJdLFswLDIsImZfe2QnfSJdLFsxLDIsInUiXV0=
+                  \[\begin{tikzcd}
+                      C \\
+                      \\
+                      Dd && {Dd'}
+                      \arrow["{f_d}"', from=1-1, to=3-1]
+                      \arrow["{f_{d'}}", from=1-1, to=3-3]
+                      \arrow["u", from=3-1, to=3-3]
+                    \end{tikzcd}\]
+                  commutes for every $u : d \to d'$.
+          \end{itemize}
+    \item A \emph{limit} of a diagram $D$ is a universal cone, i.e.\ a cone $(L, out_d)$ such that for every cone $(C, f_d)$ there exists a unique morphism $h : C \to L$ such that $out_d \comp h = f_d$ for all $d \in \obj{\CD}$:
+          % https://q.uiver.app/#q=WzAsMyxbMiwwLCJMIl0sWzIsMiwiRGQiXSxbMCwwLCJDIl0sWzAsMSwib3V0X2QiXSxbMiwwLCJoIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMSwiZl9kIiwyXV0=
+          \[\begin{tikzcd}
+              C && L \\
+              \\
+              && Dd
+              \arrow["{out_d}", from=1-3, to=3-3]
+              \arrow["h", dashed, from=1-1, to=1-3]
+              \arrow["{f_d}"', from=1-1, to=3-3]
+            \end{tikzcd}\]
+  \end{enumerate}
+\end{definition}
+
+The notion of limit can be instantiated to many interesting notions:
+
+\begin{definition}[Products (as limits)]
+  Let $\CD$ be the discrete category with 2 elements. Diagrams $D$ are pairs $(A,B)$ of objects of $\CC$, cones are pairs of morphisms
+  \[A \overset{f}{\longleftarrow} C \overset{g}{\longrightarrow} B\]
+  and limits of such diagrams are exactly products:
+  \[A \overset{\fst}{\longleftarrow} A\times B \overset{\snd}{\longrightarrow} B.\]
+\end{definition}
+
+\begin{definition}[Equalizer]
+  Let $\CD$ be a category with two non-trivial and parallel morphisms $u,v : 1 \to 2$. Diagrams are parallel morphisms
+  % https://q.uiver.app/#q=WzAsMixbMCwwLCJBXzEiXSxbMiwwLCJBXzIiXSxbMCwxLCJmIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImciLDIseyJvZmZzZXQiOjF9XV0=
+  \[\begin{tikzcd}
+      {A_1} && {A_2}
+      \arrow["f", shift left, from=1-1, to=1-3]
+      \arrow["g"', shift right, from=1-1, to=1-3]
+    \end{tikzcd}\]
+  and cones are pairs of morphisms $c : C \to A_1, d C \to A_2$, such that $f \comp c = d = g \comp c$:
+  % https://q.uiver.app/#q=WzAsMyxbMCwyLCJBXzEiXSxbMiwyLCJBXzIiXSxbMCwwLCJDIl0sWzAsMSwiZiIsMCx7Im9mZnNldCI6LTF9XSxbMCwxLCJnIiwyLHsib2Zmc2V0IjoxfV0sWzIsMCwiYyIsMl0sWzIsMSwiZCJdXQ==
+  \[\begin{tikzcd}
+      C \\
+      \\
+      {A_1} && {A_2}
+      \arrow["f", shift left, from=3-1, to=3-3]
+      \arrow["g"', shift right, from=3-1, to=3-3]
+      \arrow["c"', from=1-1, to=3-1]
+      \arrow["d", from=1-1, to=3-3]
+    \end{tikzcd}\]
+  A limit of such a diagram is called an \emph{equalizer} of $f$ and $g$:
+  % https://q.uiver.app/#q=WzAsNCxbMiwyLCJBXzEiXSxbNCwyLCJBXzIiXSxbMiwwLCJDIl0sWzAsMiwiRSJdLFswLDEsImYiLDAseyJvZmZzZXQiOi0xfV0sWzAsMSwiZyIsMix7Im9mZnNldCI6MX1dLFsyLDAsIlxcZm9yYWxsIGMiLDJdLFsyLDEsImQiXSxbMywwLCJlIl0sWzIsMywiXFxleGlzdHMhaCIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
+  \[\begin{tikzcd}
+      && C \\
+      \\
+      E && {A_1} && {A_2}
+      \arrow["f", shift left, from=3-3, to=3-5]
+      \arrow["g"', shift right, from=3-3, to=3-5]
+      \arrow["{\forall c}"', from=1-3, to=3-3]
+      \arrow["d", from=1-3, to=3-5]
+      \arrow["e", from=3-1, to=3-3]
+      \arrow["{\exists!h}"', dashed, from=1-3, to=3-1]
+    \end{tikzcd}\]
+\end{definition}
+
+% TODO equalizer in Set
+% \begin{example}
+%   In $\Set$...
+% \end{example}
+
+\begin{definition}[Regular Monomorphism]
+  A monomorphism is called \emph{regular} if it is also an equalizer.
+\end{definition}
+
+\begin{proposition}
+  Every equalizer is a monomorphism and thus a regular monomorphism.
+\end{proposition}
+\begin{proof}
+  % TODO prove that eq are mono.
+\end{proof}
+
+\begin{proposition}
+  $e$ is a regular monomorphism and an epimorphism $\iff$ e is an isomorphism.
+\end{proposition}
+\begin{proof}
+  % TODO prove that regular mono + epi == iso
+\end{proof}
+
+\begin{definition}[Pullback]
+  % TODO pullback
+\end{definition}
+% TODO pullback in Set
+% \begin{example}
+%   In $\Set$...
+% \end{example}
+
+\begin{proposition}
+  Limits are unique up to isomorphism.
+\end{proposition}
+
+\begin{definition}[Complete Category]
+  A category $\CC$ is called \emph{complete} if every diagram in $\CC$ has a limit.
+\end{definition}
+
+\begin{proposition}
+  $\CC$ is complete iff $\CC$ has all products and equalizers, i.e.\ using products and equalizer one can construct arbitrary limits.
+\end{proposition}
+
+\begin{definition}[Finitely Complete Category]
+  A category $\CC$ is called \emph{finitely complete} if every finite diagram in $\CC$ has a limit.
+\end{definition}
+
+\begin{proposition}
+  The following are equivalent:
+  \begin{enumerate}
+    \item $\CC$ is finitely complete
+    \item $\CC$ has finite products and equalizers
+    \item $\CC$ has finite products and pullbacks
+    \item $\CC$ has a terminal object and pullbacks
+  \end{enumerate}
+\end{proposition}
+
+
+\section{Colimits}
+% TODO colimits