Introduction [foundations/introduction]
Introduction [foundations/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 havn’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 (since trying to have a foundation that works for multiple branches of math will undoubtably create some), while also trying to keep them easy to understand for the working mathematician.
No commitments
The first big, and strange idea that we find in the most common of formal 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 the 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 lets 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 havn’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 in some sense a thing that belongs to 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 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. The key problem now, is that we dont exclude all of the other things that could be points of , like for example, which would then also include and so on. So, how do we remove all of these “bad” points? Well, we need to make sure that and it’s successors create the entirety of . To do this, we give the natural numbers the “universal property”, that if we have some object with some starting point , and a morphism , then there is exactly one morphism where and . Informally, if we have some starting value, lets say , and some rule from going from going from a value to the next, say , then there is exactly one way to “map” the natural numbers to the following sequence
while respecting the starting point of and the successor.
Now we can check to see if can exist. Suppose has , then there is more than one “map” from the pi sequence to the sequence as shown below.
Now what if the natural numbers 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, lets 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 . Then if we look at morphism’s from , we can see than a morphism just picks out some point in , and thus we can define points of X 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 one, 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, which consist of objects and the morphisms between them a category.