diff options
author | Gregor Kleen <gkleen@yggdrasil.li> | 2016-02-02 22:53:37 +0100 |
---|---|---|
committer | Gregor Kleen <gkleen@yggdrasil.li> | 2016-02-02 22:53:37 +0100 |
commit | ac417ac4f05b2f0422e6473a65a747692f130273 (patch) | |
tree | 10d472ea2c063acd670a5f7e02d6137070b343d0 /provider/posts/simmons-intro-to-cat-t | |
parent | e283971b74db4dd0c89b1d393fc2de6d6ec85a3a (diff) | |
download | dirty-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
Diffstat (limited to 'provider/posts/simmons-intro-to-cat-t')
-rw-r--r-- | provider/posts/simmons-intro-to-cat-t/1.2.md | 49 |
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 | --- | ||
2 | title: Exercises in Category Theory — 1.2 | ||
3 | published: 2016-02-02 | ||
4 | tags: Category Theory | ||
5 | --- | ||
6 | |||
7 | <div class="exercise"> | ||
8 | Let $\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> | ||