I think it is pretty obvious that at the challenge with all abstract mathematics in general and the category theory in particular isnt the fact that people dont understand what a "linear order" is, but the fact it is so distant from daily routine that it seems completely pointless. It's like pouring water over pefectly smooth glass
Is there a "mind-blowing fact" about category theory? Like the first time I've heard that one can prove there is no analytical solution for a polynomial equation with a degree > 5 with group theory, it was mind-blowing. What's the counterpart of category theory?
A thing is its relationships. (Yoneda lemma.) Keep track of how an object connects to everything else, and you’ve recovered the object itself, up to isomorphism. It’s why mathematicians study things by probing them: a group by its actions, a space by the maps into it, a scheme in algebraic geometry defined as the rule for what maps into it look like. (You do need the full pattern of connections, not just a list — two different rings can have the same modules, for instance.) [0]
Writing a program and proving a theorem are the same act. (Curry–Howard–Lambek.) For well-behaved programs, every program is a proof of something and every proof is a program. The match is exact for simple typed languages and leaks a bit once you add general recursion (an infinite loop “proves” anything in Haskell), but the underlying identity is real. Lambek added the third leg: these are also morphisms in a category. [1]
Algebra and geometry are one thing wearing different costumes. (Stone duality and cousins.) A system of equations and the shape it cuts out aren’t related, they’re the same object seen from opposite sides. Grothendieck rebuilt algebraic geometry on this idea, with schemes (so you can do geometry on the integers themselves) and étale cohomology (topological invariants for shapes with no actual topology). His student Deligne used that machinery to settle the Weil conjectures in 1974. Wiles’s Fermat proof lives in the same world, though it leans on much more than the categorical foundations. [2]
First of all, I hope we all appreciate how fundamentally anti-intellectual this is! You are judging an entire field of mathematics based on its ability to provide bite-sized infotainment.
Secondly, it's really not correct to say "one can prove [the unsolvability of the quintic]....with group theory." The group in question did not pop out of nowhere, it comes first from some field theory, then ordered set theory. In fact historically the proof of the Abel-Ruffini theorem was impossibly convoluted precisely because it was attempted on purely group-theoretic terms, leaving the Galois correspondence tacit and unspecified. The theorem really doesn't make sense without seriously engaging with extension fields. It's hard to think of a "purely group-theoretic" fact that would blow laypeople's minds. Maybe the sporadic simple groups.
More generally, group theory was invented to solve problems which had plagued medieval mathematicians and some of its ideas can be explained in terms familiar to 21st-century high schoolers. Individual groups are very concrete. Category theory was invented to clarify certain confusions and tacit assumptions of 20th century mathematicians, and individual categories are very abstract. As someone who knows a lot of 20th-century mathematics, I think it's really cool that almost every "intuitively natural" transformation can be formalized as a canonical morphism between objects in a certain category, so I'm not just stupidly turning a crank like I did as an undergrad. But I had to get a BS in mathematics to appreciate all that.
For the HN crowd, it's cool that categories were invented to study common abstractions in algebraic topology, but viewed as a purely symbolic/combinatorial exercise it forms a universal computational model like Turing machines and lambda calculus. Maybe it's not "mind-blowing" but it's surprising, and helps us build better tools like Rust and Lean. (I don't think the Rust devs thought much about category theory. The OCaml devs certainly did, and Rust inherited that work.)
Sure, category theory can't prove the unsolvability of the quintic. But did you know that a monad is really just a monoid object in the monoidal category of endofunctors on the category of types of your favorite language?
There is a way to frame category theory such that it's all just arrows -- by associating the identity arrow (which all objects have by definition) with the object itself. In a sense, the object is syntactic sugar.
Unless there's some idiosyncratic meaning for the `=>`, the Antisymmetry one basically says `Orange -> Yellow => Yellow -/> Orange`. The diagram is not acurate. The prose is very imprecise. "It also means that no ties are permitted - either I am better than my grandmother at soccer or she is better at it than me." NO. Antisymmetry doesn't exclude `x = y`. Ties are permitted in the equality case. Antisymmetry for a non-strict order says that if both directions hold, the two elements must in fact be the same element. The author is describing strict comparison or total comparability intuition, not antisymmetry.
I don't think they are completely wrong - "=>" is just implication. A hidden assumption in their diagrams is that circles of different colours are assumed to be different elements.
A morphism from orange to yellow means "O <= Y". From this, antisymmetry (and the hidden assumption) implies that "Y not <= O".
Totality is just the other way around (all two distinct elements are comparable in one direction).
If this is meant to be an explainer, that can't be simply implicit. The text actually seems full of imprecise claims, such as:
"All diagrams that look something different than the said chain diagram represent partial orders"
"The different linear orders that make up the partial order are called chains"
The Birkhoff theorem statement, which is materially wrong. A finite distributive lattice is not isomorphic to "the inclusion order of its join-irreducible elements".
I think the last 10% is exactly where the useful part is, at least for programmers.
In a preorder seen as a category, there is at most one arrow between any two objects. So every diagram commutes and uniqueness is basically free. Then products and coproducts stop looking like magic diagrams and become something very familiar: greatest lower bounds and least upper bounds.
Small nit: preorders are thin categories, but posets are the skeletal thin categories. In a preorder you can have distinct a and b with both a <= b and b <= a, which means they are isomorphic, not literally the same. Quotienting by that equivalence gives you the poset.
The software angle is the part I find most useful. This kind of bugs shows up when we force a total order onto something that is only partially ordered, or only preordered. Dependency graphs, versions, permissions, type hierarchies, CRDT states, rule specificity, build steps. A lot of these don’t really want a comparator and a sort. Sometimes they want a quotient, a topological sort, a join, or just the honest answer that two things are not comparable.
That feels like the practical lesson here: category theory is not always adding abstraction. Sometimes it is just a good way to stop pretending two different structures are the same thing.
I think it is pretty obvious that at the challenge with all abstract mathematics in general and the category theory in particular isnt the fact that people dont understand what a "linear order" is, but the fact it is so distant from daily routine that it seems completely pointless. It's like pouring water over pefectly smooth glass
Is there a "mind-blowing fact" about category theory? Like the first time I've heard that one can prove there is no analytical solution for a polynomial equation with a degree > 5 with group theory, it was mind-blowing. What's the counterpart of category theory?
A thing is its relationships. (Yoneda lemma.) Keep track of how an object connects to everything else, and you’ve recovered the object itself, up to isomorphism. It’s why mathematicians study things by probing them: a group by its actions, a space by the maps into it, a scheme in algebraic geometry defined as the rule for what maps into it look like. (You do need the full pattern of connections, not just a list — two different rings can have the same modules, for instance.) [0]
Writing a program and proving a theorem are the same act. (Curry–Howard–Lambek.) For well-behaved programs, every program is a proof of something and every proof is a program. The match is exact for simple typed languages and leaks a bit once you add general recursion (an infinite loop “proves” anything in Haskell), but the underlying identity is real. Lambek added the third leg: these are also morphisms in a category. [1]
Algebra and geometry are one thing wearing different costumes. (Stone duality and cousins.) A system of equations and the shape it cuts out aren’t related, they’re the same object seen from opposite sides. Grothendieck rebuilt algebraic geometry on this idea, with schemes (so you can do geometry on the integers themselves) and étale cohomology (topological invariants for shapes with no actual topology). His student Deligne used that machinery to settle the Weil conjectures in 1974. Wiles’s Fermat proof lives in the same world, though it leans on much more than the categorical foundations. [2]
[0] https://en.wikipedia.org/wiki/Yoneda_lemma
[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
[2] https://en.wikipedia.org/wiki/Stone_duality
Just Yoneda Lemma. In fact it feels like the theory just restates Yoneda Lemma over and over in different ways.
First of all, I hope we all appreciate how fundamentally anti-intellectual this is! You are judging an entire field of mathematics based on its ability to provide bite-sized infotainment.
Secondly, it's really not correct to say "one can prove [the unsolvability of the quintic]....with group theory." The group in question did not pop out of nowhere, it comes first from some field theory, then ordered set theory. In fact historically the proof of the Abel-Ruffini theorem was impossibly convoluted precisely because it was attempted on purely group-theoretic terms, leaving the Galois correspondence tacit and unspecified. The theorem really doesn't make sense without seriously engaging with extension fields. It's hard to think of a "purely group-theoretic" fact that would blow laypeople's minds. Maybe the sporadic simple groups.
More generally, group theory was invented to solve problems which had plagued medieval mathematicians and some of its ideas can be explained in terms familiar to 21st-century high schoolers. Individual groups are very concrete. Category theory was invented to clarify certain confusions and tacit assumptions of 20th century mathematicians, and individual categories are very abstract. As someone who knows a lot of 20th-century mathematics, I think it's really cool that almost every "intuitively natural" transformation can be formalized as a canonical morphism between objects in a certain category, so I'm not just stupidly turning a crank like I did as an undergrad. But I had to get a BS in mathematics to appreciate all that.
For the HN crowd, it's cool that categories were invented to study common abstractions in algebraic topology, but viewed as a purely symbolic/combinatorial exercise it forms a universal computational model like Turing machines and lambda calculus. Maybe it's not "mind-blowing" but it's surprising, and helps us build better tools like Rust and Lean. (I don't think the Rust devs thought much about category theory. The OCaml devs certainly did, and Rust inherited that work.)
Sure, category theory can't prove the unsolvability of the quintic. But did you know that a monad is really just a monoid object in the monoidal category of endofunctors on the category of types of your favorite language?
There is a way to frame category theory such that it's all just arrows -- by associating the identity arrow (which all objects have by definition) with the object itself. In a sense, the object is syntactic sugar.
Unless there's some idiosyncratic meaning for the `=>`, the Antisymmetry one basically says `Orange -> Yellow => Yellow -/> Orange`. The diagram is not acurate. The prose is very imprecise. "It also means that no ties are permitted - either I am better than my grandmother at soccer or she is better at it than me." NO. Antisymmetry doesn't exclude `x = y`. Ties are permitted in the equality case. Antisymmetry for a non-strict order says that if both directions hold, the two elements must in fact be the same element. The author is describing strict comparison or total comparability intuition, not antisymmetry.
I don't think they are completely wrong - "=>" is just implication. A hidden assumption in their diagrams is that circles of different colours are assumed to be different elements.
A morphism from orange to yellow means "O <= Y". From this, antisymmetry (and the hidden assumption) implies that "Y not <= O".
Totality is just the other way around (all two distinct elements are comparable in one direction).
If this is meant to be an explainer, that can't be simply implicit. The text actually seems full of imprecise claims, such as:
"All diagrams that look something different than the said chain diagram represent partial orders"
"The different linear orders that make up the partial order are called chains"
The Birkhoff theorem statement, which is materially wrong. A finite distributive lattice is not isomorphic to "the inclusion order of its join-irreducible elements".
The first 90% of this is standard set theory.
I'm unclear what the last 10% of 'category theory' gives us.
I think the last 10% is exactly where the useful part is, at least for programmers.
In a preorder seen as a category, there is at most one arrow between any two objects. So every diagram commutes and uniqueness is basically free. Then products and coproducts stop looking like magic diagrams and become something very familiar: greatest lower bounds and least upper bounds.
Small nit: preorders are thin categories, but posets are the skeletal thin categories. In a preorder you can have distinct a and b with both a <= b and b <= a, which means they are isomorphic, not literally the same. Quotienting by that equivalence gives you the poset.
The software angle is the part I find most useful. This kind of bugs shows up when we force a total order onto something that is only partially ordered, or only preordered. Dependency graphs, versions, permissions, type hierarchies, CRDT states, rule specificity, build steps. A lot of these don’t really want a comparator and a sort. Sometimes they want a quotient, a topological sort, a join, or just the honest answer that two things are not comparable.
That feels like the practical lesson here: category theory is not always adding abstraction. Sometimes it is just a good way to stop pretending two different structures are the same thing.