| ▲ | U4E4 5 hours ago | |||||||
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... | ||||||||
| ▲ | 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. | ||||||||
| ||||||||
| ▲ | wallhz 4 hours ago | parent | prev [-] | |||||||
[dead] | ||||||||