It is a common situation that given a set of commutative diagrams one needs to establish commutativity of another set of diagrams. The naive approach to the problem is to partition each diagram into smaller diagrams, so that each subdiagram is in the given set of commutative diagrams.
In the talk I will show how by using the notion of decreasing diagrams, one can prove an existence of such a partition instead of producing an explicit partition. Of course this is enough to attest the commutativity of the diagram in question.
The decreasing diagrams were introduced by Klop, van Oostrom, and de Vrijer in the article "A geometric proof of confluence by decreasing diagrams, J.Logic Comput. 10 (2000), no. 3, 437--460", for a purpose of proving confluence of rewriting systems. It was observed for a long time that confluence of rewriting systems should be related to coherence results in category theory. The decreasing diagrams make this relation rather explicit.