my forest
start on products for dt
+134
-1
+20
-1
trees/dt-001Z.tree
+20
-1
trees/dt-001Z.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
1
3
\taxon{Lecture}
2
4
\title{Constructions on [cpos](dt-001D) and PCF}
3
5
\author{liamoc}
4
6
\p{This lecture is based on material from [[haskellhutt]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
5
-
\p{todo}
7
+
\subtree{
8
+
\title{Products}
9
+
\p{Recall \ref{dt-000E}, which showed that the [product](dm-0005) of two [pointed posets](dt-000G) is itself a [pointed poset](dt-000G).
10
+
11
+
In \ref{dt-001X} you may also have shown that #{A \times B} is also a [cpo](dt-001D) if #{A} and #{B} are [cpos](dt-001D), with this definition for [lubs](dt-0017):
12
+
##{
13
+
\bigsqcup X \; = \; \left(\bigsqcup \{ x \mid \exists y.\ (x,y) \in X \}, \bigsqcup \{ y \mid \exists x.\ (x,y) \in X \}\right)
14
+
}
15
+
This definition can be made a little more comprehensible by defining it in terms of the two projection operators for pairs:
16
+
}
17
+
\transclude{dt-0020}
18
+
\transclude{dt-0021}
19
+
\transclude{dt-0022}
20
+
\transclude{dt-0023}
21
+
\transclude{dt-0024}
22
+
}
23
+
24
+
+45
trees/dt-0020.tree
+45
trees/dt-0020.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\author{liamoc}
4
+
\taxon{Definition}
5
+
\title{Projection operators for [products](dm-0005)}
6
+
\p{Destruction of pairs is captured by the two \em{projection} operators, defined as follows:}
7
+
\table{
8
+
\tr{
9
+
\td{
10
+
\tex{\usepackage{string-diagrams}}{
11
+
\begin{tikzpicture}
12
+
\node at (-1.5cm,0) {$ $};
13
+
\node[box, box ports west = 2, box ports east = 2, minimum width=2cm, minimum height=2cm] (A) {};
14
+
\node[dot] at (A.west.1) {};
15
+
\node[dot] at (A.east.1) {};
16
+
\draw[thick] (A.west.1) -- (A.east.1);
17
+
\draw[thick,-|] (A.west.2) -- ([xshift=-1cm]A.east.2);
18
+
\node at ([xshift=-1cm,yshift=-0.8cm]A.east.2) {$\pi_1$};
19
+
\node[dot] at (A.west.2) {};
20
+
\end{tikzpicture}
21
+
}
22
+
}
23
+
\td{
24
+
##{
25
+
\begin{array}{lcl}
26
+
\pi_0 : A \times B \rightarrow A & \qquad & \pi_1 : A \times B \rightarrow B \\
27
+
\pi_0(x, y) = x & & \pi_1(x, y) = y \\
28
+
\end{array}
29
+
}
30
+
}
31
+
\td{
32
+
\tex{\usepackage{string-diagrams}}{
33
+
\begin{tikzpicture}
34
+
\node[box, box ports west = 2, box ports east = 2, minimum width=2cm, minimum height=2cm] (B) at (12cm,0) {};
35
+
\node[dot] at (B.west.1) {};
36
+
\node[dot] at (B.east.2) {};
37
+
\draw[thick] (B.west.2) -- (B.east.2);
38
+
\draw[thick,-|] (B.west.1) -- ([xshift=-1cm]B.east.1);
39
+
\node at ([xshift=-1cm,yshift=-0.8cm]B.east.2) {$\pi_2$};
40
+
\node[dot] at (B.west.2) {};
41
+
\end{tikzpicture}
42
+
}
43
+
}
44
+
}
45
+
}
+13
trees/dt-0021.tree
+13
trees/dt-0021.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Construction}
4
+
\author{liamoc}
5
+
\title{Product of [cpos](dt-001D)}
6
+
7
+
\p{Given [cpos](dt-001D) #{A} and #{B}, the [product](dt-000G) #{A \times B} is itself a [cpo](dt-001D), ordered by
8
+
##{ (x,y) \sqsubseteq_{X \times Y} (x',y') \quad \text{iff} \quad x \sqsubseteq_X x' \land y \sqsubseteq_Y y' }
9
+
with bottom value #{\bot_{X \times Y}} being #{(\bot_A, \bot_B)}. [Least upper bounds](dt-0017) are found by taking the [lubs](dt-0017) of each component:}
10
+
11
+
##{
12
+
\bigsqcup X \; = \; \left(\bigsqcup \{ \pi_0(x) \mid x \in X \}, \bigsqcup \{ \pi_1(x) \mid x \in X \}\right)
13
+
}
+3
trees/dt-0022.tree
+3
trees/dt-0022.tree
+30
trees/dt-0023.tree
+30
trees/dt-0023.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Definition}
4
+
\author{liamoc}
5
+
\title{The split function}
6
+
\p{
7
+
\<html:div>[class]{sidefigure}{\tex{\usepackage{string-diagrams}}{
8
+
\begin{tikzpicture}
9
+
\node[box, box ports west = 1, box ports east = 2, minimum width=3cm, minimum height=3cm] (A) {};
10
+
\node[dot] at (A.east.1) {};
11
+
\node[dot] at (A.east.2) {};
12
+
\node[dot] at (A.west.1) {};
13
+
\node[dot] (X) at ([xshift=1cm]A.west.1) {};
14
+
\node[box,thick] (f) at ([xshift=-1cm]A.east.1) {f};
15
+
\node[box,thick] (g) at ([xshift=-1cm]A.east.2) {g};
16
+
\wires[thick]{
17
+
f = { west = X.north, east=A.east.1},
18
+
g = { west = X.south, east=A.east.2},
19
+
X = { west = A.west.1 }
20
+
}{}
21
+
\end{tikzpicture}}}
22
+
Construction of pairs is captured by the \em{split} function: If #{f : A \rightarrow B} and #{g : B \rightarrow C}, then \em{split}, written #{\langle f , g \rangle}, is defined as:
23
+
24
+
25
+
##{
26
+
\begin{array}{lr}
27
+
\langle f , g \rangle : A \rightarrow B \times C\\
28
+
\langle f , g \rangle\ a = (f(a), g(a))
29
+
\end{array}
30
+
}}
+23
trees/dt-0024.tree
+23
trees/dt-0024.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Theorem}
4
+
\author{liamoc}
5
+
\p{For [continuous functions](dt-001J) #{f} and #{g}, the [split function](dt-0023) #{\langle f, g \rangle} is [continuous](dt-001J).}
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\subtree{\taxon{Proof}
10
+
\ul{
11
+
\li{ \em{#{\langle f, g \rangle} is [monotonic](dt-000J)}. Let #{x \sqsubseteq y \in A}. Then: ##{\begin{array}{lclr}
12
+
\langle f , g \rangle\ x & = & (f(x), g(x)) & \text{(def)}\\
13
+
& \sqsubseteq & (f(y), g(y)) & \text{(monotonicity of $f$,$g$)}\\
14
+
& = & \langle f , g \rangle\ y & \text{(def)}
15
+
\end{array}}}
16
+
\li{ \em{#{\langle f , g \rangle} preserves [lubs](dt-0017) of [directed](dt-0010) sets}. Let #{X \subseteq A} be [directed](dt-0010). Then:}
17
+
##{\begin{array}{lclr}
18
+
\langle f , g \rangle\ (\bigsqcup X) & = & (f(\bigsqcup X), g(\bigsqcup X)) & \text{(def)}\\
19
+
& = & (\bigsqcup \{ f(x) \mid x \in X \}, \bigsqcup \{ g(x) \mid x \in X \}) & \text{(continuity of $f$,$g$)}\\
20
+
& = & \bigsqcup \{ \langle f , g \rangle\ x \mid x \in X \} & \text{(def)}
21
+
\end{array}}
22
+
}
23
+
}}