There is something about category theory that just puts me to sleep. I cannot count the number of times I picked up a category theory text, full of best intentions, started reading, and ... woke up a few hours later.
Dozens of diagrams pointing here and there don't help. It is somehow as if the abstractness of category theory is abstract in the wrong way for me.
It’s not just you. Category theory has been called “abstract nonsense” for a very long time and even referred to as such by Saunders Mac Lane [1], cofounder of the discipline itself! The subject is just very difficult to motivate because it’s so abstract that it’s hard to see the relevance of its results.
Yet its origin seems to be something quite concrete and practical.
For example, just recently I came across this text:
"Foundations of Algebraic Topology", by Eilenberg and Steenrod. Its preamble is highly readable and engaging, see below. We have a topology and compute some algebraic structure from it. Sounds easy!
------------------------------
The principal contribution of this book is an axiomatic approach to the part of algebraic topology called homology theory. It is the oldest and most extensively developed portion of algebraic topology, and may be regarded as the main body of the subject. The present axiomatization is the first which has been given. The dual theory of cohomology is likewise axiomatized.
It is assumed that the reader is familiar with the basic concepts of algebra and of point set topology. No attempt is made to axiomatize these subjects. This has been done extensively in the literature. Our achievement is different in kind. Homology theory is a transition (or function) from topology to algebra. It is this transition which is axiomatized.
Speaking roughly, a homology theory assigns groups to topological spaces and homomorphisms to continuous maps of one space into another. To each array of spaces and maps is assigned an array of groups and homomorphisms. In this way, a homology theory is an algebraic image of topology. The domain of a homology theory is the topologist's field of study. Its range is the field of study of the algebraist. Topological problems are converted into algebraic problems.
In this respect, homology theory parallels analytic geometry. How ever, unlike analytic geometry, it is not reversible. The derived algebraic system represents only an aspect of the given topological system, and is usually much simpler. This has the advantage that the geometric problem is stripped of inessential features and replaced by a familiar type of problem which one can hope to solve. It has the disadvantage that some essential feature may be lost. In spite of this, the subject has proved its value by a great variety of successful applications.
Our axioms are statements of the fundamental properties of this assignment of an algebraic system to a topological system. The axioms are categorical in the sense that two such assignments give isomorphic algebraic systems.
Eilenberg and Steenrod is great, but if you're not quite ready for algebraic topology, Mac Lane and Birkhoff's _Algebra_ [1] is an introductory abstract algebra text that makes well-motivated use of category theory throughout. From the preface:
…we hold that the general and abstract ideas needed should grow naturally from concrete instances. With this in view, it is fortunate that we do not need to begin with the general notion of a category. The most basic category is the category whose objects are all sets and whose morphisms are all functions (from one set to another); hence we can start Chapter I with sets — more accurately, with sets, functions, and the composition of functions — as the fundamental materials. On this background, Chapter II introduces the integers as the most basic example of an algebraic system. All the other categories which we need are quite "concrete" ones — each object A in the category is a set (with some structure), and each morphism from an object A to an object B in the category is a function (one which preserves the structure) on the set A to the set B. Hence we can give in Chapter I an easy, explicit definition of a "concrete" category, leaving the full treatment of the more general notion of a category to Chapter XV. In the same spirit, the idea fundamental to the notion of adjoint functor turns out to be the simple one of a "universal" construction. This idea, introduced in Chapter I for sets and in Chapter II for other concrete categories (such as monoids and lattices), is then developed with successive examples throughout the subsequent chapters.
What kind of mathematical background do you have? Despite category theory itself being entirely independent of anything else (it has pretty much no formal prerequisites for its study), without an undergraduate level knowledge of pure mathematics I imagine it’s quite hard to appreciate what’s going on and what the value of any of it is. And the deeper you get, the more it attempts to model and simplify even more ‘advanced’ branches of the subject.
Category theory doesn't have to be presented in such a diagram-heavy way. It's just that the people who love category theory also love diagrams.
I don't know one that avoids diagrams as much as possible, but the book "Abstract and Concrete Categories" is not too diagram heavy. I think the PDF is legally available online.
My main problem with these books (this one also) is that they don't take me to anything interesting I can do with categories quickly enough before I fall asleep.
It seems I have to wade through hundreds of trivial examples first.
Maybe I should write my own book about categories, that might keep me awake long enough.
Oh, maybe that is why there are so many books about category theory!
A lot of category theory is just identifying that a bunch of similar elementary results across algebra and topology can be stated and proved once in a common framework. The examples in ACC serve to show the different guises the elementary results take in different settings, as well as a source of counterexamples. I would guess this is not to your taste.
The only nontrivial theorems of general interest are the Adjoint Functor Theorems, which give very general existence proofs for universal constructions. For that, the chapter in Saunders Maclane's book is probably better.
Though it could be that none of this is worth your time. Category theory inspires intense enthusiasm from some people, but outside of a few areas of math it's not strictly necessary.
I've seen toposes declared as some fundamental notion, and I'd very much like to understand them.
Is there a short definition somewhere out there of what a topos is in terms of first-order predicate logic? Something I can understand without reading through 200 pages of preliminary material first?
I've seen statements that such a formulation in first-order logic would be misguided, because category theorists have their own notion of logic, but I'd like to understand it using my own notion of logic first.
If you understand the STLC (= simply typed lambda calculus) and why it is also a HOL (= higher-order logic) then you understand most of topoi already (although the match is not perfect).
Topos theory is a branch of mathematics which applies what programmers would call an aggressive refactoring to the category of sets and functions - a foundational workspace within which almost all of conventional math is conducted (whether the practitioners realise it or not). Math is refactored in a way reminiscent of how HOL refactors math (but constructively).
Set theory is a legacy platform like MS-DOS (!) with many limitations and anomalies which topos theory can explain and perhaps alleviate. A topos is a "virtual machine, for math ... Definitions, constructions, theorems "run" in a topos just as apps run on a VM, or SQL statements run on a database. The promise of topos theory is to cleanly separate language from implementation (just as webdesigners separate HTML from business logic) A lot of math can easily be "refactored" to apply in a much wider context.
The steps in building this refactoring are:
• Define the concept of category, a workspace of dots and composable arrows between them
• Identify the category Sets as fundamental
• Abstract out the operations and laws that make Sets useful (think CCCs (= cartesian closed categories) with some extras)
• Axiomatise a topos as a category equipped with operations obeying these laws
• Find other naturally occurring examples of topoi
• Via internal categories, understand topoi as a complete foundation for math
• Specify a language for describing constructions and deductions in a topos
Note, if you don't care about foundations, then topos theory gives you nothing new, except labour of re-learning what you already know in a new form that is awkward if you heavily rely on non-constructive reasoning.
I understand HOL, because it is just sorted first-order logic.
I also care about foundations, which is why I need to understand what a topos exactly is.
So, it seems that the steps you describe, until and including "Find other naturally occuring examples of topoi" can all be done in first-order logic set theory, is that right?
ps: for people saying topoi, do you also say thermoi as a plural for thermos?
Yep an elementary ("Lawvere-Tierney") topos is crafted to be just first order logic. 100% standrad FOL, as Category Theory is.
An elementary topos is a cartesian closed category, with finite limits and a subojbect classifier.
Cartesian closedness means that for objects A and B there is an exponential object A^B of functions from B to A. Cartesian closedness is the right intuition on functions being first class citizens and is at the center of the equivalence CCC-lambda calculus-functional programming. Limits are bread and butter categorical stuff, and the pesky subobject classifier is sort of a pain of what Category Theory understands as classifying things.
In Set, monos into X (inyections into X, subsets of X), determine the characteristic function of the subset, subset of say, U. The characteristic function is U->Bool={True, False}. Summing up, the subobject classifier in Set is Bool and provides the correspondence of functions U->X and X->Bool. In an arbitrary elementary topos, the subobject classifier would be an Ω such that monic arrows ?->X corresponds to arrows X->Ω. I would agree that this has bad digestion, maybe delving in applications one just grow accustomed.
There is an idea of one doing mathematics in an "ambient" set theory, and categorists want to look at that as an ambient category of sets. But then they asked, what are the miminum features I am really using of this ambient category of sets? The list is the requirements of a category to be an elementary topos. So the category of sets is a topos (the topos of sets) very by design. But other categories also do. When one changes Sets to other topos is when weird intepretations emerge. Topos requirements don't let you recover the axiom of choice, for instance. Excluded middle is not available anymore.
Ok, thank you. I think I will just have to sit down and write up what these conditions mean explicitly as axioms in my logic.
In general I feel category theory is a somewhat clumsy way of encoding higher-order things in a first-order way, but on the other hand I think the various type theories are not the right way to declumsify this. But that's just an impression, hopefully I will know more soon.
Makkai's work my fit: "First Order Logic with Dependent Sorts,with Applications to Category Theory"
"For instance, the definition of elementary topos (with operations defined by universal properties up to isomorphism, not specified as
univalued operations) can be given as a finite set of sentences in FOLDS."
Interesting find, but again an example of where you first need to learn some new logic FOLDS ("FOLDS has the first two of these, contexts and types (although the latter are called 'sorts'), but it does not have the third, terms (except in the rudimentary form of mere variables), and it has equality in a greatly restricted form only.").
I wonder if it is impossible to describe a topos as a normal axiom system of first-order logic, or if people are just unwilling to do it.
The logic of toposes is higher order intuitionistic logic. The logic of higher toposes is presumed to be intensional dependent type theory. The best introduction to these logics is probably the homotopy type theory book.
I cannot understand the homotopy type theory book. It just makes no sense to me, sorry.
> The logic of toposes is higher order intuitionistic logic.
Yes, I have read that a lot. Eventually, I would like to understand how toposes form a model of higher-order intuitionistic logic (which is what "The logic of toposes is higher order intuitionistic logic" probably means?). But first, I would like to understand what a topos is in first-order logic terms. You know, baby steps.
The category of sets is a topos and can be expressed/presented with first order classical logic but the general logic of toposes is intuitionistic and non-classical. There is no single topos with a single logic, each topos has its own logic and the common thread is that they're non-classical and higher order.
So are you saying that "T is a topos" cannot be expressed via first-order classical logic? Unlike something such as "G is a group", or "T is a topology" or "C is a category"?
None of your examples are expressible in first order logic either. Those are all instances of mathematical structures which can be formalized in different toposes with different logics.
Groups in the topos of sets are different from groups in the topos of smooth sets. The structure of a group can be expressed as a diagram which can then be interpreted in any topos with the prerequisite mathematical structures. Toposes have products (finite limits) so every topos can potentially have group objects just like every topos can have a natural number object which is an initial algebra (colimit) for a certain diagram.
In any case, there is no royal road and if you're not willing to spend the time and effort to learn what others have written about toposes then there isn't much I can help you with here. There are no royal roads in mathematics.
Oh, I see what you mean. You mean that for the definition of groups, topology, etc. I need to refer to a mathematical theory like set theory within first-order logic. Ok, let's do that. But then there is a definition of what "T is a topos" means, in terms of set theory based on first-order logic, right? Obviously, that definition cannot include the category of sets, because that category wouldn't be a set itself, so I am fine with considering only "small" toposes which are representable as sets, just as I am fine with just considering "small" groups, "small" topologies, and "small" categories.
So what is your question? The standard definition of a topos spells out the structural constraints for subobject classifier, finite limits, and Cartesian closure. You can write out these definitions for the topos of sets and any "small" structures in your topos which are points of the specified logical/structural variety will be small toposes internal to the topos of sets.
But there are royal roads. I mean, that is what mathematics is all about, finding those royal roads. We just may not know them yet. I doubt that topos theory is a royal road. But it is at least one of these dirty side roads I need to travel to get to the royal road.
Category theory is being applied in all sorts of domains and recently has been making some inroads in ML as well, e.g. https://arxiv.org/abs/2106.07032
Sheaves capture two properties: if you have a solution to a problem on a big piece of a space, you can shrink it to a smaller piece, and if you have solutions on small pieces of a space that agree with each other on overlaps, you can glue them together to get a solution on a bigger piece.
An easy example is a function on a set. If you have function defined on the whole set, you can shrink it to give you a function defined on a subset. If you have functions defined on several subsets, and those functions agree on the overlaps of the subsets, then you can use that to define a function on the union of the subsets. More interesting examples arise in topology and related fields.
I don’t know sheaves (except that they are a generalization of differential geometry or something?), but a great example of local to global is the fundamental theorem of calculus.
You take this property of a function that’s only defined in an arbitrarily small neighborhood of a point, and from it you can determine the function’s value anywhere else. That is, you take infinitesimally small changes (e.g. velocity) and add them up in the right way and get finite changes (e.g. distance).
It’s more interesting than it sounds because you aren’t computing a sum or something with numbers when you add up infinitesimal change. Local/infinitesimal change is in some ways a different beast than finite/global change.
Why not, they sound like similar problems and the latter would motivate computer scientists to learn about sheafs as per the approach taken in OP's book which is applied/example driven.
Dozens of diagrams pointing here and there don't help. It is somehow as if the abstractness of category theory is abstract in the wrong way for me.