From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8340 Path: news.gmane.org!not-for-mail From: Aleks Kissinger Newsgroups: gmane.science.mathematics.categories Subject: Soundness of commutative diagram proofs Date: Thu, 25 Sep 2014 12:31:18 -0500 Message-ID: Reply-To: Aleks Kissinger NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: ger.gmane.org 1411670060 31466 80.91.229.3 (25 Sep 2014 18:34:20 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 25 Sep 2014 18:34:20 +0000 (UTC) To: categories Original-X-From: majordomo@mlist.mta.ca Thu Sep 25 20:34:15 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.127]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1XXDre-0008AN-JU for gsmc-categories@m.gmane.org; Thu, 25 Sep 2014 20:34:02 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:48879) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1XXDrJ-00027p-Mg; Thu, 25 Sep 2014 15:33:41 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1XXDrI-000295-7T for categories-list@mlist.mta.ca; Thu, 25 Sep 2014 15:33:40 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8340 Archived-At: 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/ ]