summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2016-02-02 22:53:37 +0100
committerGregor Kleen <gkleen@yggdrasil.li>2016-02-02 22:53:37 +0100
commitac417ac4f05b2f0422e6473a65a747692f130273 (patch)
tree10d472ea2c063acd670a5f7e02d6137070b343d0
parente283971b74db4dd0c89b1d393fc2de6d6ec85a3a (diff)
downloaddirty-haskell.org-ac417ac4f05b2f0422e6473a65a747692f130273.tar
dirty-haskell.org-ac417ac4f05b2f0422e6473a65a747692f130273.tar.gz
dirty-haskell.org-ac417ac4f05b2f0422e6473a65a747692f130273.tar.bz2
dirty-haskell.org-ac417ac4f05b2f0422e6473a65a747692f130273.tar.xz
dirty-haskell.org-ac417ac4f05b2f0422e6473a65a747692f130273.zip
Cat-T 1.2.1
-rw-r--r--provider/posts/simmons-intro-to-cat-t/1.2.md49
1 files changed, 49 insertions, 0 deletions
diff --git a/provider/posts/simmons-intro-to-cat-t/1.2.md b/provider/posts/simmons-intro-to-cat-t/1.2.md
new file mode 100644
index 0000000..00a9546
--- /dev/null
+++ b/provider/posts/simmons-intro-to-cat-t/1.2.md
@@ -0,0 +1,49 @@
1---
2title: Exercises in Category Theory — 1.2
3published: 2016-02-02
4tags: Category Theory
5---
6
7<div class="exercise">
8Let $\ca{Pno}$ be the category of objects $(A, \alpha, a)$ where $A$ is a set, $\alpha : A \to A$ is a unary function, and $a \in A$ is a nominated Element and morphisms $\arr{(A, \alpha, a)}{}{(B, \beta, b)}$ which are functions $f: A \to B$ preserving the structure such that $f \circ \alpha = \beta \circ f$ and $f(a) = b$.
9
10 a) Verify that $\ca{Pno}$ is a category
11
12 1. For every $A \in \ca{Pno}$ there exists $\idarr{(A, \alpha, b)}$
13 <div class="proof">
14 $\id$ on $A$ is indeed a function which preserves the structure ($\id \circ \alpha = \alpha = \alpha \circ \id$, $\id(a) = a$) and thus a morphism
15 </div>
16
17 2. There exists a partial binary operation $\circ$ on the arrows of $\ca{Pno}$
18 <div class="proof">
19 Given three objects $(A, \alpha, a), (B, \beta, b), (C, \gamma, c)$ and two functions $g: A \to B$ and $f: B \to C$ the function $f \circ g: A \to C$ is an arrow in $\ca{Pno}$, that is to say, it preserves structure:
20 $$(f \circ g) \circ \alpha = f \circ \beta \circ g = \gamma \circ (f \circ g)$$
21 and
22 $$(f \circ g)(a) = f(b) = c$$
23 </div>
24
25 b) Show that $(\N, \textrm{succ}, 0)$ is a $\ca{Pno}$-object
26
27 <div class="proof">
28 $\N$ is indeed a Set, $\textrm{succ}$ is indeed an unary function and $0$ is indeed an element of $\N$.
29 </div>
30
31 c) Show that for each $\ca{Pno}$-object $(A, \alpha, a)$ there is an unique arrow
32 $$\arr{(\N, \textrm{succ}, 0)}{}{(A, \alpha, a)}$$
33 and describe the behaviour of the carrying function.
34
35 <div class="proof">
36 We construct a carrying function recursively:
37 $$\begin{aligned}
38 f : \N & \to A \\
39 0 & \mapsto a \\
40 \textrm{succ}(x) & \mapsto \alpha(f(x))
41 \end{aligned}$$
42 $f : \N \to A$ is indeed a morphism and thus an arrow.
43
44 Given two morphisms $f : \N \to A$ and $g : \N \to A$ we show that they are pointwise identical by induction over $\N$:
45 * $f(0) = a = g(0)$
46 * Given $n \in \N$:
47 $$(f \circ \mathrm{succ})(n) = (\alpha \circ f)(n) \overset{\text{ind.}}{=} (\alpha \circ g)(n) = (g \circ \mathrm{succ})(n)$$
48 </div>
49</div>