index 1fae38d..f05747f 100644 (file)
@@ -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: <code>F(g &#8728; f) = F(g) &#8728; F(f)</code>

-*      if <code>&eta;</code> is a natural transformation from `F` to `G`, then for every <code>f:C1&rarr;C2</code> in `F` and `G`'s source category <b>C</b>: <code>&eta;[C2] &#8728; F(f) = G(f) &#8728; &eta;[C1]</code>.
+*      if <code>&eta;</code> is a natural transformation from `G` to `H`, then for every <code>f:C1&rarr;C2</code> in `G` and `H`'s source category <b>C</b>: <code>&eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]</code>.
+
+*      <code>(&eta; F)[E] = &eta;[F(E)]</code>
+
+*      <code>(K &eta;)[E} = K(&eta;[E])</code>
+
+*      <code>((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))</code>

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 <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:
+Recall that `join` is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:

<pre>
(1) join[C2] &#8728; MM(f)  =  M(f) &#8728; join[C1]
</pre>

-Next, consider the composite transformation <code>((join MG') -v- (MM &gamma;))</code>.
+Next, let <code>&gamma;</code> be a transformation from `G` to `MG'`, and
+ consider the composite transformation <code>((join MG') -v- (MM &gamma;))</code>.

-*      <code>&gamma;</code> is a transformation from `G` to `MG'`, and assigns elements `C1` in <b>C</b> a morphism <code>&gamma;\*: G(C1) &rarr; MG'(C1)</code>. <code>(MM &gamma;)</code> is a transformation that instead assigns `C1` the morphism <code>MM(&gamma;\*)</code>.
+*      <code>&gamma;</code> assigns elements `C1` in <b>C</b> a morphism <code>&gamma;\*: G(C1) &rarr; MG'(C1)</code>. <code>(MM &gamma;)</code> is a transformation that instead assigns `C1` the morphism <code>MM(&gamma;\*)</code>.

-*      `(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 &gamma;)) assigns to C1 the morphism join[MG'(C1)] &#8728; MM(&gamma;*).
</pre>

-Next, consider the composite transformation <code>((M &gamma;) -v- (join G))</code>.
+Next:

<pre>
-       (3) This assigns to C1 the morphism M(&gamma;*) &#8728; join[G(C1)].
+       (3) Consider the composite transformation <code>((M &gamma;) -v- (join G))</code>. This assigns to C1 the morphism M(&gamma;*) &#8728; join[G(C1)].
</pre>

So for every element `C1` of <b>C</b>:

<pre>
((join MG') -v- (MM &gamma;))[C1], by (2) is:
-       join[MG'(C1)] &#8728; MM(&gamma;*), which by (1), with f=&gamma;*: G(C1)&rarr;MG'(C1) is:
+       join[MG'(C1)] &#8728; MM(&gamma;*), which by (1), with f=&gamma;*:G(C1)&rarr;MG'(C1) is:
M(&gamma;*) &#8728; join[G(C1)], which by 3 is:
((M &gamma;) -v- (join G))[C1]
</pre>
@@ -329,33 +336,34 @@ So for every element `C1` of <b>C</b>:
So our **(lemma 1)** is:

<pre>
-       ((join MG') -v- (MM &gamma;))  =  ((M &gamma;) -v- (join G)), where &gamma; is a transformation from G to MG'.
+       ((join MG') -v- (MM &gamma;))  =  ((M &gamma;) -v- (join G)),
+       where as we said &gamma; is a natural transformation from G to MG'.
</pre>

-Next recall that unit is a natural transformation from `1C` to `M`. So for elements `C1` in <b>C</b>, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism <code>f:a&rarr;b</code> in <b>C</b>:
+Next recall that `unit` is a natural transformation from `1C` to `M`. So for elements `C1` in <b>C</b>, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:

<pre>
-       (4) unit[b] &#8728; f = M(f) &#8728; unit[a]
+       (4) unit[C2] &#8728; f = M(f) &#8728; unit[C1]
</pre>

-Next consider the composite transformation <code>((M &gamma;) -v- (unit G))</code>:
+Next:

<pre>
-       (5) This assigns to C1 the morphism M(&gamma;*) &#8728; unit[G(C1)].
+       (5) Consider the composite transformation ((M &gamma;) -v- (unit G)). This assigns to C1 the morphism M(&gamma;*) &#8728; unit[G(C1)].
</pre>

-Next consider the composite transformation <code>((unit MG') -v- &gamma;)</code>.
+Next:

<pre>
-       (6) This assigns to C1 the morphism unit[MG'(C1)] &#8728; &gamma;*.
+       (6) Consider the composite transformation ((unit MG') -v- &gamma;). This assigns to C1 the morphism unit[MG'(C1)] &#8728; &gamma;*.
</pre>

So for every element C1 of <b>C</b>:

<pre>
((M &gamma;) -v- (unit G))[C1], by (5) =
-       M(&gamma;*) &#8728; unit[G(C1)], which by (4), with f=&gamma;*: G(C1)&rarr;MG'(C1) is:
+       M(&gamma;*) &#8728; unit[G(C1)], which by (4), with f=&gamma;*:G(C1)&rarr;MG'(C1) is:
unit[MG'(C1)] &#8728; &gamma;*, which by (6) =
((unit MG') -v- &gamma;)[C1]
</pre>
@@ -363,7 +371,8 @@ So for every element C1 of <b>C</b>:
So our **(lemma 2)** is:

<pre>
-       (((M &gamma;) -v- (unit G))  =  ((unit MG') -v- &gamma;)), where &gamma; is a transformation from G to MG'.
+       (((M &gamma;) -v- (unit G))  =  ((unit MG') -v- &gamma;)),
+       where as we said &gamma; is a natural transformation from G to MG'.
</pre>