cat theory tweaks

[lambda.git] / advanced_topics / monads_in_category_theory.mdwn

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index 8c5f4cd..3e34f85 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -82,12 +82,11 @@ A **functor** is a "homomorphism", that is, a structure-preserving mapping, betw
 <pre>
          (i) associate with every element C1 of <b>C</b> an element F(C1) of <b>D</b>
 
 <pre>
          (i) associate with every element C1 of <b>C</b> an element F(C1) of <b>D</b>
 

-        (ii) associate with every morphism f:C1&rarr;C2 of <b>C</b> a morphism
-             F(f):F(C1)&rarr;F(C2) of <b>D</b>
+        (ii) associate with every morphism f:C1&rarr;C2 of <b>C</b> a morphism F(f):F(C1)&rarr;F(C2) of <b>D</b>

 
        (iii) "preserve identity", that is, for every element C1 of <b>C</b>:
 
        (iii) "preserve identity", that is, for every element C1 of <b>C</b>:

-             F of C1's identity morphism in <b>C</b> must be the identity morphism
-                 of F(C1) in <b>D</b>: F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.
+             F of C1's identity morphism in <b>C</b> must be the identity morphism of F(C1) in <b>D</b>:
+             F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.

 
         (iv) "distribute over composition", that is for any morphisms f and g in <b>C</b>:
              F(g &#8728; f) = F(g) &#8728; F(f)
 
         (iv) "distribute over composition", that is for any morphisms f and g in <b>C</b>:
              F(g &#8728; f) = F(g) &#8728; F(f)


@@ -105,17 +104,21 @@ Natural Transformation
 ----------------------
 So categories include elements and morphisms. Functors consist of mappings from the elements and morphisms of one category to those of another (or the same) category. **Natural transformations** are a third level of mappings, from one functor to another.
 
 ----------------------
 So categories include elements and morphisms. Functors consist of mappings from the elements and morphisms of one category to those of another (or the same) category. **Natural transformations** are a third level of mappings, from one functor to another.
 

-Where `G` and `H` are functors from category <b>C</b> to category <b>D</b>, a natural transformation &eta; between `G` and `H` is a family of morphisms &eta;[C1]:G(C1)&rarr;H(C1)` in <b>D</b> for each element `C1` of <b>C</b>. That is, &eta;[C1]` has as source `C1`'s image under `G` in <b>D</b>, and as target `C1`'s image under `H` in <b>D</b>. The morphisms in this family must also satisfy the constraint:
+Where `G` and `H` are functors from category <b>C</b> to category <b>D</b>, a natural transformation &eta; between `G` and `H` is a family of morphisms <code>&eta;[C1]:G(C1)&rarr;H(C1)</code> in <b>D</b> for each element `C1` of <b>C</b>. That is, <code>&eta;[C1]</code> has as source `C1`'s image under `G` in <b>D</b>, and as target `C1`'s image under `H` in <b>D</b>. The morphisms in this family must also satisfy the constraint:

 
 

-       for every morphism f:C1&rarr;C2 in <b>C</b>: &eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]
+<pre>
+       for every morphism f:C1&rarr;C2 in <b>C</b>:
+       &eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]
+</pre>

 
 

-That is, the morphism via `G(f)` from `G(C1)` to `G(C2)`, and then via &eta;[C2]` to `H(C2)`, is identical to the morphism from `G(C1)` via &eta;[C1]` to `H(C1)`, and then via `H(f)` from `H(C1)` to `H(C2)`.
+That is, the morphism via `G(f)` from `G(C1)` to `G(C2)`, and then via <code>&eta;[C2]</code> to `H(C2)`, is identical to the morphism from `G(C1)` via <code>&eta;[C1]</code> to `H(C1)`, and then via `H(f)` from `H(C1)` to `H(C2)`.

 
 
 How natural transformations compose:
 
 Consider four categories <b>B</b>, <b>C</b>, <b>D</b>, and <b>E</b>. Let `F` be a functor from <b>B</b> to <b>C</b>; `G`, `H`, and `J` be functors from <b>C</b> to <b>D</b>; and `K` and `L` be functors from <b>D</b> to <b>E</b>. Let &eta; be a natural transformation from `G` to `H`; &phi; be a natural transformation from `H` to `J`; and &psi; be a natural transformation from `K` to `L`. Pictorally:
 
 
 
 How natural transformations compose:
 
 Consider four categories <b>B</b>, <b>C</b>, <b>D</b>, and <b>E</b>. Let `F` be a functor from <b>B</b> to <b>C</b>; `G`, `H`, and `J` be functors from <b>C</b> to <b>D</b>; and `K` and `L` be functors from <b>D</b> to <b>E</b>. Let &eta; be a natural transformation from `G` to `H`; &phi; be a natural transformation from `H` to `J`; and &psi; be a natural transformation from `K` to `L`. Pictorally:
 

