From 704abdbe4afe78e553738662a3cb0bb6944b54ff Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 2 Nov 2010 11:26:23 -0400 Subject: [PATCH] cat theory tweaks Signed-off-by: Jim Pryor --- advanced_topics/monads_in_category_theory.mdwn | 43 ++++++++++++++++---------- 1 file changed, 26 insertions(+), 17 deletions(-) diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index 1fae38d1..f05747f6 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -288,22 +288,29 @@ Let's remind ourselves of some principles: * functors "distribute over composition", that is for any morphisms `f` and `g` in `F`'s source category: `F(g ∘ f) = F(g) ∘ F(f)` -* if `η` is a natural transformation from `F` to `G`, then for every `f:C1→C2` in `F` and `G`'s source category C: `η[C2] ∘ F(f) = G(f) ∘ η[C1]`. +* if `η` is a natural transformation from `G` to `H`, then for every `f:C1→C2` in `G` and `H`'s source category C: `η[C2] ∘ G(f) = H(f) ∘ η[C1]`. + +* `(η F)[E] = η[F(E)]` + +* `(K η)[E} = K(η[E])` + +* `((φ -v- η) F) = ((φ F) -v- (η F))` Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas. -Recall that join is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in C, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism `f:C1→C2` in C: +Recall that `join` is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in C, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism `f:C1→C2` in C:
``` 	(1) join[C2] ∘ MM(f)  =  M(f) ∘ join[C1]
```
-Next, consider the composite transformation `((join MG') -v- (MM γ))`. +Next, let `γ` be a transformation from `G` to `MG'`, and + consider the composite transformation `((join MG') -v- (MM γ))`. -* `γ` is a transformation from `G` to `MG'`, and assigns elements `C1` in C a morphism `γ\*: G(C1) → MG'(C1)`. `(MM γ)` is a transformation that instead assigns `C1` the morphism `MM(γ\*)`. +* `γ` assigns elements `C1` in C a morphism `γ\*: G(C1) → MG'(C1)`. `(MM γ)` is a transformation that instead assigns `C1` the morphism `MM(γ\*)`. -* `(join MG')` is a transformation from `MMMG'` to `MMG'` that assigns `C1` the morphism `join[MG'(C1)]`. +* `(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`. Composing them: @@ -311,17 +318,17 @@ Composing them: (2) ((join MG') -v- (MM γ)) assigns to C1 the morphism join[MG'(C1)] ∘ MM(γ*). -Next, consider the composite transformation `((M γ) -v- (join G))`. +Next:
```-	(3) This assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
+	(3) Consider the composite transformation `((M γ) -v- (join G))`. This assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
```
So for every element `C1` of C:
``` 	((join MG') -v- (MM γ))[C1], by (2) is:
-	join[MG'(C1)] ∘ MM(γ*), which by (1), with f=γ*: G(C1)→MG'(C1) is:
+	join[MG'(C1)] ∘ MM(γ*), which by (1), with f=γ*:G(C1)→MG'(C1) is:
M(γ*) ∘ join[G(C1)], which by 3 is:
((M γ) -v- (join G))[C1]
```
@@ -329,33 +336,34 @@ So for every element `C1` of C: So our **(lemma 1)** is:
```-	((join MG') -v- (MM γ))  =  ((M γ) -v- (join G)), where γ is a transformation from G to MG'.
+	((join MG') -v- (MM γ))  =  ((M γ) -v- (join G)),
+	where as we said γ is a natural transformation from G to MG'.
```
-Next recall that unit is a natural transformation from `1C` to `M`. So for elements `C1` in C, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism `f:a→b` in C: +Next recall that `unit` is a natural transformation from `1C` to `M`. So for elements `C1` in C, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism `f:C1→C2` in C:
```-	(4) unit[b] ∘ f = M(f) ∘ unit[a]
+	(4) unit[C2] ∘ f = M(f) ∘ unit[C1]
```
-Next consider the composite transformation `((M γ) -v- (unit G))`: +Next:
```-	(5) This assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].
+	(5) Consider the composite transformation ((M γ) -v- (unit G)). This assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].
```
-Next consider the composite transformation `((unit MG') -v- γ)`. +Next:
```-	(6) This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
+	(6) Consider the composite transformation ((unit MG') -v- γ). This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
```
So for every element C1 of C:
``` 	((M γ) -v- (unit G))[C1], by (5) =
-	M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*: G(C1)→MG'(C1) is:
+	M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*:G(C1)→MG'(C1) is:
unit[MG'(C1)] ∘ γ*, which by (6) =
((unit MG') -v- γ)[C1]
```
@@ -363,7 +371,8 @@ So for every element C1 of C: So our **(lemma 2)** is:
```-	(((M γ) -v- (unit G))  =  ((unit MG') -v- γ)), where γ is a transformation from G to MG'.
+	(((M γ) -v- (unit G))  =  ((unit MG') -v- γ)),
+	where as we said γ is a natural transformation from G to MG'.
```
-- 2.11.0