Re: Soundness of commutative diagram proofs

[ralphw@bakermountain.org]

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/ ]