Re: Soundness of commutative diagram proofs

[Adam Gal <adamgpol@gmail.com>]

Hi Aleks,

I don't have a complete answer but maybe this will help:
In your example, the problem is that your diagram has several faces on the
same plane as another face. I think if you have a diagram where this does
not happen you should be fine. E.g in your example it should have been a
tetrahedron, and then the outer triangle is just another face.

Best,
Adam

On Thursday, September 25, 2014, Aleks Kissinger <aleks0@gmail.com> 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/ ]