On Sat, Apr 7, 2012 at 7:45 PM, Tom Bachmann <[email protected]> wrote: > On 07.04.2012 16:38, Sergiu Ivanov wrote: >> >> On Fri, Apr 6, 2012 at 12:00 PM, Tom Bachmann<[email protected]> wrote: >>> >>> >>> Let me first say that it would be quite amazing to have sympy code to >>> check >>> commutativity of diagrams. However, I think there is a reason that "no" >>> computer programs for category theory exist so far: most proofs in >>> category >>> theory are trivial! As soon as you have formalized your diagram enough to >>> put it into a computer, it should be obvious how to prove commutativity. >> >> >> According to my experience, this is just untrue. >> >> As an example, I attach a (rather old, but still good) book on >> category theory. Take a look at the theorem on page 36. I must >> confess I found it very hard to check the commutativity of those >> diagrams. Note though that the diagrams I refer to are still rather >> small, I've caught glimpses of yet larger diagrams (not that much, >> though). >> >> Now, the commutativity of these diagrams is based on the commutativity >> of some other diagrams, which are introduced in the previous sections >> of the book. >> > > Hm. It seems my perspective on category theory is indeed skewed towards > applications. I have seen some horrendous diagrams, but only in settings > where the desired method of proof is diagram chasing.
I see. Diagram chasing is a very cool thing, I would be very glad to give it a try at implementing. Is it OK if I add this point to my proposal on the wiki and post a corresponding comment on Melange? :-) >> Actually, reading the very book I suggest as an example was what gave >> me the idea of checking the commutativity of a diagram automatically. >> >> I would be very interested in finding out what your category theoretic >> background is. By what you say, I suspect that category theory was >> shown to you as an instrument to formulate stuff already proved in >> certain concrete categories. What you say about algebraic geometry, >> commutative algebra and algebraic topology is not really (pure) >> category theoretic reasoning. When one defines concrete morphisms, >> this becomes an application of category theoretical language and >> (sometimes) results. On the other hand, in abstract categories there >> are a number of (very important) results which are formulated and >> checked via commutative diagrams. While I state this without citing >> anything, you may still take a look at the book I attach to see that >> there at least is a lot of stuff done via commutative diagrams :-) >> > > You are very right. I admit defeat on this one :-). Yay :-) Thank you for your feedback! Sergiu -- You received this message because you are subscribed to the Google Groups "sympy" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
