Finish proof that K is commutative

thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt

@@ -20,3 +20,8 @@
 {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q test: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
 {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
 {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:diamond Diamond\\E$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object A for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}

thesis/src/04_iteration.tex

@@ -5,24 +5,43 @@ In this chapter we will draw on the inherent connection between partiality and i
 
 \improvement{Add some text}
 \unsure[inline]{Check types etc.}
+\begin{definition}[Unguarded Elgot Algebra]
+  \todo[inline]{Definition unguarded Elgot algebra}
+\end{definition}
 
 \begin{definition}[Elgot Algebra]
   A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
   \begin{itemize}
-    \item An object X
+    \item An object A
-    \item for every $f : S \rightarrow X + S$ the iteration $f^\# : S \rightarrow X$, satisfying:
+    \item for every $f : X \rightarrow A + X$ the iteration $f^\# : X \rightarrow A$, satisfying:
     \begin{itemize}
       \item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: $f^\# = [ id , f ^\# ] \circ f$
+      \\ for $f : X \rightarrow A + X$
       \item \customlabel{law:uniformity}{\textbf{Uniformity}}: $(id + h) \circ f = g \circ h \Rightarrow f ^\# = g^\# \circ h$
-      \\ for $f : S \rightarrow X + S,\; g : R \rightarrow A + R,\; h : S \rightarrow R$
+      \\ for $f : X \rightarrow A + X,\; g : Y \rightarrow A + Y,\; h : X \rightarrow Y$
       \item \customlabel{law:folding}{\textbf{Folding}}: $((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ] ^\#$
-      \\ for $f : S \rightarrow A + S,\; h : R \rightarrow S + R$
+      \\ for $f : X \rightarrow A + X,\; h : Y \rightarrow X + Y$
     \end{itemize}
   \end{itemize}
 \end{definition}
 
-\todo[inline]{Diamond and stutter laws}
+\begin{lemma}
-\customlabel{law:diamond}{\textbf{Diamond}}
+  Every Elgot algebra $(A , (-)^\#)$ satisfies the following additional laws
+
+  \begin{itemize}
+    \item \customlabel{law:stutter}{\textbf{Stutter}}: $(([ h , h ] + id) \circ f)^\# = (i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )^\# \circ inr$
+    \\ for $f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A$
+    \item \customlabel{law:diamond}{\textbf{Diamond}}: $((id + \Delta) \circ f)^\# = ([ i_1 , ((id + \Delta) \circ f)^\# + id] \circ f)^\#$
+    \\ for $f : X \rightarrow A + (X + X)$
+    \item \customlabel{law:compositionality}{\textbf{Compositionality}}: $((f^\# + id) \circ h)^\# = ([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])^\# \circ i_2$
+    \\ for $f : X \rightarrow A + X, h : Y \rightarrow X + Y$
+  \end{itemize}
+\end{lemma}
+\begin{proof}
+  \todo[inline]{Prove diamond and stutter laws}
+\end{proof}
+
+\todo[inline]{Mention here that previous lemma implies that unguarded Elgot are id guarded Elgot and diamond gives alternate way of classifying Elgot algebras citing Sergey}
 
 Morphisms between Elgot algebras that are coherent with respect to the iteration operator are of special interest to us, the following definition classifies them.
 
@@ -707,7 +726,7 @@ The following Lemma is central to the proof of commutativity.
     \\=\;&(\pi_1 + (\pi_1 \circ \pi_1 \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
     \\=\;&(\pi_1 + \pi_1) \circ dstr \circ (\hat{f} \times id)
     \\=\;&\pi_1 \circ (\hat{f} \times id)
-    \\=\;&\hat{f} \circ \pi_1
+    \\=\;&\hat{f} \circ \pi_1 .
   \end{alignat*}
 
   This concludes the proof.
@@ -716,8 +735,8 @@ The following Lemma is central to the proof of commutativity.
 \begin{theorem}
   $\mathbf{K}$ is a commutative monad.
 \end{theorem}
-\begin{proof}
+\begin{proof} We need to show that $\tau^* \circ \sigma = \sigma^* \circ \tau : KX \times KY \rightarrow K(X \times Y)$. 
-  We use remark~\ref{rem:proofbystability} again:
+  Let us proceed by right stability, consider the following diagram.
   % https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0=
   \[\begin{tikzcd}
     & {KX \times KY} && {K(KX \times Y)} \\
@@ -731,11 +750,16 @@ The following Lemma is central to the proof of commutativity.
     \arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
     \arrow["{\sigma}"', curve={height=12pt}, from=4-1, to=3-4]
   \end{tikzcd}\]
-  \todo[inline]{Maybe don't omit proofs, give them point by point?}
-  The proofs for \ref{sharpr1} and the proof that $\sigma^* \circ \tau$ is right iteration preserving are straightforward and can be looked up in the formalization.
-  The proof that $\tau^* \circ \sigma$ is right iteration preserving is non-trivial, so we will look at it in more detail:
-  Let $Z \in \obj{\C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \sigma$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving:
 
+  The diagram commutes since
+  \[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma\]
+  and
+  \[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = (\tau \circ (id \times \eta))^* \circ \sigma = \sigma.\]
+
+  We are left to show that both $\sigma^* \circ \tau$ and $\tau^* \circ \sigma$ are right iteration preserving. Let $h : Z \rightarrow KY + Z$, indeed
+  \[\sigma^* \circ \tau \circ (id \times h^\#) = \sigma^* ((\tau + id) \circ dstl \circ (id \times h))^\# = (((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))^\#. \]
+
+  Let $\psi := \tau^* \circ \sigma$ and let us proceed by left stability to show that $\psi$ is right iteration preserving, consider the following diagram
   % https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
   \[\begin{tikzcd}
     &&&& {KX \times KY} \\
@@ -748,8 +772,61 @@ The following Lemma is central to the proof of commutativity.
     \arrow["{\eta \times id}", from=4-1, to=2-1]
     \arrow["{\tau \circ (id \times h^\#)}"', from=4-1, to=2-5]
   \end{tikzcd}\]
-\change[inline]{Be more specific}
+  which commutes, since
-\todo[inline]{Introduce Diamond and Stutter laws}
+  \begin{alignat*}{1}
+    &\psi \circ (id \times h^\#) \circ (\eta \times id)
+    \\=\;&\psi \circ (\eta \times id) \circ (id \times h^\#)
+    \\=\;&\tau^* \circ \eta \circ (id \times h^\#)
+    \\=\;&\tau \circ (id \times h^\#)
+    \\=\;&((\tau + id) \circ dstl \circ (id \times h))^\#
+    \\=\;&((\psi + id) \circ dstl \circ (id \times h))^\# \circ (\eta \times id).\tag{\ref{law:uniformity}}
+  \end{alignat*}
+
+  We are left to show that both $\psi \circ (id \times h^\#)$ and $((\psi + id) \circ dstl \circ (id \times h))^\#$ are left iteration preserving. Let $g : A \rightarrow KX + A$, then $\psi \circ (id \times h^\#)$ is left iteration preserving, since
+  \begin{alignat*}{1}
+    &\psi \circ (id \times h^\#) \circ (g^\# \times id)
+    \\=\;&\psi \circ (g^\# \times id) \circ (id \times h^\#)
+    \\=\;&\tau^* \circ ((\sigma + id) \circ dstr \circ (g \times id))^\# \circ (id \times h^\#)
+    \\=\;&((\psi + id) \circ dstr \circ (g \times id))^\# \circ (id \times h^\#)
+    \\=\;&(((\psi \circ (id \times h^\#)) + id) \circ dstr \circ (g \times id))^\#.\tag{\ref{law:uniformity}}
+  \end{alignat*}
+
+  Lastly, we need to show that
+  \[((\psi + id) \circ dstl \circ (id \times h))^\# \circ (g^\# \times id) = ((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#.\]
+  Note that by \ref{law:uniformity} the left-hand side can be rewritten as
+  \[((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#.\]
+
+  Consider now, that 
+  \begin{alignat*}{1}
+    &((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#
+    \\=\;&(((((\psi + id) \circ dstl \circ (id \times h))^\#)^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))^\#
+    \\=\;&(((\psi + id) \circ dstl \circ (id \times h))^\#)^* \circ ((\eta + id) \circ dstr \circ (g \times id))^\#
+    \\=\;&(((\psi + id) \circ dstl \circ (id \times h))^\#)^* \circ (((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))^\#
+    \\=\;&(((\psi + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&(((\psi^* + id) \circ (\eta + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ ((((\tau \circ (id \times \eta)) + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ (((\tau + id) \circ dstl \circ (id \times ((\eta + id) \circ h)))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ (\tau \circ (id \times ((\eta + id) \circ h)^\#))^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ \tau^* \circ K(id \times ((\eta + id) \circ h)^\#) \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times ((\eta + id) \circ h)^\#) \circ (((\eta + id) \circ g)^\# \times id)
+    \\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#),
+  \end{alignat*}
+  and by a symmetric argument
+  \begin{alignat*}{1}
+    &((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#
+    \\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#).
+  \end{alignat*}
+
+  We are thus done by
+  \begin{alignat*}{1}
+    &((\psi + id) \circ dstl \circ (id \times h))^\# \circ (g^\# \times id)
+    \\=\;&((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#\tag{\ref{law:uniformity}}
+    \\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#)
+    \\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#)\tag{\ref{lem:KCommKey}}
+    \\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#.
+  \end{alignat*}
 \end{proof}
 
 \begin{theorem}\label{thm:Klifting}