|
| ▲ | U4E4 5 hours ago | parent | next [-] |
| 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 |
| |
| ▲ | 5 hours ago | parent | next [-] | | [deleted] | |
| ▲ | brador 3 hours ago | parent | prev | next [-] | | We should call it “relationship lemma”. That way its function is contained within its name. And would not require the definition step every time. We should strive to name all things by their function not by their inventor or discoverer IMO. But people like their ribbons. | | |
| ▲ | wholinator2 2 hours ago | parent [-] | | In my study, it's basically never that the person names the thing after themselves. My theory goes: Often a discovery is presented in a paper by someone(s), who gives it a usually only barely passable name. For a time, only a handful of experts in the field know about it and none of them care to write general explainers for the layman. So they call it what's easy. "[Name] [concept]" because they're used to talking in names all the time. Academic experts have a large library of people's names tied to the concepts in their papers, i know my PI certainly did, every query was met with a name that had solved it to go look up. Anyways, the discussion begins with these people. Who all use the name to reference the paper which contains the result. As the discussion expand, it remains centered on this group and you have to talk _with_ them and not at them so you use the name they do. This usage slowly expands, until eventually it gets written in a textbook, taught to grad students, then to undergrads, and it becomes hopeless to change the name. I share the frustration with naming, we can come up with such better names for things now. But until we give stipend bonuses for good naming, the experts will never care to do so. But i wholeheartedly disagree that the problem as a whole can be reduced to "people like their ribbons". Naming something after yourself is so gauche and would not be tolerated in my field at least. The other professors would create a better name simply out of spite for your greed. |
| |
| ▲ | wallhz 4 hours ago | parent | prev [-] | | [dead] |
|
|
| ▲ | IsTom 3 hours ago | parent | prev | next [-] |
| I think that CT is more akin to just a different language for mathematics than a solid set of axioms from which you can prove things. The most fact-y proof I've personally seen was that you can't extend the usual definition of functions in set theory to work with parametric polymorphism (not that just some constructions won't work, but that there isn't one at all). |
|
| ▲ | tux3 5 hours ago | parent | prev | next [-] |
| 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? |
| |
|
| ▲ | throw567643u8 4 hours ago | parent | prev | next [-] |
| Just Yoneda Lemma. In fact it feels like the theory just restates Yoneda Lemma over and over in different ways. |
| |
| ▲ | azan_ 3 hours ago | parent [-] | | And the number of things you can prove using Yoneda lemma just proves how powerful category theory is. |
|
|
| ▲ | 4 hours ago | parent | prev [-] |
| [deleted] |
