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.
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 :-).
--
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.
