my forest
finish sums
+142
-5
+1
-1
trees/dm/dm-000L.tree
+1
-1
trees/dm/dm-000L.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{Commutative Diagrams}
3
+
\title{Commutative diagrams}
4
4
\p{When working in a [category](dm-000G), we can state many theorems compactly using \em{commutative diagrams}, such as this diagram for products:
5
5
\figure{
6
6
\tex{\usepackage{tikz-cd}}{
+5
-4
trees/dt/dt-0030.tree
+5
-4
trees/dt/dt-0030.tree
···
2
2
\title{Sums}
3
3
\author{liamoc}
4
4
\transclude{dt-0031}
5
-
\subtree{
6
-
\title{Primitive functions for sums}
7
-
\author{liamoc}
8
-
\transclude{dt-0032}
5
+
\transclude{dt-003D}
6
+
\transclude{dt-0039}
7
+
\transclude{dt-0036}
8
+
\upshotblock{
9
+
\p{Our [category #{\mathbf{Cpo}}](dt-002B) has only [local](dt-0039) sums.}
9
10
}
+6
trees/dt/dt-0033.tree
+6
trees/dt/dt-0033.tree
+13
trees/dt/dt-0034.tree
+13
trees/dt/dt-0034.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{The case function}
5
+
\p{Elimination of [sums](dt-0031) is captured by the \em{case} function #{\scase{f}{g} : (A + B) \contto C}, made from functions #{f : A \contto C} and #{g : B \contto C}. This function is defined by:
6
+
##{
7
+
\begin{array}{l}
8
+
\scase{f}{g} : (A + B) \contto C\\
9
+
\scase{f}{g}(x) = \begin{cases} f(a) & \text{if}\ x = (0,a) \\
10
+
g(b) & \text{if}\ x = (1,b) \\
11
+
\bot_C & \text{if}\ x = \bot_{A+B}\end{cases}
12
+
\end{array}
13
+
}}
+31
trees/dt/dt-0035.tree
+31
trees/dt/dt-0035.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\p{
5
+
Prove that the [case function](dt-0034) #{\scase{f}{g}(x)} is, given [continuous](dt-001J) functions #{f : A \contto C} and #{g : B \contto C}, [continuous](dt-001J) on its argument #{x}.
6
+
\solnblock{
7
+
\p{
8
+
As mentioned in \ref{dt-0031}, the only [directed](dt-0010) subsets of #{A + B} are those that contain entirely values of the format #{(0,\_)} and optionally #{\bot_{A+B}}, \em{or} those that contain entirely values of the format #{(1,\_)} and optionally #{\bot_{A+B}}. Call this [directed](dt-0010) subset #{X}.
9
+
}
10
+
\ul{
11
+
\li{\em{When #{\bigsqcup X = \bot_{A+B}}}: This means that #{X = \Set{\bot_{A+B}}} as #{\bot} is always the least element. From \ref{dt-0034}, we have: ##{\begin{array}{lcl} \scase{f}{g}(\bigsqcup X) &=& \scase{f}{g}(\bot_{A+B}) \\ &=& \bot_C \\ &=& \bigsqcup \Set{\bot_C} \\ &=& \bigsqcup\Set{\scase{f}{g}(\bot_{A+B})} \\ &=& \bigsqcup \Set{\scase{f}{g}(x) \mid x \in X}\end{array} } This discharges both requirements in \ref{dt-001J} for this case.}
12
+
\li{\em{When #{\bigsqcup X = (0,\_)}}: This means that #{X} consists of at least one #{(0,\_)} value plus possibly #{\bot_{A+B}}, that is #{X \setminus \Set{\bot_{A+B}} = \Set{ (0,a) \mid a \in Y} } for some nonempty #{Y \subseteq A}. We have the following, using the [continuity](dt-001J) of #{f}:
13
+
##{\begin{array}{lcl}
14
+
\scase{f}{g}(\bigsqcup X) &=& \scase{f}{g}(\bigsqcup (X \setminus \Set{\bot_{A+B}})) \\
15
+
&=& \scase{f}{g}(\bigsqcup \Set{ (0,a) \mid a \in Y} )\\
16
+
&=& \scase{f}{g}(0,\bigsqcup Y) \\
17
+
&=& f(\bigsqcup Y) \\
18
+
&=& \bigsqcup \Set{ f(a) \mid a \in Y } \\
19
+
&=& \bigsqcup \Set{ \scase{f}{g}(0,a) \mid a \in Y} \\
20
+
&=& \bigsqcup \Set{ \scase{f}{g}(x) \mid x \in X \setminus \Set{\bot_{A+B}} } \\
21
+
&=& \bigsqcup (\Set{ \scase{f}{g}(x) \mid x \in X \setminus \Set{\bot_{A+B}} } \cup \Set{\bot_C}) \\
22
+
&=& \bigsqcup \Set{ \scase{f}{g}(x) \mid x \in X } \\
23
+
\end{array}}
24
+
}
25
+
\li{
26
+
\em{When #{\bigsqcup X = (1,\_)}}: Similar to the #{(0,\_)} case but using #{g} rather than #{f}.
27
+
}
28
+
29
+
}
30
+
}
31
+
}
+6
trees/dt/dt-0036.tree
+6
trees/dt/dt-0036.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Sums form a bifunctor}
4
+
\p{With these, we can define the morphism mapping for the [sum](dt-0031) [bifunctor](dm-000M) #{(+) : \textbf{Cpo} \times \textbf{Cpo} \rightarrow \textbf{Cpo}}. Just as with [products](dt-0026) and [functions](dt-002W), we will overload the #{+} notation for \em{morphisms} as well as objects in [the category #{\mathbf{Cpo}}](dt-002B).}
5
+
\transclude{dt-0037}
6
+
\transclude{dt-0038}
+5
trees/dt/dt-0037.tree
+5
trees/dt/dt-0037.tree
+8
trees/dt/dt-0038.tree
+8
trees/dt/dt-0038.tree
+17
trees/dt/dt-0039.tree
+17
trees/dt/dt-0039.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Locality of sums}
4
+
\p{We can see by the definitions of [case](dt-0034) and our [constructors](dt-0032) that #{\scase{f}{g} \circ \mathit{inl} = f} and #{\scase{f}{g} \circ \mathit{inr} = g}, or, in a [commutative diagram](dm-000L):}
5
+
\figure{
6
+
\tex{\usepackage{tikz-cd}}{
7
+
\begin{tikzcd}[row sep=large]
8
+
& C \arrow[dl, "f",<-,labels=above left]\arrow[dr,<-,"g"]\arrow[d,"{[ f, g ]}", <-, labels=description] & \\
9
+
A & A + B \ar[l, "{\mathit{inl}}",<-,labels=below] \ar[r, "{\mathit{inr}}",<-,labels=below]& B
10
+
\end{tikzcd}
11
+
}
12
+
}
13
+
\p{Note that this diagram is like the [dual](dm-000Q) of the diagram seen in the [universal property for products](dt-0029) — the arrows are reversed. That is because, generally speaking, sums are dual to products. However, because of our additional #{\bot} value, our [cpo sums](dt-0031) are only \em{weakly} universal — the #{h} arrow is \em{not} unique.
14
+
}
15
+
\transclude{dt-003A}
16
+
\transclude{dt-003B}
17
+
\transclude{dt-003C}
+16
trees/dt/dt-003A.tree
+16
trees/dt/dt-003A.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\title{Weak universality of cpo sums}
5
+
\p{
6
+
Consider this scenario with the [cpos](dt-001D) #{\textbf{2} = \Set{ \top, \bot }} and #{\textbf{1} = \Set{\bot }}:
7
+
\figure{
8
+
\tex{\usepackage{tikz-cd}}{
9
+
\begin{tikzcd}[row sep=large]
10
+
& \mathbf{2} \arrow[dl, "\lambda x.\ \top",<-,labels=above left]\arrow[dr,<-,"\lambda x.\ \top"]\arrow[d,"{h}", <-, labels=description] & \\
11
+
\mathbf{1} & \mathbf{1} + \mathbf{1} \ar[l, "{\mathit{inl}}",<-,labels=below] \ar[r, "{\mathit{inr}}",<-,labels=below]& \mathbf{1}
12
+
\end{tikzcd}
13
+
}
14
+
}
15
+
In this case, setting the function #{h = \lambda x.\ \top} makes the diagram commute, but #{(\lambda x.\ \top) \neq \scase{\lambda x.\ \top}{ \lambda x.\ \top}} due to the different handling of #{\bot_{\textbf{1}+\textbf{1}}}.
16
+
}
+8
trees/dt/dt-003B.tree
+8
trees/dt/dt-003B.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Weak universal property for [cpo sums](dt-0031)}
5
+
##{
6
+
(h \circ \mathit{inl} = f \land h \circ \mathit{inr} = g)\;\; \text{iff}\;\; \scase{f}{g} \sqsubseteq h
7
+
}
8
+
\p{This property is called \em{weak} because it uses only the [information ordering](dt-000B) rather than equality on the right hand side.}
+11
trees/dt/dt-003C.tree
+11
trees/dt/dt-003C.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Failure of sum isomorphisms}
4
+
\taxon{Warning}
5
+
\p{
6
+
The weakness of the [universal property for sums](dt-0038) means that many common [isomorphisms](dt-002E) for sums in other contexts do not hold:
7
+
\ul{
8
+
\li{ #{A + (B + C) \not\simeq (A + B) + C}}
9
+
\li{ #{(A \contto C) \times (B \contto C) \not\simeq (A+B) \contto C}}
10
+
}
11
+
}
+6
trees/dt/dt-003D.tree
+6
trees/dt/dt-003D.tree
+9
trees/dt/dt-macros.tree
+9
trees/dt/dt-macros.tree
···
6
6
\subtree{\taxon{Proof}
7
7
\body
8
8
}}}
9
+
\def\upshotblock[body]{\scope{
10
+
\put\transclude/toc{false}
11
+
\put\transclude/numbered{false}
12
+
\subtree{\taxon{Upshot}
13
+
\body
14
+
}}}
9
15
\def\solnblock[body]{\scope{
10
16
\put\transclude/toc{false}
11
17
\put\transclude/numbered{false}
···
23
29
\def\fixop{#{\textbf{fix}}}
24
30
\def\acr[distance]{\\[\distance]}
25
31
\def\lsquare{\startverb[\stopverb}
32
+
\def\rsquare{\startverb]\stopverb}
33
+
\def\lparen{\startverb(\stopverb}
26
34
\def\rparen{\startverb)\stopverb}
35
+
\def\scase[x][y]{\lsquare\x,\y\rsquare}
27
36
\def\op-cl-int[x][y]{\lsquare\x,\y\rparen}
28
37
\def\contto{\twoheadrightarrow}