CategoryTheory/algprog
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Work on colimits

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-31 12:54:31 +02:00
parent 5bae77ae05
commit 78cd9676f4
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 182 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tex/.vscode/ltex.dictionary.en-US.txt vendored
View file

@ -62,3 +62,9 @@ colimits
colimit
finitary
Finitary
cocone
cocones
Cocones
coequalizer
coequalizers
pushouts

BIN
tex/main.pdf
View file

Binary file not shown.

194
tex/sections/02_categories.tex
View file

@ -979,7 +979,7 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
% TODO example proof, needs some interesting functions introduced earlier.
\end{example}
\section{Limits}
\section{Limits}\label{sec:limit}
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}
@ -988,40 +988,40 @@ Limits are an abstraction of products and many other categorical concepts.
\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=
% https://q.uiver.app/#q=WzAsMyxbMSwwLCJDIl0sWzAsMiwiRGQiXSxbMiwyLCJEZCciXSxbMCwxLCJmX2QiLDJdLFswLDIsImZfe2QnfSJdLFsxLDIsIkR1Il1d
\[\begin{tikzcd}
C \\
& 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]
\arrow["{f_d}"', from=1-2, to=3-1]
\arrow["{f_{d'}}", from=1-2, to=3-3]
\arrow["Du", 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=
\item A \emph{limit} of a diagram $D$ is a terminal 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=WzAsMyxbMiwwLCJMIl0sWzEsMiwiRGQiXSxbMCwwLCJDIl0sWzAsMSwib3V0X2QiXSxbMiwwLCJoIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMSwiZl9kIiwyXV0=
\[\begin{tikzcd}
C && L \\
\\
&& Dd
\arrow["{out_d}", from=1-3, to=3-3]
& Dd
\arrow["{out_d}", from=1-3, to=3-2]
\arrow["h", dashed, from=1-1, to=1-3]
\arrow["{f_d}"', from=1-1, to=3-3]
\arrow["{f_d}"', from=1-1, to=3-2]
\end{tikzcd}\]
\end{enumerate}
\end{definition}
The notion of limit can be instantiated to many interesting notions:
\begin{definition}[Terminal object (as limit)]
\begin{definition}[Terminal Object (as Limit)]
Let $\CD$ be the empty category $\emptyset$.
Diagrams of $\CD$ are empty and thus cones consist of just the apex $C\in\obj{\CC}$.
This also means that every object in $\CC$ forms a cone for this diagram.
The limit $1 \in \obj{\CC}$ is thus the terminal object, since for any $C \in \obj{\CC}$ there is a unique morphism $\bang : C \to 1$.
\end{definition}
\begin{definition}[Product (as limit)]
\begin{definition}[Product (as Limit)]
Let $\CD$ be the discrete category with 2 elements. Diagrams $D$ are pairs $(A,B)$ of objects of $\CC$, cones are pairs of morphisms
% https://q.uiver.app/#q=WzAsMyxbMSwwLCJDIl0sWzAsMSwiQSJdLFsyLDEsIkIiXSxbMCwxLCJmIiwyXSxbMCwyLCJnIl1d
\[\begin{tikzcd}
@ -1167,11 +1167,16 @@ The notion of limit can be instantiated to many interesting notions:
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{theorem}
The following are equivalent:
\begin{enumerate}
\item $\CC$ is complete
\item $\CC$ has (all) products and equalizers
\item $\CC$ has products and pullbacks
\end{enumerate}
\end{theorem}
\begin{proof}
% TODO proof that complete iff products and eq
% TODO
\end{proof}
\begin{definition}[Finitely Complete Category]
@ -1193,4 +1198,157 @@ The notion of limit can be instantiated to many interesting notions:
\section{Colimits}
% TODO colimits
Dual to the notion of limit is the notion of \emph{colimit}.
\begin{definition}[Colimit]
Again, we will need a preliminary notion.
\begin{enumerate}
\item A \emph{cocone} of a diagram $D : \CD \to CC$ consists of
\begin{itemize}
\item an object $C \in \obj{\CC}$ that we call the \emph{foot} and
\item a family of morphisms ${(f_d : Dd \to C)}_{d \in \obj{\CD}}$ such that
% https://q.uiver.app/#q=WzAsMyxbMSwyLCJDIl0sWzAsMCwiRGQiXSxbMiwwLCJEZCciXSxbMSwwLCJmX2QiLDJdLFsyLDAsImZfe2QnfSJdLFsxLDIsIkR1Il1d
\[\begin{tikzcd}
Dd && {Dd'} \\
\\
& C
\arrow["{f_d}"', from=1-1, to=3-2]
\arrow["{f_{d'}}", from=1-3, to=3-2]
\arrow["Du", from=1-1, to=1-3]
\end{tikzcd}\]
commutes for every $u : d \to d'$.
\end{itemize}
\item A \emph{colimit} of a diagram $D$ is an initial cocone, i.e.\ a cocone $(L, in_d)$ such that for every cocone $(C, f_d)$ there exists a unique morphism $h : L \to C$ such that $h \comp in_d = f_d$ for all $d \in \obj{\CD}$:
% https://q.uiver.app/#q=WzAsMyxbMiwyLCJMIl0sWzEsMCwiRGQiXSxbMCwyLCJDIl0sWzEsMCwie2lufV9kIl0sWzAsMiwiXFxleGlzdHMhaCIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsImZfZCIsMl1d
\[\begin{tikzcd}
& Dd \\
\\
C && L
\arrow["{{in}_d}", from=1-2, to=3-3]
\arrow["{\exists!h}"', dashed, from=3-3, to=3-1]
\arrow["{f_d}"', from=1-2, to=3-1]
\end{tikzcd}\]
\end{enumerate}
\end{definition}
Now we can instantiate the notion of colimit to the dual notions of \autoref{sec:limit}.
\begin{definition}[Initial Object (as Colimit)]
Let $\CD$ be the empty category $\emptyset$.
Diagrams of $\CD$ are empty and thus cocones of these diagrams are equal to the cones, which consist of a single object.
The colimit $0 \in \obj{\CC}$ of such a diagram is thus the initial object, since for any $C\in\obj{\CC}$ there is a unique morphism $\cobang : 0 \to C$.
\end{definition}
\begin{definition}[Coproduct (as Colimit)]
Let $\CD$ be the discrete category with 2 elements. Cocones are pairs of morphisms:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzIsMCwiQiJdLFsxLDEsIkMiXSxbMCwyLCJmIiwyXSxbMSwyLCJnIl1d
\[\begin{tikzcd}
A && B \\
& C
\arrow["f"', from=1-1, to=2-2]
\arrow["g", from=1-3, to=2-2]
\end{tikzcd}\]
and limits are exactly the coproducts:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzIsMCwiQiJdLFsxLDEsIkErQiJdLFsxLDMsIkMiXSxbMCwyLCJcXGlubCJdLFsxLDIsIlxcaW5yIiwyXSxbMCwzLCJmIiwyLHsiY3VydmUiOjN9XSxbMSwzLCJnIiwwLHsiY3VydmUiOi0zfV0sWzIsMywiXFxleGlzdHMhW2YsZ10iLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
\[\begin{tikzcd}
A && B \\
& {A+B} \\
\\
& C
\arrow["\inl", from=1-1, to=2-2]
\arrow["\inr"', from=1-3, to=2-2]
\arrow["f"', curve={height=18pt}, from=1-1, to=4-2]
\arrow["g", curve={height=-18pt}, from=1-3, to=4-2]
\arrow["{\exists![f,g]}"', dashed, from=2-2, to=4-2]
\end{tikzcd}\]
\end{definition}
\begin{definition}[Coequalizer]
Let $\CD$ be a category with two non-trivial and parallel morphisms $u,v : 1 \to 2$. Cocones are pairs of morphisms:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJBXzEiXSxbMiwwLCJBXzIiXSxbMSwyLCJDIl0sWzAsMSwiZiIsMCx7Im9mZnNldCI6LTF9XSxbMCwxLCJnIiwyLHsib2Zmc2V0IjoxfV0sWzAsMiwiYyIsMl0sWzEsMiwiZCJdXQ==
\[\begin{tikzcd}
{A_1} && {A_2} \\
\\
& C
\arrow["f", shift left, from=1-1, to=1-3]
\arrow["g"', shift right, from=1-1, to=1-3]
\arrow["c"', from=1-1, to=3-2]
\arrow["d", from=1-3, to=3-2]
\end{tikzcd}\]
The initial cocone is called a \emph{coequalizer} of $f$ and $g$:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJBXzEiXSxbMiwwLCJBXzIiXSxbMSwyLCJFIl0sWzEsNCwiQyJdLFswLDEsImYiLDAseyJvZmZzZXQiOi0xfV0sWzAsMSwiZyIsMix7Im9mZnNldCI6MX1dLFswLDJdLFsxLDIsImUiXSxbMCwzLCIiLDAseyJjdXJ2ZSI6M31dLFsxLDMsImMiLDAseyJjdXJ2ZSI6LTN9XSxbMiwzLCJcXGV4aXN0cyFoIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}
{A_1} && {A_2} \\
\\
& E \\
\\
& C
\arrow["f", shift left, from=1-1, to=1-3]
\arrow["g"', shift right, from=1-1, to=1-3]
\arrow[from=1-1, to=3-2]
\arrow["e", from=1-3, to=3-2]
\arrow[curve={height=18pt}, from=1-1, to=5-2]
\arrow["c", curve={height=-18pt}, from=1-3, to=5-2]
\arrow["{\exists!h}", dashed, from=3-2, to=5-2]
\end{tikzcd}\]
where the unnamed morphisms are usually omitted.
\end{definition}
\begin{definition}[Regular Epimorphism]
An epimorphism is called \emph{regular} if it is also a coequalizer.
\end{definition}
\begin{lemma}
Every coequalizer is an epimorphism and thus a regular epimorphism.
\end{lemma}
\begin{proof}
By duality.
\end{proof}
\begin{proposition}
$e$ is a regular epimorphism and a monomorphism $\iff$ $e$ is an isomorphism.
\end{proposition}
\begin{proof}
By duality.
\end{proof}
\begin{definition}[Pushout]
% TODO
\end{definition}
\begin{lemma}
Colimits are unique up to isomorphism.
\end{lemma}
\begin{proof}
By duality.
\end{proof}
\begin{definition}
A category $\CC$ is called \emph{cocomplete}, if every diagram has a colimit in $\CC$.
\end{definition}
\begin{theorem} The following are equivalent:
\begin{enumerate}
\item $\CC$ is cocomplete
\item $\CC$ has (all) coproducts and coequalizers
\item $\CC$ has coproducts and pushouts
\end{enumerate}
\end{theorem}
\begin{proof}
% TODO
\end{proof}
\begin{definition}
A category $\CC$ is called \emph{finitely cocomplete}, if every finite diagram in $\CC$ has a limit.
\end{definition}
\begin{theorem}
The following are equivalent:
\begin{enumerate}
\item $\CC$ is finitely cocomplete
\item $\CC$ has finite coproducts and coequalizers
\item $\CC$ has finite coproducts and pushouts
\item $\CC$ has an initial object and pushouts
\end{enumerate}
\end{theorem}
\begin{proof}
% TODO
\end{proof}