+<pre>

        - <b>B</b> -+ +--- <b>C</b> --+ +---- <b>D</b> -----+ +-- <b>E</b> --
                 | |        | |            | |
         F: -----&rarr; G: -----&rarr;     K: -----&rarr;
        - <b>B</b> -+ +--- <b>C</b> --+ +---- <b>D</b> -----+ +-- <b>E</b> --
                 | |        | |            | |
         F: -----&rarr; G: -----&rarr;     K: -----&rarr;


@@ -126,39 +129,52 @@ Consider four categories <b>B</b>, <b>C</b>, <b>D</b>, and <b>E</b>. Let `F` be
                 | |        | |  v         | |
                 | |    J: -----&rarr;         | |
        -----+ +--------+ +------------+ +-------
                 | |        | |  v         | |
                 | |    J: -----&rarr;         | |
        -----+ +--------+ +------------+ +-------

+</pre>

 
 

-Then `(&eta; F)` is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `b1` is an element of category <b>B</b>, `(&eta; F)[b1] = &eta;[F(b1)]`---that is, the morphism in <b>D</b> that &eta; assigns to the element `F(b1)` of <b>C</b>.
+Then <code>(&eta; F)</code> is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `B1` is an element of category <b>B</b>, <code>(&eta; F)[B1] = &eta;[F(B1)]</code>---that is, the morphism in <b>D</b> that <code>&eta;</code> assigns to the element `F(B1)` of <b>C</b>.

 
 

-And `(K &eta;)` is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category <b>C</b>, `(K &eta;)[C1] = K(&eta;[C1])`---that is, the morphism in <b>E</b> that `K` assigns to the morphism &eta;[C1]` of <b>D</b>.
+And <code>(K &eta;)</code> is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category <b>C</b>, <code>(K &eta;)[C1] = K(&eta;[C1])</code>---that is, the morphism in <b>E</b> that `K` assigns to the morphism <code>&eta;[C1]</code> of <b>D</b>.

 
 
 
 

-`(&phi; -v- &eta;)` is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where `f:C1&rarr;C2`:
+<code>(&phi; -v- &eta;)</code> is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where <code>f:C1&rarr;C2</code>:

 
 

+<pre>

        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = &phi;[C2] &#8728; H(f) &#8728; &eta;[C1]
        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = &phi;[C2] &#8728; H(f) &#8728; &eta;[C1]

+</pre>

 
 

-by naturalness of &phi;, is:
+by naturalness of <code>&phi;</code>, is:

 
 

+<pre>

        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]
        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]

+</pre>

 
 

-by naturalness of &eta;, is:
+by naturalness of <code>&eta;</code>, is:

 
 

+<pre>

        &phi;[C2] &#8728; &eta;[C2] &#8728; G(f) = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]
        &phi;[C2] &#8728; &eta;[C2] &#8728; G(f) = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]

+</pre>

 
 

-Hence, we can define `(&phi; -v- &eta;)[x]` as: &phi;[x] &#8728; &eta;[x]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
+Hence, we can define <code>(&phi; -v- &eta;)[x]</code> as: <code>&phi;[x] &#8728; &eta;[x]</code> and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:

 
 

+<pre>

        (&phi; -v- &eta;)[C2] &#8728; G(f) = J(f) &#8728; (&phi; -v- &eta;)[C1]
        (&phi; -v- &eta;)[C2] &#8728; G(f) = J(f) &#8728; (&phi; -v- &eta;)[C1]

+</pre>

 
 An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
 
 
 An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
 

+<pre>

        ((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))
        ((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))

+</pre>

 
 I'll assert without proving that vertical composition is associative and has an identity, which we'll call "the identity transformation."
 
 
 
 I'll assert without proving that vertical composition is associative and has an identity, which we'll call "the identity transformation."
 
 

-`(&psi; -h- &eta;)` is natural transformation from the (composite) functor `KG` to the (composite) functor `LH`; this is known as a "horizontal composition." It's trickier to define, but we won't be using it here. For reference:
+<code>(&psi; -h- &eta;)</code> is natural transformation from the (composite) functor `KG` to the (composite) functor `LH`; this is known as a "horizontal composition." It's trickier to define, but we won't be using it here. For reference:

 
 

+<pre>

        (&phi; -h- &eta;)[C1]  =  L(&eta;[C1]) &#8728; &psi;[G(C1)]
                                           =  &psi;[H(C1)] &#8728; K(&eta;[C1])
        (&phi; -h- &eta;)[C1]  =  L(&eta;[C1]) &#8728; &psi;[G(C1)]
                                           =  &psi;[H(C1)] &#8728; K(&eta;[C1])

+</pre>

 
 Horizontal composition is also associative, and has the same identity as vertical composition.
 
 
 Horizontal composition is also associative, and has the same identity as vertical composition.