From c5b7e5a4de155dd17cdb8835034d19046ba6b757 Mon Sep 17 00:00:00 2001 From: Boris Marinov Date: Sun, 5 Mar 2023 21:27:08 +0200 Subject: [PATCH] stuff --- _chapters/05_logic.md | 50 +- _chapters/05_logic/bhk_iff.svg | 153 +++ _chapters/06_functors.md | 245 ++-- .../06_functors/category_isomorphism.svg | 1176 +++++++---------- .../category_order_isomorphism.svg | 404 +++--- .../category_order_isomorphism_2.svg | 136 +- _chapters/06_functors/chain.svg | 67 + _chapters/06_functors/constant_functor.svg | 270 ++-- _chapters/06_functors/diagram_functor.svg | 928 ++++++++----- .../06_functors/endofunctor_programming.svg | 449 ++++--- _chapters/06_functors/functor.svg | 874 ++++++------ _chapters/06_functors/functor_carnap.svg | 53 +- .../06_functors/functor_laws_composition.svg | 954 +++++++------ .../06_functors/functor_laws_identity.svg | 934 ++++++------- _chapters/06_functors/functor_morphisms.svg | 779 ++++++----- .../06_functors/functor_morphisms_formal.svg | 442 ++++--- _chapters/06_functors/functor_objects.svg | 424 +++--- _chapters/06_functors/order_isomorphism.svg | 860 ++++++------ _chapters/06_functors/set_isomorphism.svg | 534 ++++---- _chapters/06_functors/text.md | 9 - _chapters/08_adjunctions.md | 24 - .../forgetful_functors.svg | 0 .../free_forgetful_functors.svg | 0 .../free_functors.svg | 0 _chapters/09_yoneda.md | 17 + .../hom_functor.svg | 0 .../{06_functors => 09_yoneda}/hom_set.svg | 0 dictionary.txt | 10 +- index.md | 19 +- .../category_theory_2_and_3 (1).pdf | Bin .../category_theory_notes.pdf | Bin 31 files changed, 4936 insertions(+), 4875 deletions(-) create mode 100644 _chapters/05_logic/bhk_iff.svg create mode 100644 _chapters/06_functors/chain.svg delete mode 100644 _chapters/06_functors/text.md rename _chapters/{06_functors => 08_adjunctions}/forgetful_functors.svg (100%) rename _chapters/{06_functors => 08_adjunctions}/free_forgetful_functors.svg (100%) rename _chapters/{06_functors => 08_adjunctions}/free_functors.svg (100%) rename _chapters/{06_functors => 09_yoneda}/hom_functor.svg (100%) rename _chapters/{06_functors => 09_yoneda}/hom_set.svg (100%) rename category_theory_2_and_3 (1).pdf => temp/category_theory_2_and_3 (1).pdf (100%) rename category_theory_notes.pdf => temp/category_theory_notes.pdf (100%) diff --git a/_chapters/05_logic.md b/_chapters/05_logic.md index afb57a0..d7e2114 100644 --- a/_chapters/05_logic.md +++ b/_chapters/05_logic.md @@ -129,7 +129,7 @@ Classical logic. The truth-functional interpretation The above is a summary of a worldview that is due to the Greek philosopher Plato and is sometimes called Plato's *theory of forms*. Originally, the discipline of logic represents an effort to think and structure our thoughts in a way that they apply to this world of forms i.e. in a "formal" way. Today, this original paradigm of logic is known as "classical logic". Although it all started with Plato, most of it is due to the 20th century mathematician David Hilbert. -The existence of the world of forms implies that even if there are many things that we people don't know, at least *somewhere out there* there exists an answer to every question. In logic, this translates to *the principle of bivalence* that states that *each proposition is either true or false*. Due to this principle, propositions in classical logic can be aptly represented using set theory by boolean set, which contains those two values. +The existence of the world of forms implies that, even if there are many things that we, people, don't know and would not ever know, at least *somewhere out there* there exists an answer to every question. In logic, this translates to *the principle of bivalence* that states that *each proposition is either true or false*. And, due to this principle, propositions in classical logic can be aptly represented in set theory by the boolean set, which contains those two values. ![The set of boolean values](boolean_set.svg) @@ -179,7 +179,7 @@ If we are tired of diagrams, we can represent the composition diagram above as t Each proposition in classical logic can be proved with such diagrams/tables. -The and and or operations +The *and* and *or* operations --- OK, *you* know what *and* means and *I* know what it means, but what about those annoying people that want everything to be formally specified (nudge, nudge). Well we already know how we can satisfy them - we just have to construct the boolean function that represents *and*. @@ -216,7 +216,7 @@ Using those tables, we can also prove some axiom schemas we can use later: The *implies* operation --- -Let's now look into something less trivial: the *implies* operation, (also known as *entailment*). This operation binds two propositions in a way that the truth of the first one implies the truth of the second one. You can read $p → q$ as "if $p$ is true, then $q$ must also be true. +Let's now look into something less trivial: the *implies* operation, (also known as *entailment*). This operation binds two propositions in a way that the truth of the first one implies the truth of the second one (or that the first proposition is a *necessary condition* for the second.) You can read $p → q$ as "if $p$ is true, then $q$ must also be true. Entailment is also a binary function - it is represented by a function from an ordered pair of boolean values, to a boolean value. @@ -236,6 +236,30 @@ Now there are some aspects of this which are non-obvious so let's go through eve It might help you to remember that in classical logic $p → q$ ($p$ implies $q$) is true when $\neg p ∨ q$ (either $p$ is false or $q$ is true.) + +The *in and only if* operation +--- + +Now, let's review the operation that indicates that two propositions are equivalent (or, when one proposition is *a necessary and sufficient condition* for the other (which implies that the reverse is also true.)) This operation yields true when the propositions have the same value. + +| p | q | p ↔ q | +|---| --- | --- | +| True | True | True | +| True | False | False | +| False | True | False | +| False | False | True | + +But what's more interesting about this operation is that it can be constructed using the *implies* operation - it is equivalent to each of the propositions implying the other one (so $p \leftrightarrow q$ is the same as $p \to q \land q \to p$) - something which we can easily prove by comparing some truth tables. + +| p | q | p → q | q → p | p → q ∧ q → p| +|---| --- | --- | --- | --- | --- | +| True | True | True | True | True | +| True | False | False | True | False | +| False | True | True | False | False | +| False | False | True | True | True | + +Because of this, the equivalence operation is called "if and only if", or "iff" for short. + Proving results by axioms/rules of inference --- @@ -283,10 +307,10 @@ This bivalence is at the heart of what is called the Brouwer–Heyting–Kolmogo The original formulation of the BHK interpretation is not based on any particular mathematical theory. Here, we will first illustrate it using the language of set theory (just so we can abandon it a little later). -The and and or operations +The *and* and *or* operations --- -As the existence of a proof of a proposition is taken to mean that the proposition is true, the definitions of *and* is rather simple - the proof of $A ∧ B$ is just *a pair* containing a proof of $A$, and a proof of $B$ i.e. *a set-theoretic product* of the two (see chapter 2). The principle for determining whether the proposition is true or false is similar to that of primary propositions - if the pair of proofs of $A$ and $B$ exist (i.e. if both proofs exist) then the proof of $A ∧ B$ can be constructed (and so $A ∧ B$ is "true"). +As the existence of a proof of a proposition is taken to mean that the proposition is true, the definitions of *and* is rather simple - the proof of $A ∧ B$ is just *a pair* containing a proof of $A$, and a proof of $B$ i.e. *a set-theoretic product* of the two (see chapter 2). The principle for determining whether the proposition is true or false is similar to that of primary propositions - if the pair of proofs of $A$ and $B$ exist (i.e. if both proofs exist) then the proof of $A \land B$ can be constructed (and so $A \land B$ is "true"). ![And in the BHK interpretation](bhk_and.svg) @@ -295,13 +319,21 @@ As the existence of a proof of a proposition is taken to mean that the propositi The *implies* operation --- -Saying that $A$ implies $B$ ($A → B$) would just mean that there exist a function which can convert a proof of $A$ to a proof of $B$. +Now for the punchline: in the BHK interpretation, the *implies* operation is just a *function* between proofs. Saying that $A$ implies $B$ ($A \to B$) would just mean that there exist a function which can convert a proof of $A$ to a proof of $B$. ![Implies in the BHK interpretation](bhk_implies.svg) -And the *modus ponens* rule of inference is expressed by the fact that if we have a proof of $A$ we can call this function ($A → B$) to obtain a proof of $B$. +And the *modus ponens* rule of inference is nothing more than *functional application*. i.e. if we have a proof of $A$ and a function $A \to B$ we can call this function to obtain a proof of $B$. + +(In order to define this formally, we also need to define functions in terms of sets i.e. we need to have a set representing $A \to B$ for each $A$ and $B$. We will come back to this later.) + +The *if and only if* operation +--- + +In the section on classical logic, we proved that two propositions $A$ and $B$ are equivalent if $A$ implies $B$ and $B$ implies $A$. But if the *implies* operation is just a function, then proposition are equivalent precisely when the exist two functions, converting each of them to the other i.e. when the propositions are *isomorphic*. + +![Implies in the BHK interpretation](bhk_iff.svg) -(Note that in order for this to work, we also need to define the functions in terms of sets i.e. we need to have a set representing $A → B$ for each $A$ and $B$. We will come back to this later.) The *negation* operation --- @@ -309,7 +341,7 @@ The *negation* operation So according to BHK interpretation saying that $A$ is true, means that that we possess a proof of $A$ - simple enough. But it's a bit harder to express the fact that $A$ is false: it is not enough to say that we *don't have a proof* of $A$ (the fact that don't have it, doesn't mean it doesn't exist). Instead, we must show that claiming that $A$ is true leads to a *contradiction*. -To express this, intuitionistic logic defines the constant $⊥$ which plays the role of *False* (and is also known as "absurdity" or "bottom value"). $⊥$ is defined as the proof of a formula that does not have any proofs. And the equivalent of false propositions are the ones that imply that the bottom value is provable (which is a contradiction). So $¬A$ is $A → ⊥$. +To express this, intuitionistic logic defines the constant $⊥$ which plays the role of *False* (and is also known as "absurdity" or "bottom value"). $⊥$ is defined as the proof of a formula that does not have any proofs. And the equivalent of false propositions are the ones that imply that the bottom value is provable (which is a contradiction). So $¬A$ is $A \to ⊥$. In set theory, the $⊥$ constant is expressed by the empty set. diff --git a/_chapters/05_logic/bhk_iff.svg b/_chapters/05_logic/bhk_iff.svg new file mode 100644 index 0000000..a16b222 --- /dev/null +++ b/_chapters/05_logic/bhk_iff.svg @@ -0,0 +1,153 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/_chapters/06_functors.md b/_chapters/06_functors.md index 831eaf3..5ada856 100644 --- a/_chapters/06_functors.md +++ b/_chapters/06_functors.md @@ -16,15 +16,16 @@ 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* +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. +We also saw that it 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 other algebraic objects that turned out to be just *special types of categories*, 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) @@ -53,7 +54,7 @@ The simplest category is $0$ (enjoy the minimalism of this diagram.) ![The finite category 0](finite_zero.svg) -The next simplest category is $1$ - it is comprised of one object no morphism besides its identity morphism (which we we don't draw, as usual) +The next simplest category is $1$ - it is comprised of one object no morphism besides its identity morphism (which we don't draw, as usual) ![the finite category 1](finite_one.svg) @@ -67,10 +68,10 @@ And finally the category $3$ has 3 objects and also 3 morphisms (one of which is ![the finite category 3](finite_three.svg) -Isomorphisms +Categorical isomorphisms === -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. +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 a *greatest* and a *least* object. 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 such connection is the good old isomorphism. Set isomorphisms --- @@ -79,13 +80,13 @@ In chapter 1 we talked about *set isomorphisms*, which establish an equivalence ![Set isomorphism](set_isomorphism.svg) -It can alternatively be viewed as two "twin" functions each of which equals identity when composed with the other. +It can alternatively be viewed as two "twin" functions such that each of which equals identity, when composed with the other one. Order isomorphisms --- -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. +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. the greatest object of one order should be connected to the greatest object of the other one, the least object of one order should be connected to the least object of the other one, and same for all objects that are in between. ![Order isomorphism](order_isomorphism.svg) @@ -94,23 +95,36 @@ Or more formally put, for any $a$ and $b$ if we have $a ≤ b$ we should also ha Categorical isomorphisms --- -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): +Now, we will generalize the definition of an order isomorphism, so it also applies to all other categories (i.e. to categories that may have more than one morphism between two objects): -> 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 mapping between the underlying sets of objects, *and* an invertible mapping 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 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.) +After examining this definition closely, we realize that, although it *sounds* a bit more complex (and *looks* a bit messier) than the one we have for orders *it is actually the same thing*. It is just that the so-called "morphism mapping" between categories that have just one morphism for any two objects are trivial, and so we can omit them. ![Order isomorphism](category_order_isomorphism_2.svg) -However, when we can have more than one morphism between two given objects we need to make sure that each morphism in one category has a corresponding morphism in the other one. +**Question:** What are the morphism functions for orders? + + + +However, when we can have more than one morphism between two given objects, we need to make sure that each morphism in the source category has a corresponding morphism in the target one, and for this reason we need not only a mapping between the categories' objects, but one between their morphisms. ![Category isomorphism](category_order_isomorphism.svg) -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. +By the way, what we just did (taking a concept that is defined for a more narrow structure (orders) and redefining it for a more broad one (categories)) is called *generalizing* of the concept. -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*. +The problem with categorical isomorphisms +--- + +By examining them more closely, we realize that categorical isomorphisms are not so hard to define. However there is another issue with them, namely that they *don't capture the essence of what categorical equality should be*. I have devised a very good and intuitive explanation why is it the case, that this ~~margin~~ section is to narrow to contain. + +In the next chapter we will devise a more apt way to define a *two-way connection* between categories. But for this, we need to first examine *one-way connections* between them, i.e. *functors*. + +PS: Categorical isomorphisms are also *very rare in practice* - the only one that comes to mind me is the Curry-Howard-Lambek isomorphism from the previous chapter. That's because if two categories are isomorphic then there is no reason at all to treat them as different categories - they are one and the same. + Maps are functors --- -Functors are sometimes called "maps" for a good reason - maps, like all other diagrams are functors. For example, if we consider a map of different cities and roads between them categorically, then a diagram is a map of the region where the cities are located (or an index category as we dubbed it in the definition), together with a functor connectin it to the region that it represents (i.e. a mapping from the objects in the map to real-world objects.) +> A map is not the territory it represents, but, if correct, it has a similar structure to the territory, which accounts for its usefulness. Alfred Korzybski + +Functors are sometimes called "maps" for a good reason - maps, like all other diagrams, are functors. If we consider some space, containing cities and roads that we travel by, as a category, in which the cities are objects and roads between them are morphisms, then a road map can be viewed as category that represent some region of that space, together with a functor that maps the objects in the map to real-world objects. ![A map and a preorder of city pathways](preorder_map_functor.svg) -In maps, morphisms that are a result of composition are often not displayed, but we use them all the time - they are called *routes*. +In maps, morphisms that are a result of composition are often not displayed, but we use them all the time - they are called *routes*. And the law of preserving composition tells us that every route that we create on a map corresponds to a real-world route. ![A map and a preorder of city pathways](preorder_map_functor_route.svg) -The law of preserving composition tells us that the route we create on a map corresponds to a real-world route. - - -Notice that in order to be a functor, a map does not have to list *all* roads that exist in real life, and *all* travelling options ("the map is not the territory"), the only requirement is that *the roads that it lists should be actual* - this is a characteristic shared by all many-to-one relationships (i.e. functions.) - +Notice that in order to be a functor, a map does not have to list *all* roads that exist in real life, and *all* traveling options ("the map is not the territory"), the only requirement is that *the roads that it lists should be actual* - this is a characteristic shared by all many-to-one relationships (i.e. functions.) Human perception is functorial --- -As you can see from the last two chapters, we, humans, make a good use of functors in our thinking (especially considering that most of us don't know anything about them.) In my [blog post about using logic to model real-life thinking](/logic-thought)) I argue that is because human perception, human thinking is itself functorial. +We saw that, aside from being a category-theoretic concept, functors are connected to disciplines that study the human mind, like logic, linguistics, semiotics and the like. Why is it so? Recently, I wrote a [blog post about using logic to model real-life thinking](/logic-thought)) where I tackle the "unreasonable effectiveness" of functors (and "maps" in general), where I argue that is because human perception, human thinking, is functorial, that perception is just a series of functors. + +My thesis is that to perceive the world around us, we are going through a bunch of functors that go from more raw "low-level" mental models to more abstract "high-level" ones. For example, our brain creates a functor between the category of raw sensory data that we receive from our senses, to a category containing some basic model of how the world works (one that tells us where are we in space, how many objects are we seeing etc.) Then we are connecting this model to another, more abstract model, which provides us with a higher-level view of the situation that we are in, and so on. + +![Perception is functorial](chain.svg) + +You can view this as a progression from simpler to more abstract rom categories with less morphisms to categories with more morphisms - we start with the category of pieces of sensory data that have no connections between one another, and proceed to another category where some of these pieces of data are connected. Then, we transfer this structure in another category with even more connections. ![Perception is functorial](logic_thought.svg) -My thesis is that to perceive the world around us, we are creating a bunch of functors that go from more raw "low-level" maps to more abstract "high-level" ones. - -For example, our brain creates a functor between the category of raw sensory data that we receive from our senses, to a category containing some basic model of how the world works (one that tells us where are we in space, how many objects are we seeing etc.) Then we are connecting this model to another, more abstract model, which provides us with a higher-level view of the situation that we are in, and so on. - -You can view this progression of more simple to more abstract functors to a progression from categories with less morphisms to categories with more morphisms - we start with the category of pieces of sensory data that have no connections between one another, and proceed to another category where some of these pieces of data are connected. Then, we transfer this structure in another category with even more connnections. - -This is, of course, all just a speculation. But how can we check if it is true. You might say that if it were true, functors would be everywhere i.e. all mathematical objects would have functors and functors will play a significant role for them. As we will see in the next chapters, this is not far from the truth. +All this is, of course, just a speculation, but we might convince yourself that there is some basis for it, especially after we see how significant functors are for the mathematical structures that we saw before. Functors in monoids === -In group theory, there is this cool thing called *group homomorphism* (or *monoid homomorphism* when we are talking about monoids) - it is a function between the groups' underlying sets which preserves the group operation. +So, after this slight detour, we will return to our usual modus operandi: -If the time of the day right now is 00:00 o'clock (or 12 PM) then what would the time be after $n$ hours? The answer to this question can be expressed as a function with the set of integers as source and target. +Hey, do you know that in group theory, there is this cool thing called *group homomorphism* (or *monoid homomorphism* when we are talking about monoids) - it is a function between the groups' underlying sets which preserves the group operation. + +So, for example, If the time of the day right now is 00:00 o'clock (or 12 PM) then what would the time be after $n$ hours? The answer to this question can be expressed as a function with the set of integers as source and target. ![Group homomorphism as a function](group_homomorphism_function.svg) -This function is interesting - it preserves the operation of (modular) addition. That is, 13 hours from now the time will be 1 o'clock and if 14 hours from now it will be 2 o'clock, then the time after (13 + 14) hours will be (1 + 2) o'clock. - -Or to put it formally, if we call it (the function) $F$, then we have the following equation - $F(a + b) = F(a) + F(b)$ (where $+$ in the right-hand side of the equation means modular addition) Because this equation holds, the $F$ function is a *group homomorphism* between the group of integers under addition and the group of modulo arithmetic with base 11 under modular addition (where you can replace 11 with any other number.) +This function is interesting - it preserves the operation of (modular) addition: if, 13 hours from now the time will be 1 o'clock and if 14 hours from now it will be 2 o'clock, then the time after (13 + 14) hours will be (1 + 2) o'clock. ![Group homomorphism](group_homomorphism.svg) -The groups don't have to be so similar for there to be a homomorphism between them. Take, for example, the function that maps any number $n$ to 2 to the *power of $n$,* so $n \to 2ⁿ$ (here, again, you can replace 2 with any other number.) This function gives a rise to a group homomorphism between the group of integers under addition and the integers under multiplication, or $F(a + b) = F(a) * F(b)$ +Or to put it formally, if we call it (the function) $F$, then we have the following equation - $F(a + b) = F(a) + F(b)$ (where $+$ in the right-hand side of the equation means modular addition.) Because this equation holds, the $F$ function is a *group homomorphism* between the group of integers under addition and the group of modulo arithmetic with base 11 under modular addition (where you can replace 11 with any other number.) + + +The groups don't have to be so similar for there to be a homomorphism between them. Take, for example, the function that maps any number $n$ to 2 to the *power of $n$,* so $n \to 2ⁿ$ (here, again, you can replace 2 with any other number.) This function gives a rise to a group homomorphism between the group of integers under addition and the integers under multiplication, or $F(a + b) = F(a) \times F(b)$. ![Group homomorphism between different groups](group_homomorphism_addition_multiplication.svg) @@ -276,7 +297,7 @@ Wait, what were we talking about, again? Oh yeah - group homomorphisms are funct ![Group homomorphism as a functor](group_homomorphism_functor.svg) -When we view groups as one-object categories, a group homomorphism is just a functor between these categories). +It seems that when we view groups/monoid as one-object categories, a group/monoid homomorphism is just a functor between these categories. Let's see if that is the case. Object mapping --- @@ -286,27 +307,24 @@ Groups/monoids have just one object when viewed as categories, so there is also Morphism mapping --- -Because of the above, the morphism mapping is the only relevant component of the group homomorphism. In the category-theoretic perspective group objects are morphisms and so the morphism mapping is just mapping between the group's objects, as we can see in the diagram. +Because of the above, the morphism mapping is the only relevant component of the group homomorphism. In the category-theoretic perspective, group objects (like $1$ and $2$ $3$ etc.) correspond to morphisms (like $+1$, $+2$ $+3$ etc.) and so the morphism mapping is just mapping between the group's objects, as we can see in the diagram. + Functor laws --- -The first functor law trivial, it just says that the one and only identity object of the source group (which corresponds to the identity morphism of its one and only object) should be mapped to the one and only identity object of the target group. And we can see that this is the case - in our first example, $0$, the identity of the addition operation, is mapped to $0$. And in the second one $0$ is mapped to $1$ - the identity object of the multiplication operation. +The first functor law trivial, it just says that the one and only identity object of the source group (which corresponds to the identity morphism of its one and only object) should be mapped to the one and only identity object of the target group. -As we said, in order for a function to be a group homomorphism, it must satisfy the equation -$F(a + b) = F(a) \times F(b)$ (where the $+$ and $\times$ operators are arbitrary.) And if you remember that, when interpreted categorically, group objects (like $1$ and $2$ $3$ etc.) correspond to morphisms (like $+1$, $+2$ $+3$ etc.) and the monoid operation of combining two objects corresponds to *functional composition*, you would see that this equation is actually a just a formulation of the second functor law: $F(g•f) = F(g)•F(f)$. +And if we remember that the group operation of combining two objects corresponds to *functional composition* if we view groups as categories, we realize that the group homomorphism equation $F(a + b) = F(a) \times F(b)$ is just a formulation of the second functor law: $F(g•f) = F(g)•F(f)$. And many algebraic operations satisfy this equation, for example the functor law for the group homomorphism between $n \to 2ⁿ$ is just the famous algebraic rule, stating that $gᵃ gᵇ= gᵃ⁺ᵇ$. **Task:** Although it's trivial, we didn't prove that the first functor law (the one about the preservation of identities always holds. Interestingly enough, for groups/monoids it actually follows from the second law. Try to prove that. Start with the definition of the identity function. - - - Functors in orders === -And now let's talk about one concept that is completely unrelated to functors, nudge-nudge (hey, bad jokes are better than no jokes at all, right?) In the theory of orders, we have the concept of functions between orders (which is unsurprising, given that orders, like monoids/groups, are based on sets.) One very interesting type of such function, which has applications in calculus and analysis, is a *monotonic function* (also called *monotone map*) - this is a function between two orders that *preserves the order of the objects in the source order, in the target order. So a function $F$ is monotonic when for every $a$ and $b$ in the source order, if $a ≤ b$ then $F(a) ≤ F(b)$. +And now let's talk about a concept that is completely unrelated to functors, nudge-nudge (hey, bad jokes are better than no jokes at all, right?) In the theory of orders, we have the concept of functions between orders (which is unsurprising, given that orders, like monoids/groups, are based on sets) and one very interesting type of such function, which has applications in calculus and analysis, is a *monotonic function* (also called *monotone map*) - this is a function between two orders that *preserves the order of the objects in the source order, in the target order. So a function $F$ is monotonic when for every $a$ and $b$ in the source order, if $a ≤ b$ then $F(a) ≤ F(b)$. For example, the function that maps the current time to the distance traveled by some object is monotonic because the distance traveled increases (or stays the same) as time increases. @@ -333,7 +351,7 @@ Functor laws It is not hard to see that monotone maps obey the first functor law as identities are the only morphisms that go between a given object and itself. -And the second law ($F(g•f) = F(g)•F(f)) also follows trivially: both morphisms $F(g•f)$ and $F(g)•F(f)$ have the same type signature - so for example if we take the signature of $f$ and $g$ to be $f :: a \to b$ and $g :: b \to c$, then they both would go from $F(a)$ and $F(c)$. But because in orders there can be just one morphism between $F(a)$ and $F(c)$ so these two morphisms must be equal to one another. +And the second law ($F(g•f) = F(g)•F(f)$) also follows trivially: both morphisms $F(g•f)$ and $F(g)•F(f)$ have the same type signature. But because in orders there can be just one morphism with a given type signature, these two morphisms must be equal to one another. **Task:** Expand the proof. @@ -355,7 +373,7 @@ But because in orders there can be just one morphism between $F(a)$ and $F(c)$ s Linear functions === -OK, enough with this abstract nonsence, let's talk about "normal" functions - ones between numbers. +OK, enough with this abstract nonsense, 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). @@ -365,12 +383,10 @@ But if we start plotting some such functions we will realize that there is anoth **Question:** Why is that? -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)$. +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)$. We already know that this equation is equivalent to the second functor law. So linear functions are just *functors between the group of natural numbers under addition and itself.* As we will see later, they are example of functors in the *category of vector spaces*. ![Linear functions](linear_function_functor.svg) -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?