categories - Category Theory list
 help / color / mirror / Atom feed
* Soundness of commutative diagram proofs
@ 2014-09-25 17:31 Aleks Kissinger
  2014-09-25 18:44 ` ralphw
  2014-09-26  1:29 ` Adam Gal
  0 siblings, 2 replies; 3+ messages in thread
From: Aleks Kissinger @ 2014-09-25 17:31 UTC (permalink / raw)
  To: categories

A common style of proof in CT papers is to draw a huge commutative
diagram, number some subset of the faces, and justify why each of
these faces commute. However, such an argument alone doesn't imply
that the overall diagram commutes. Consider for example a triangle of
arrows with three additional arrows connecting each of the corners to
a fourth object in the centre. It is very easy to find examples where
the three little triangles commute, but not the big outside triangle.
E.g. take the three inward-pointing arrows to be 0 morphisms, then we
can take f,g,h to be arbitrary on the outside.

So, my question is:

Is there a simple way of judging soundness for a commutative diagram proof?

One answer is to determine what constitutes a legal pasting of
diagrams, then only admit those which were obtained inductively by
legal pastings of commuting faces. However, its not immediately
obvious that, given a diagram without such a decomposition into legal
pastings, we can obtain the decomposition efficiently. Has this
problem been studied formally somewhere?


Best,

Aleks


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]


^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2014-09-26  1:29 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-09-25 17:31 Soundness of commutative diagram proofs Aleks Kissinger
2014-09-25 18:44 ` ralphw
2014-09-26  1:29 ` Adam Gal

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).