Introduction [introduction]
Introduction [introduction]
Flora
What we are trying to do
The goal of Flora is to be able to explore and explain many branches of mathematics in some “formal” way, without obscuring the math that we are actually doing. Numbers, for example, can be defined without much fuss in quite a few ways, and if you haven’t seen it, check out the Peano axioms, as they provide a pretty simple way of axiomatizing the naturals. What we are trying to do here is to give a way of “axiomatizing” things like the naturals and other mathematical objects with minimal fuss. Some fuss will be unavoidable if we want a foundation that works for multiple branches of math, but we will try to keep the ideas easy to understand for the working mathematician.
No commitments
The first big and strange idea that we find in the most common foundations of mathematics is that everything is represented as a set. This idea, while useful, obscures mathematics and allows for frankly absurd notions, which are specific to particular constructions of set theory, for example . Another issue with doing such a thing is that it forces us to think about how objects are constructed, even when this isn’t useful, making it more difficult to sit down and do math.
Then, since we aren’t making everything a set, what are we doing? The purpose of the foundations used here will be to allow different fields of mathematics to communicate with each other without specifying the “rules” of the math that will be done in any field. The way we will be doing this is by talking about objects and their relationships.
A motivating example: The natural numbers
So let’s actually start doing some math, shall we? Most of you probably have a pretty good idea of what the natural numbers are; they are the numbers , also known as the non-negative integers. The main idea behind the description of the natural numbers is that you have some first number that we represent as , then every natural number has a successor . For example, we have that . Now, for some terminology. We will think of the natural numbers, or as an object, and we say that the numbers are points of . We haven’t seen quite yet what exactly it means for something to be an object or point, but it suffices for the moment to say that an object is something that we can study, and a point is a way of specifying a particular place within that object.
The Successor
Well, we have the object , and the points of , but what is the successor? We call the successor a morphism, which is a way of taking some point in to another. So, now, to get the naturals we need some starting point , then the natural numbers are the points and so on, and we define the points The key problem now is that we don’t exclude all of the other things that could be points of . What we will do now is we will show how we can exclude all the things that we don’t want to be a part of the natural numbers. To do this, we give the natural numbers the “universal property”: if we have some sequence and a morphism that gives the next value in the sequence, then there is a unique morphism where and . We then take a point of that we don’t want in and name it , in particular it is not , or eventually a successor of . Then, since has a successor morphism, we have that are all points of . We can then show that there isn’t a unique mapping , so no longer satisfies the universal property. Since is not eventually a successor of , we can map to any and then choose the rest of the mappings so that and . In this case is not unique.
Now what if the successor loops around, as in Then we can’t map to the whole sequence.
Then we have that maps to both and , which is impossible.
Now that we have a fairly complete description of the naturals, let’s go back and figure out what a point is. First, we will define an object with the property that every object has exactly one morphism ; in particular, has only one place that can be specified. Then, if we look at morphisms from , we can see that a morphism just picks out some place in , because there is only one way to move from the place in to a particular place in . We then define points of to be these morphisms . Then we can say that is the starting point of . Then, to obtain the next point of , we compose with to get , which is , and we can continue to do this for each natural number, , , and so on, where we define to be the composition of and , with .
Now that we have some general idea of objects and morphisms, it becomes important to figure out which objects and morphisms we are considering, because different areas of mathematics will have different kinds of objects and morphisms between them. We call one of these mathematical settings, consisting of objects and the morphisms between them, a category. The information here should be enough to get us started with math, in particular, I’d recommend checking out our intro to the natural numbers. If you want to read more on categories, you can instead go check out a more formal intro to categories.