From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8341 Path: news.gmane.org!not-for-mail From: ralphw@bakermountain.org Newsgroups: gmane.science.mathematics.categories Subject: Re: Soundness of commutative diagram proofs Date: Thu, 25 Sep 2014 14:44:12 -0400 (EDT) Message-ID: References: Reply-To: ralphw@bakermountain.org NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain;charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1411726373 25115 80.91.229.3 (26 Sep 2014 10:12:53 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 26 Sep 2014 10:12:53 +0000 (UTC) Cc: categories@mta.ca To: "Aleks Kissinger" Original-X-From: majordomo@mlist.mta.ca Fri Sep 26 12:12:48 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 1XXSW8-00073o-5X for gsmc-categories@m.gmane.org; Fri, 26 Sep 2014 12:12:48 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:50009) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1XXSVX-000581-Cj; Fri, 26 Sep 2014 07:12:11 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1XXSVX-0007Rk-4p for categories-list@mlist.mta.ca; Fri, 26 Sep 2014 07:12:11 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8341 Archived-At: The notions of Q-sequences and, more generally, Q-trees from "Categories Allegories" by Freyd and Scedrov may answer your question. Sincerely, Ralph Wojtowicz Baker Mountain Research Corporation P.O. Box 68 Yellow Spring, WV 26865 email: ralphw@bakermountain.org phone: 304-874-4161 web : www.bakermountain.org On Thu, September 25, 2014 1:31 pm, Aleks Kissinger wrote: > 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/ ]