Soundness of commutative diagram proofs

Soundness of commutative diagram proofs

[Aleks Kissinger]

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

Re: Soundness of commutative diagram proofs

[ralphw]

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

Re: Soundness of commutative diagram proofs

[Adam Gal]

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