From 969e0efe4176ec8df7979e3be79560cd72975750 Mon Sep 17 00:00:00 2001 From: Boris Marinov Date: Sat, 18 Feb 2023 23:41:02 +0200 Subject: [PATCH] stuff --- _chapters/02_category.md | 2 +- _chapters/06_functors.md | 141 +++++++++++++++++++++++---------------- 2 files changed, 86 insertions(+), 57 deletions(-) diff --git a/_chapters/02_category.md b/_chapters/02_category.md index 1f55d33..73886d5 100644 --- a/_chapters/02_category.md +++ b/_chapters/02_category.md @@ -377,7 +377,7 @@ For future reference, let's restate what a category is. A category is a collection of *objects* (we can think of them as *points*) and *morphisms* ( or *arrows*) that go from one object to another, where: 1. Each object has to have the identity morphism. -2. There should be a way to compose two morphisms with an appropriate type signature into a third one in a way that is *associative*. +2. There should be a way to compose two morphisms with an appropriate type signature into a third one, in a way that is *associative*. This is it. diff --git a/_chapters/06_functors.md b/_chapters/06_functors.md index 06acb25..831eaf3 100644 --- a/_chapters/06_functors.md +++ b/_chapters/06_functors.md @@ -6,7 +6,7 @@ title: Functors Functors === -From this chapter on, we will change the tactic a bit (as I am sure you are a bit tired of jumping through different subjects) and we will dive at full throttle into the world of categories, using the structures that we saw so far as context. This will allow us to generalize some of the concepts that we saw in these structures so they are valid for all categories. +From this chapter on, we will change the tactic a bit (as I am sure you are tired of jumping through different subjects) and we will dive at full throttle into the world of categories, using the structures that we saw so far as context. This will allow us to generalize some of the concepts that we examined in these structures and thus make them valid for all categories. Categories we saw so far === @@ -16,31 +16,34 @@ So far, we saw many different categories and category types. Let's review them o The category of sets --- -We began by reviewing the mother of all categories - *the category of sets* - which is not only the archetype of a category, but it contains within itself many other categories, such as the category of types in programming languages. - +We began by reviewing the mother of all categories - *the category of sets* ![The category of sets](category_sets.svg) +The category of sets contains within itself many other categories, such as the category of types in programming languages. + Special types of categories --- -We also learned about some special types of categories each of which has some distinct properties, like categories that have just one *object* (monoids, groups) and categories that have only one *morphism* between any two objects (preorders, partial orders.) +We also learned about some *special types of categories* each of which has some distinct properties, like categories that have just one *object* (monoids, groups) and categories that have only one *morphism* between any two objects (preorders, partial orders.) ![Types of categories](category_types.svg) Other categories --- -We also defined a lot of *categories based on different things*, like the ones based on logics/programming languages, but also some "less-serious ones", as for example the color-mixing partial order/category. +We also defined a lot of *categories based on different concepts*, like the ones based on logics/programming languages, but also some "less-serious ones", as for example the color-mixing partial order/category. ![Category of colors](category_color_mixing.svg) Finite categories --- -And most importantly, we saw some categories that are *completely made up*, such as my soccer player hierarchy. Those are formally called *finite categories* and, although they are not useful by themselves, the idea of finite categories is important - we can draw any combination of points and arrows and call it a category, in the same way that we can construct a set out of every combination of objects. +And most importantly, we saw some categories that are *completely made up*, such as my soccer player hierarchy. Those are formally called *finite categories*. ![Finite categories](finite_categories.svg) +Although they are not useful by themselves, the idea behind them is important - we can draw any combination of points and arrows and call it a category, in the same way that we can construct a set out of every combination of objects. + Examining some finite categories --- @@ -67,32 +70,37 @@ And finally the category $3$ has 3 objects and also 3 morphisms (one of which is Isomorphisms === -Many of the categories we saw have similarities between one another, as for example both the color-mixing order and categories that represent logic have greatest and least objects. To pinpoint such similarities and understand what they mean, it is useful to have formal ways to connect categories with one another. +Many of the categories that we saw are similar to one another, as for example both the color-mixing order and categories that represent logic have greatest and least objects. To pinpoint such similarities and understand what they mean, it is useful to have formal ways to connect categories with one another. The simplest type of connection is the good old isomorphism. Set isomorphisms --- -In chapter 1 we talked about *set isomorphisms*, which establish an equivalence between two sets. In case you have forgotten, a set isomorphism is a *two-way function* between two sets, which can alternatively be viewed as two "twin" functions each of which equals identity when composed with the other. +In chapter 1 we talked about *set isomorphisms*, which establish an equivalence between two sets. In case you have forgotten, a set isomorphism is a *two-way function* between two sets. ![Set isomorphism](set_isomorphism.svg) +It can alternatively be viewed as two "twin" functions each of which equals identity when composed with the other. + + Order isomorphisms --- -Then, in chapter 4, we encountered *order isomorphisms* and we saw that they are the same thing as set isomorphisms, but with one extra condition - aside from just being there, the functions that define the isomorphism have to preserve the order of the elements i.e. all elements have to have the same arrows pointing to and from them. Or more formally put, for any $a$ and $b$ if we have $a ≤ b$ we should also have $F(a) ≤ F(b)$ (and vise versa.) +Then, in chapter 4, we encountered *order isomorphisms* and we saw that they are like set isomorphisms, but with one extra condition - aside from just being there, the functions that define the isomorphism have to preserve the order of the object e.g. a greatest object of one order should be connected to the greatest object of the other one, a least object should be connected to a least object and same for all objects in between. ![Order isomorphism](order_isomorphism.svg) +Or more formally put, for any $a$ and $b$ if we have $a ≤ b$ we should also have $F(a) ≤ F(b)$ (and vise versa.) + Categorical isomorphisms --- -Now we will extend the definition of order isomorphisms, so it applies to categories that have more than one morphism between two objects AKA categories different from orders. This will make the definition a little more complex, but not a lot. +Now we will generalize the definition of order isomorphisms, so it also applies to all other categories (to categories that may have more than one morphism between two objects): -The definition of categorical isomorphism is the following: given two categories, an isomorphism between them is an invertible function between the underlying sets of objects, *and* an invertible function between the morphisms that connect them, which maps each morphism from one category to a morphism *with the same signature*. +> Given two categories, an isomorphism between them is an invertible function between the underlying sets of objects, *and* an invertible function between the morphisms that connect them, which maps each morphism from one category to a morphism *with the same signature*. ![Category isomorphism](category_isomorphism.svg) -If we examine it closely we will see that, although it *sounds* a bit more complex, this definition is actually the same definition as one we have for orders. It is just that morphism functions between categories that have just one morphism for any two objects, are trivial - we always map the single morphism of the source category to the single morphism of the target category (which, because of the *order-preserving* condition, is guaranteed to exist.) +If we examine it closely we will see that, although it *sounds* a bit more complex, this definition is actually the same definition as one we have for orders, it is just that the so-called "morphism functions" between categories that have just one morphism for any two objects, are trivial - we always map the single morphism of the source category to the single morphism of the target category (which is guaranteed to exist, due to the *order-preserving* condition.) ![Order isomorphism](category_order_isomorphism_2.svg) @@ -100,9 +108,9 @@ However, when we can have more than one morphism between two given objects we ne ![Category isomorphism](category_order_isomorphism.svg) -As you see, categorical isomorphisms are not hard to define, however there is another issue with them, namely that they are *very rare in practice* - the only one that comes to mind to me is the Curry-Howard-Lambek isomorphism from the last chapter, as in order for them to be isomorphic, the categories they are basically the same category. We devise a more apt way to tell if two categories are equivalent, that is also more common than categorical isomorphisms, but we will do it in the next chapter. +As you see, categorical isomorphisms are easy to define, however there is another issue with them, namely that they are *very rare in practice* (the only one that comes to mind to me is the Curry-Howard-Lambek isomorphism from the last section) as two categories that are isomorphic are basically the same category. -For now we will review a relationship that is even more abundant than isomorphisms, which are *two-way connections* between categories, namely *one-way connections* between categories, i.e. *functors*. +In the next chapter, we will see in detail why the whole concept of categorical isomorphism is not useful, and we will devise a more apt way to define a *two-way connection* between categories. But first, we will define *one-way connections* between them, i.e. *functors*. Linear functions === -Now let's talk about the "normal" functions - ones between numbers. +OK, enough with this abstract nonsence, let's talk about "normal" functions - ones between numbers. In calculus, there is this concept of *linear functions* (also called "degree one polynomials") that are sometimes defined as functions of the form $f(x) = xa$ i.e. ones that contain no operations other than multiplying the argument by some constant (designated as $a$ in the example). -But if we start plotting some such functions we will realize that there is another way to describe them - their graphs are always straight lines. +But if we start plotting some such functions we will realize that there is another way to describe them - their graphs are always comprised of straight lines. ![Linear functions](linear_functions.svg) **Question:** Why is that? -An interesting property of these functions is that most of them *preserve* addition, that is for any $x$ and $y$, you have $f(x) + f(y) = f(x + y)$. +Another interesting property of these functions is that most of them *preserve* addition, that is for any $x$ and $y$, you have $f(x) + f(y) = f(x + y)$. ![Linear functions](linear_function_functor.svg) -And if you paid attention to the functor law formula, you would already know that linear functions are just *functors between the group of natural numbers under addition and itself.* +And if you pay attention, you would know that you just saw the functor law formula. So linear functions are just *functors between the group of natural numbers under addition and itself.* (more generally, they are functors in the category of vector spaces.) **Question:** Are the two formulas we presented to define linear functions completely equivalent? @@ -361,19 +394,15 @@ but $f(x) = ax$, so $f(x) + f(y) = f(x + y)$ --> - And if we view that natural numbers as an order, linear functions are also functors as well, as all functions that are plotted with straight lines are obviously monotonic. -The above definition has one caveat: not all functions that are straight lines preserve addition - functions of the form $f(x) = x * a + b$ in which $b$ is non-zero, are also straight lines (and are also called linear in some contexts,) but they don't preserve addition. +The above definition has one caveat: not all functions that are straight lines preserve addition - functions of the form $f(x) = x * a + b$ in which $b$ is non-zero, are also straight lines (and are also called linear) but they don't preserve addition. ![Linear functions](linear_function_non_functor.svg) For those, the above formula looks like this: $f(x) + b + f(y) + b = f(x + y) + b$.