Hacker News new | ask | show | jobs
by solomonb 543 days ago
Its a way of demonstrating that two paths through a diagram are in some sense equal. The dots in the corners are objects and the arrows are morphisms.

To keep this simple just imagine the objects are types and the arrows are functions between those types.

You start out in the upper left corner and walk through the two paths checking the types as you go along. If the diagram typechecks correctly then it is said to commute and the two paths are in some sense equivalent. The specific sense depends on a bunch of details elided here.

1 comments

Diagrams are assumed to typecheck. The point of a commutative diagram is all the various paths you could take calling the functions to get from one spot to another give equal answers. e.g. in the Wikipedia article with the ladder looking diagram for the five lemma, going from A to C', n(g(f(a))) = s(r(l(a))) = s(m(f(a))), and likewise for any two paths that share a start and end. So it lets you write down a ton of equations in a comprehensible way.

Frequently there may be some sense in which you think of a diagram like that as a mapping from a chain of maps in the top row to a chain of maps in the bottom row, where the "mapping" is actually a list of functions linking the two chains (so all the vertical functions together map a row to another row). So it lets you wrap your head around quite complicated structures. Such things may arise for example when you have a structure described by generators with relations, and those relations themselves are described by generators with relations, which themselves have generators with relations... You get a chain of all of these relationships which "factors" the structure in some way, and then you want to study maps of your structure using maps of the chains of relationships.

Yeah I understand that the existence of the commutative diagram implies that it typechecks. I was trying to give OP a basic intuition for them. I should have said something like:

If you follow the two paths around the square you will find that everything typechecks correctly and both paths get you to the same result. This shows how the two paths are equal in some sense.