my forest
colimit construction
+127
-4
+1
-1
trees/dt/dt-004S.tree
+1
-1
trees/dt/dt-004S.tree
···
2
2
\author{liamoc}
3
3
\taxon{Definition}
4
4
\title{Least upper bounds in the category #{\mathbf{Cpo}}}
5
-
\p{A [cpo](dt-001D) #{A} is the [\em{least} upper bound](dt-0017) of an [#{\omega}-chain of cpos](dt-004Q) if is both an [upper bound](dt-004R) and if there exists a \em{unique} #{k} for any other [upper bound](dt-004R) #{B} such that the following diagram commutes (i.e. #{h_i = g_i \circ k} for all #{i \in \mathbb{N}}):}
5
+
\p{A [cpo](dt-001D) #{A} is the [\em{least} upper bound](dt-0017) of an [#{\omega}-chain of cpos](dt-004Q) if is both an [upper bound](dt-004R) and if there exists a \em{unique} #{k} for any other [upper bound](dt-004R) #{B} such that the following diagram commutes (i.e. #{h_i = k \circ g_i} for all #{i \in \mathbb{N}}):}
6
6
\figure{
7
7
\tex{\usepackage{tikz-cd}}{
8
8
\begin{tikzcd}
+3
-1
trees/dt/dt-004Z.tree
+3
-1
trees/dt/dt-004Z.tree
+1
trees/dt/dt-0052.tree
+1
trees/dt/dt-0052.tree
+5
-1
trees/dt/dt-005A.tree
+5
-1
trees/dt/dt-005A.tree
···
1
1
\title{Generalising to #{\textbf{Cpo}^\textbf{R}}}
2
2
\author{liamoc}
3
3
\p{All of our other notions for #{\textbf{Cpo}} naturally generalise to a setting with [retraction pairs](dt-0054) #{\textbf{Cpo}^\textbf{R}}: least elements, [#{\omega}-chains](dt-004Q), [upper bounds](dt-004R), [colimits](dt-004S), [cocontinuous endofunctors](dt-004V) and so on.}
4
-
\transclude{dt-005C}
4
+
\transclude{dt-005C}
5
+
\transclude{dt-005D}
6
+
\transclude{dt-005G}
7
+
\transclude{dt-005F}
8
+
\transclude{dt-005E}
+1
-1
trees/dt/dt-005B.tree
+1
-1
trees/dt/dt-005B.tree
···
1
1
\taxon{Theorem}
2
2
\title{Fixed point theorem for endofunctors on #{\textbf{Cpo}^\textbf{R}}}
3
-
\p{Every [cocontinuous endofunctor](TODO) #{\mathcal{F}} on #{\mathbf{Cpo}^\textbf{R}} has a least fixed point, given by the [colimit](TODO) of the ascending [#{\omega}-chain](dt-005C):
3
+
\p{Every [cocontinuous endofunctor](dt-005E) #{\mathcal{F}} on #{\mathbf{Cpo}^\textbf{R}} has a least fixed point, given by the [colimit](dt-005F) of the ascending [#{\omega}-chain](dt-005C):
4
4
\figure{
5
5
\tex{\usepackage{tikz-cd}}{\begin{tikzcd}
6
6
\mathbf{1} \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em] &
+10
trees/dt/dt-005D.tree
+10
trees/dt/dt-005D.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Endofunctors on #{\textbf{Cpo}^\textbf{R}}}
5
+
\p{An \em{endofunctor} on [the category #{\textbf{Cpo}^\textbf{R}}](dt-0058) is a [functor](dm-000J) #{\textbf{Cpo}^\textbf{R} \rightarrow \textbf{Cpo}^\textbf{R}}, i.e. a mapping #{\mathcal{F}} on [cpos](dt-001D) together with a mapping #{\mathcal{F}} on [retraction pairs](dt-0054), such that:}
6
+
\ol{
7
+
\li{If #{(f,g)} is a [retraction pair](dt-0054) #{A \rpair{f}{g} B} then #{\mathcal{F}(f,g)} is a [retraction pair](dt-0054) #{\mathcal{F}(A)\rpair{}{} \mathcal{F}(B)} }
8
+
\li{#{\mathcal{F}(\mathsf{id}_A : A\rpair{}{} A) = \mathsf{id}_{\mathcal{F}(A)} : \mathcal{F}(A)\rpair{}{} \mathcal{F}(A)}}
9
+
\li{#{\mathcal{F}(f \circ g) = \mathcal{F}(f) \circ \mathcal{F}(g)}} (where #{\circ} is [composition of retraction pairs](dt-0056))
10
+
}
+31
trees/dt/dt-005E.tree
+31
trees/dt/dt-005E.tree
···
1
+
\import{dt-macros}
2
+
\title{Cocontinuous endofunctors on #{\textbf{Cpo}^\textbf{R}}}
3
+
\taxon{Definition}
4
+
\p{An [endofunctor](dt-005D) #{\mathcal{F}} is \em{cocontinuous} iff it preserves [colimits](dt-005F) of [#{\omega}-chains of cpos](dt-005C). That is, given a [chain](dt-005C) where #{A} is a [colimit](dt-005F):
5
+
\figure{
6
+
\tex{\usepackage{tikz-cd}}{
7
+
\begin{tikzcd}
8
+
&&A\ar[ddll,<-,xshift=-0.8em]\ar[ddll,->,xshift=-0.2em]
9
+
\ar[ddl,<-,xshift=-0.35em]\ar[ddl,->,xshift=0.1em]
10
+
\ar[dd,<-,xshift=-0.1em]\ar[dd,->,xshift=0.3em] \\
11
+
&&&\cdots \\
12
+
D_0 \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em] &
13
+
D_1 \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em] &
14
+
D_2 \ar[r,-,dotted,yshift=0.2em]\ar[r,dotted,-,yshift=-0.2em]&
15
+
\cdots
16
+
\end{tikzcd}
17
+
}}
18
+
Then #{\mathcal{F}(A)} is a [colimit](dt-005F) for the following [chain](dt-005C):
19
+
\figure{\tex{\usepackage{tikz-cd}}{
20
+
\begin{tikzcd}
21
+
&&\mathcal{F}(A)\ar[ddll,<-,xshift=-0.8em]\ar[ddll,->,xshift=-0.2em]
22
+
\ar[ddl,<-,xshift=-0.35em]\ar[ddl,->,xshift=0.1em]
23
+
\ar[dd,<-,xshift=-0.1em]\ar[dd,->,xshift=0.3em] \\
24
+
&&&\cdots \\
25
+
\mathcal{F}(D_0) \ar[r,"\mathcal{F}(f_0)",->,yshift=0.2em]\ar[r,"\mathcal{F}(g_0)"', <-,yshift=-0.2em] &
26
+
\mathcal{F}(D_1) \ar[r,"\mathcal{F}(f_1)",->,yshift=0.2em]\ar[r,"\mathcal{F}(g_1)"', <-,yshift=-0.2em] &
27
+
\mathcal{F}(D_2) \ar[r,-,dotted,yshift=0.2em]\ar[r,dotted,-,yshift=-0.2em]&
28
+
\cdots
29
+
\end{tikzcd}
30
+
}}
31
+
}
+5
trees/dt/dt-005F.tree
+5
trees/dt/dt-005F.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Colimits in the category #{\mathbf{Cpo}^\mathbf{R}}}
5
+
\p{A [cpo](dt-001D) #{A} is the \em{colimit} of an [#{\omega}-chain of cpos](dt-005C) #{A_i} if is both an [upper bound](dt-005G), i.e. there exists [retraction pairs](dt-0054) #{(f_i,g_i) : A_i \rpair{}{} A}, and for any other [upper bound](dt-005G) #{B}, for which there will exist [retraction pairs](dt-0054) #{(m_i,n_i) : A_i \rpair{}{} B}, there exists a \em{unique} [retraction pair](dt-0054) #{A \rpair{k}{k'} B} such that #{(m_i,n_i) = (k,k') \circ(f_i,g_i) } for all #{i \in \mathbb{N}}, where #{\circ} is [composition of retraction pairs](dt-0056). Viewed diagramatically, it is the same as \ref{dt-004S} where [continuous functions](dt-001J) are replaced by [retraction pairs](dt-0054).}
+17
trees/dt/dt-005G.tree
+17
trees/dt/dt-005G.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\title{Upper bounds in the category #{\mathbf{Cpo}^\mathbf{R}}}
4
+
\p{A [cpo](dt-001D) #{A} is an [upper bound](dm-000C) of an [#{\omega}-chain of cpos](dt-005C) #{A_i} in [the category #{\mathbf{Cpo}^\textbf{R}}](dt-0058) if there is a family of [retraction pairs](dt-0054) #{A_i \rpair{f_i}{g_i} A} such that the following diagram commutes (i.e. for all #{i \in \mathbb{N}}, #{(f_i, g_i) = (f_{i+1},g_{i+1}) \circ (s_i,t_i)}, where #{\circ} is [composition of retraction pairs](dt-0056)):}
5
+
\figure{
6
+
\tex{\usepackage{tikz-cd}}{
7
+
\begin{tikzcd}
8
+
&&A\ar[ddll,<-,xshift=-0.8em,"f_0"']\ar[ddll,->,"g_0",xshift=-0.2em]
9
+
\ar[ddl,<-,"g_1",xshift=-0.35em]\ar[ddl,->,"f_1"',xshift=0.1em]
10
+
\ar[dd,<-,"f_2"',xshift=-0.1em]\ar[dd,->,"g_2",xshift=0.3em] \\
11
+
&&&\cdots \\
12
+
A_0 \ar[r,"s_0",->,yshift=0.2em]\ar[r,"t_0"', <-,yshift=-0.2em] &
13
+
A_1 \ar[r,"s_1",->,yshift=0.2em]\ar[r,"t_1"', <-,yshift=-0.2em] &
14
+
A_2 \ar[r,-,dotted,yshift=0.2em]\ar[r,dotted,-,yshift=-0.2em]&
15
+
\cdots
16
+
\end{tikzcd}
17
+
}}
+53
trees/dt/dt-005H.tree
+53
trees/dt/dt-005H.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Construction}
4
+
\title{The colimit #{D^\infty}}
5
+
\p{Given an [#{\omega}-chain](dt-005C):}
6
+
\figure{
7
+
\tex{\usepackage{tikz-cd}}{
8
+
\begin{tikzcd}
9
+
D_0 \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em] &
10
+
D_1 \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em] &
11
+
D_2 \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em] &
12
+
D_3 \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em] &
13
+
\cdots
14
+
\end{tikzcd}
15
+
}}
16
+
\p{The [colimit](dt-005F) (or inverse limit) is the [cpo](dt-001D) of #{\omega}-tuples:
17
+
##{
18
+
D_\infty\; \triangleq\; \left\Set{ (x_0, x_1, \dots ) \mid x_i \in D_i \land x_i = g_i(x_{i+1}) \right}
19
+
}
20
+
That is, it is countable sequence of elements, one for each domain #{D_i}, where each element is consistent with earlier elements.}
21
+
\p{ \strong{Ordering:} The ordering is the pointwise ordering of products, naturally generalised to #{\omega}-tuples. Under this ordering, #{D_\infty} is a [cpo](dt-001D). In fact if each #{D_i} is a [Scott domain](dt-004G), so is #{D_\infty}.
22
+
\proofblock{
23
+
\p{We shall prove that #{D_\infty} is an [upper bound](dt-005G) of the [#{\omega}-chain](dt-005C). Proof that it is the [least upper bound](dt-005F) is straightforward but tedious, and is omitted.}
24
+
\p{We must construct a family of [retraction pairs](dt-0054):
25
+
##{\left\Set{ D_i \rpair{\theta_{i,\infty}}{\theta_{\infty,i}} D_\infty \middle|\;\; i \in \mathbb{N}\;\; \right}}
26
+
such that the following diagram commutes:
27
+
\figure{
28
+
\tex{\usepackage{tikz-cd}}{\begin{tikzcd}
29
+
&&D_\infty\ar[ddll,<-,xshift=-0.8em]\ar[ddll,->,xshift=-0.2em]
30
+
\ar[ddl,<-,xshift=-0.35em]\ar[ddl,->,xshift=0.1em]
31
+
\ar[dd,<-,xshift=-0.1em]\ar[dd,->,xshift=0.3em] \\
32
+
&&&\cdots \\
33
+
D_0 \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em] &
34
+
D_1 \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em] &
35
+
D_2 \ar[r,-,dotted,yshift=0.2em]\ar[r,dotted,-,yshift=-0.2em]&
36
+
\cdots
37
+
\end{tikzcd}
38
+
}}
39
+
Defining the projection of the [retraction pair](dt-0054) #{D_i \rpair{\theta_{i,\infty}}{\theta_{\infty,i}} D_\infty} is straightforward:
40
+
##{
41
+
\theta_{\infty,i}(x_0,x_1,\dots) \; \triangleq \; x_i
42
+
}
43
+
However, to define the \em{embedding} #{\theta_{i,\infty}} requires us to, for a given value #{x \in D_i}, produce an #{\omega}-tuple of values consistent with #{x} in every domain #{D_k}. We do this by defining #{\theta_{i,\infty}} in terms of helper functions #{\theta_{i,j}}:
44
+
##{
45
+
\theta_{i,\infty}(x) \; \triangleq \; (\theta_{i,0}(x),\theta_{i,1}(x),\theta_{i,2}(x),\dots)
46
+
}
47
+
The helper functions #{\theta_{i,j}} are defined by composing sequences of \em{embeddings} (#{f}s) or \em{projections} (#{g}s), depending on whether #{i < j} or #{j < i}. For example, when #{i = 2}:
48
+
##{
49
+
\begin{array}{lcl} \theta_{2,\infty}(x) &=& (\theta_{i,0}(x),\theta_{i,1}(x),\theta_{i,2}(x),\theta_{i,3}(x),\theta_{i,4}(x),\dots) \\[1em]
50
+
&=& \lparen\underbrace{g_0(g_1(x))\rparen, g_1(x)}_{\text{\emph{approximations} to}\ x}, x, \underbrace{f_2(x), f_3(f_2(x)),\dots}_{\text{\emph{equivalent} to}\ x}\rparen
51
+
\end{array}
52
+
}
53
+
}}}