From 488d16570b6cd0d1bdd265e22c87e19da6e179a0 Mon Sep 17 00:00:00 2001
From: Franciszek Malinka <franciszek.malinka@gmail.com>
Date: Wed, 29 Jun 2022 15:23:29 +0200
Subject: =?UTF-8?q?Kanoniczna=20amalgamacja=20ju=C5=BC=20prawie=20gotowa!?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lic_malinka.tex | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

(limited to 'lic_malinka.tex')

diff --git a/lic_malinka.tex b/lic_malinka.tex
index 6672e83..4ce39e0 100644
--- a/lic_malinka.tex
+++ b/lic_malinka.tex
@@ -376,6 +376,10 @@
   \emph{identity morphism} $\id_A$ such that for any morphism $f\in \Mor(A, B)$
   it follows that $f\circ id_A = \id_B \circ f$.
 
+  We say that $f\colon A\to B$ is \emph{isomorphism} if there is (necessarily
+  unique) morphism $g\colon B\to A$ such that $g\circ f = id_A$ and $f\circ g = id_B$.
+  Automorphism is an isomorphism where $A = B$.
+
   A \emph{functor} is a ``homeomorphism`` of categories. We say that 
   $F\colon\cC\to\cD$ is a functor
   from category $\cC$ to category $\cD$ if it associates each object $A\in\cC$
@@ -388,6 +392,12 @@
   functors. Here, we only consider \emph{covariant functors}, so we will simply
   say \emph{functor}.
 
+  \begin{fact}
+	\label{fact:functor_iso}
+	Functor $F\colon\cC\to\cD$ maps isomorphism $f\colon A\to B$ in $\cC$
+	to the isomorphism $F(f)\colon F(A)\to F(B)$ in $\cD$.
+  \end{fact}
+
   Notion that will be very important for us is a ``morphism of functors``
   which is called \emph{natural transformation}.
   \begin{definition}
@@ -726,6 +736,13 @@
 			& C \arrow[ur] \arrow[ul] \arrow[uu, dashed, "\gamma"] & \\ 
 		  \end{tikzcd}
 		\end{center}
+		% \begin{center}
+		%   \begin{tikzcd}
+			% & A \ar[rrr, dashed, "\alpha"] \ar[drr, bend left=20, crossing over] & & & A' \ar[dr] & \\
+			% C \ar[rr, dashed, "\gamma"] \ar[ur] \ar[dr] & & C \ar[rrd, bend right=20] \ar[rru, bend left=20] & A\otimes_C B \ar[rr, dashed, "\delta"] & & A' \otimes_C B' \\
+			% & B \ar[rrr, dashed, "\beta"] \ar[urr, bend right=20, crossing over] & & & B' \ar[ur] & \\
+		%   \end{tikzcd}
+		% \end{center}
 	\end{itemize}
   \end{definition}
 
@@ -735,6 +752,43 @@
 	Then the class $\cH$ of $L$-structures with automorphism is a Fraïssé class.
   \end{theorem}
 
+  \begin{proof}
+	$\cH$ is obviously countable and has HP. It suffices to show that it
+	has AP (JEP follows by taking $C$ to be the empty structure). Take any
+	$(A,\alpha), (B,\beta), (C,\gamma)\in \cH$ such that $(C,\gamma)$ embeds
+	into $(A,\alpha)$ and $(B,\beta)$. Then $\alpha, \beta, \gamma$ yield
+	an automorphism $\eta$ (as a natural transformation) of a cospan:
+	\begin{center}
+	  \begin{tikzcd}
+		A & & B \\
+		% & C \ar[ur] \ar[ul] & \\
+		A \ar[u, dashed, "\alpha"] & C \ar[ur] \ar[ul] & B \ar[u, dashed, "\beta"'] \\
+		& C \ar[ur] \ar[ul] \ar[u, dashed, "\gamma"] &
+		% (A, \alpha) & & (B, \beta) \\
+		% & (C, \gamma) \ar[ur] \ar[ul] &
+	  \end{tikzcd}
+	\end{center}
+	
+	Then, by the fact \ref{fact:functor_iso}, $\otimes_C(\eta)$ is an automorphism
+	of the pushout diagram:
+	
+	\begin{center}
+	  \begin{tikzcd}
+		& A\otimes_C B \ar[loop above, "\delta"] & \\
+		A \ar[ur] \ar[loop left, "\alpha"]& & B \ar[ul] \ar[loop right, "\beta"]\\
+		& C \ar[ur] \ar[ul] \ar[loop below, "\gamma"] & 
+	  \end{tikzcd}
+	\end{center}
+	
+	TODO: ten diagram nie jest do końca taki jak trzeba, trzeba w zasadzie skopiować
+	ten z definicji kanonicznej amalgamcji. Czy to nie będzie wyglądać źle?
+
+	This means that the morphism $\delta\colon A\otimes_C B\to A\otimes_C B$
+	has to be automorphism. Thus, by the fact that the diagram commutes, 
+	we have the amalgamation of $(A, \alpha)$ and $(B, \beta)$ over $(C,\gamma)$ 
+	in $\cH$.
+  \end{proof}
+
   \subsection{Graphs with automorphism}
   The language and theory of unordered graphs is fairly simple. We extend the
   language by one unary symbol $\sigma$ and interpret it as an arbitrary
-- 
cgit v1.2.3