diff --git a/exam/main.tex b/exam/main.tex index 17c56f2..57af663 100644 --- a/exam/main.tex +++ b/exam/main.tex @@ -33,7 +33,7 @@ \begin{parts} \part Was sind F-Algebren? \part Was sind initiale Algebren? - \part Hat jede Algebra eine initiale Algebra? Wenn nein Gegenbeispiel + \part Hat jeder Funktor eine initiale Algebra? Wenn nein Gegenbeispiel \part Wie beweist man Lambeks Lemma? \part Wie konstruiert man F-Algebren? \end{parts} diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index bf59a35..725289b 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/tex/.vscode/ltex.dictionary.en-US.txt @@ -68,3 +68,5 @@ Cocones coequalizer coequalizers pushouts +pushout +monic diff --git a/tex/main.pdf b/tex/main.pdf deleted file mode 100644 index aa80921..0000000 Binary files a/tex/main.pdf and /dev/null differ diff --git a/tex/main.tex b/tex/main.tex index 7d337f9..1e4af0f 100644 --- a/tex/main.tex +++ b/tex/main.tex @@ -25,6 +25,7 @@ \pagestyle{scrheadings} \newcounter{resumeenum} % for resuming enumerated lists, https://tex.stackexchange.com/a/1702 \usepackage{catprog} +\usepackage{multicol} %%%% %%%% Metadata diff --git a/tex/sections/02_categories.tex b/tex/sections/02_categories.tex index 49f63e1..53330a6 100644 --- a/tex/sections/02_categories.tex +++ b/tex/sections/02_categories.tex @@ -940,11 +940,12 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial: \end{remark} \begin{example} As a consequence of the previous remark, we can follow that for $FX = 2 \times X^\Sigma$ the following holds: - \[x \sim y \iff x,y accept the same formal language.\] + \[x \sim y \iff x,y \text{ accept the same formal language.}\] \end{example} \begin{definition}[Bisimulation] - Let $F : \Set \to \Set$ and let $(C,c), (D,d)$ be F-coalgebras. A \emph{bisimulation} is a relation $R \subseteq C \times C$ such that a coalgebra $(R, r)$ exists where + Let $F : \Set \to \Set$ and let $(C,c), (D,d)$ be F-coalgebras. + A \emph{bisimulation} is a relation $R \subseteq C \times D$ such that a coalgebra $(R, r)$ exists where % https://q.uiver.app/#q=WzAsOCxbMCwwLCJDIl0sWzAsMiwiRkMiXSxbMiwwLCJSIl0sWzIsMiwiRlIiXSxbNCwwLCJEIl0sWzQsMiwiRkQiXSxbMSwxLCJcXGNvbW0iXSxbMywxLCJcXGNvbW0iXSxbMCwxLCJjIl0sWzIsMywiciJdLFs0LDUsImQiXSxbMiwwLCJcXHBpXzEiLDJdLFsyLDQsIlxccGlfMiJdLFszLDEsIkZcXHBpXzEiLDJdLFszLDUsIkZcXHBpXzIiXV0= \[\begin{tikzcd} C && R && D \\ @@ -1107,14 +1108,13 @@ The notion of limit can be instantiated to many interesting notions: \begin{definition}[Pullback] Let $\CD$ be a poset category illustrated by the following diagram: - % https://q.uiver.app/#q=WzAsMyxbMSwwLCJcXGJ1bGxldCJdLFswLDEsIlxcYnVsbGV0Il0sWzIsMSwiXFxidWxsZXQiXSxbMCwxXSxbMCwyXV0= + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXGJ1bGxldCJdLFsyLDAsIlxcYnVsbGV0Il0sWzEsMSwiXFxidWxsZXQiXSxbMCwyXSxbMSwyXV0= \[\begin{tikzcd} - & \bullet \\ - \bullet && \bullet - \arrow[from=1-2, to=2-1] - \arrow[from=1-2, to=2-3] + \bullet && \bullet \\ + & \bullet + \arrow[from=1-1, to=2-2] + \arrow[from=1-3, to=2-2] \end{tikzcd}\] - Diagrams consist of two arrows with the same codomain. Cones are of the form: % https://q.uiver.app/#q=WzAsNixbMiwwLCJDIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJEIl0sWzEsMiwiXFxjb21tIl0sWzMsMiwiXFxjb21tIl0sWzAsMSwiZiIsMl0sWzAsMiwiZyJdLFsxLDMsIm0iLDJdLFsyLDMsIm4iXSxbMCwzLCJoIiwyXV0= @@ -1160,7 +1160,35 @@ The notion of limit can be instantiated to many interesting notions: Limits are unique up to isomorphism. \end{proposition} \begin{proof} - % TODO proof that limits are up to iso + Let $\CD$ be a small category and $D : \CD \to \CC$ a diagram. + Furthermore, let $(L, {out}_d)$ and $(L', {out'}_d)$ be two limits of this diagram. + Note that both $L$ and $L'$ are apexes of cones, thus they induce morphisms: + \begin{multicols}{2} + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJMIl0sWzIsMCwiTCciXSxbMSwyLCJEZCJdLFswLDIsIntvdXR9X2QiLDJdLFsxLDIsIntvdXQnfV9kIl0sWzAsMSwiaSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== + \[\begin{tikzcd} + L && {L'} \\ + \\ + & Dd + \arrow["{{out}_d}"', from=1-1, to=3-2] + \arrow["{{out'}_d}", from=1-3, to=3-2] + \arrow["i", dashed, from=1-1, to=1-3] + \end{tikzcd}\] + \columnbreak + % https://q.uiver.app/#q=WzAsMyxbMiwwLCJMIl0sWzAsMCwiTCciXSxbMSwyLCJEZCJdLFswLDIsIntvdXR9X2QiXSxbMSwyLCJ7b3V0J31fZCIsMl0sWzEsMCwiaV5cXG1vbmUiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0= + \[\begin{tikzcd} + {L'} && L \\ + \\ + & Dd + \arrow["{{out}_d}", from=1-3, to=3-2] + \arrow["{{out'}_d}"', from=1-1, to=3-2] + \arrow["{i^\mone}", dashed, from=1-1, to=1-3] + \end{tikzcd}\] + \end{multicols} + Now, using the fact that the ${out}_d$ and ${out'}_d$ are jointly monic, we are done by: + \[{out}_d \comp i^\mone \comp i = {out'}_d \comp i = {out}_d = {out}_d \comp id_L \Rightarrow i^\mone \comp i = id_L\] + and + \[{out'}_d \comp i \comp i^\mone = {out}_d \comp i^\mone = {out'}_d = {out'}_d \comp id_{L'} \Rightarrow i \comp i^\mone = id_{L'}\] + Thus $L \iso L'$. \end{proof} \begin{definition}[Complete Category] @@ -1311,7 +1339,49 @@ Now we can instantiate the notion of colimit to the dual notions of \autoref{sec \end{proof} \begin{definition}[Pushout] - % TODO + Let $\CD$ be the poset: + % https://q.uiver.app/#q=WzAsMyxbMSwwLCJcXGJ1bGxldCJdLFswLDEsIlxcYnVsbGV0Il0sWzIsMSwiXFxidWxsZXQiXSxbMCwxXSxbMCwyXV0= + \[\begin{tikzcd} + & \bullet \\ + \bullet && \bullet + \arrow[from=1-2, to=2-1] + \arrow[from=1-2, to=2-3] + \end{tikzcd}\] + + Diagrams consist of two arrows with the same domain and cocones are of the form: + % https://q.uiver.app/#q=WzAsNixbMiwwLCJIIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJDIl0sWzEsMiwiXFxjb21tIl0sWzMsMiwiXFxjb21tIl0sWzAsMSwibSIsMl0sWzAsMiwibiJdLFsxLDMsImYiLDJdLFsyLDMsImciXSxbMCwzLCJoIiwyXV0= + \[\begin{tikzcd} + && H \\ + \\ + A & \comm && \comm & B \\ + \\ + && C + \arrow["m"', from=1-3, to=3-1] + \arrow["n", from=1-3, to=3-5] + \arrow["f"', from=3-1, to=5-3] + \arrow["g", from=3-5, to=5-3] + \arrow["h"', from=1-3, to=5-3] + \end{tikzcd}\] + where $h$ is usually omitted, and instead the condition is expressed as $f \comp m = g \comp n$. + A colimit of such a diagram is called a \emph{pushout} and usually denoted: + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJIIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJQIl0sWzIsNiwiQyJdLFsxLDMsInBfMSIsMl0sWzIsMywicF8yIl0sWzAsMSwiZiIsMl0sWzAsMiwiZyJdLFszLDQsIiIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDQsImEiLDIseyJjdXJ2ZSI6M31dLFsyLDQsImIiLDAseyJjdXJ2ZSI6LTN9XSxbMywwLCIiLDAseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XV0= + \[\begin{tikzcd} + && H \\ + \\ + A &&&& B \\ + \\ + && P \\ + \\ + && C + \arrow["{p_1}"', from=3-1, to=5-3] + \arrow["{p_2}", from=3-5, to=5-3] + \arrow["f"', from=1-3, to=3-1] + \arrow["g", from=1-3, to=3-5] + \arrow[dashed, from=5-3, to=7-3] + \arrow["a"', curve={height=18pt}, from=3-1, to=7-3] + \arrow["b", curve={height=-18pt}, from=3-5, to=7-3] + \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=5-3, to=1-3] + \end{tikzcd}\] \end{definition} \begin{lemma} diff --git a/tex/sections/03_constructions.tex b/tex/sections/03_constructions.tex index 02c049f..7a72854 100644 --- a/tex/sections/03_constructions.tex +++ b/tex/sections/03_constructions.tex @@ -120,7 +120,7 @@ A consequence of \autoref{lem:finclosed} is that for any signature $\Sigma$, the is finitary. \begin{theorem} - Let $\CC$ be cocomplete and $F : \CC \to \CC$ $\sigma$-cocontinuous. Then $F$ has the initial algebra $I = \oname{colim}_{n\in\mathbb{N}} F^n 0$. + Let $\CC$ be cocomplete and $F : \CC \to \CC$ $\omega$-cocontinuous. Then $F$ has the initial algebra $I = \oname{colim}_{n\in\mathbb{N}} F^n 0$. More concretely $I$ is the colimit of the $\omega$-chain: % https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzIsMCwiRjAiXSxbNCwwLCJGRjAiXSxbNiwwLCJcXGxkb3RzIl0sWzIsMiwiXFxtdSBGIl0sWzAsMSwiaSJdLFsxLDIsIkZpIl0sWzIsMywiXFxsZG90cyJdLFswLDQsIlxcaW90YV8wIiwyLHsiY3VydmUiOjJ9XSxbMSw0LCJcXGlvdGFfMSIsMl0sWzIsNCwiXFxpb3RhXzIiLDIseyJjdXJ2ZSI6LTN9XSxbMyw0LCJcXGxkb3RzIiwwLHsiY3VydmUiOi0zfV1d \[\begin{tikzcd}