Quiver: A Modern Commutative Diagram Editor(github.com) |
Quiver: A Modern Commutative Diagram Editor(github.com) |
The focus on commutative diagrams, rather than a free-form canvas, is a brilliant design choice that keeps it clean and easy to use. I wish I'd had this during my thesis; it would have saved so much time.
[0] https://q.uiver.app/#q=WzAsOCxbMCwxLCJnIFxcdGV4dHsgb24gfVxcb...
Petri nets are cool. They’re sort of like if finite state machines could be multithreaded.
I first found out about petri nets when reading the writings of an organization called “statebox”. Statebox was interested in petri nets and commutative diagrams (as well as many other category theory concepts). I read some of their papers, was entranced, and it became my dream to work there. Unfortunately their homepage now is just the text “imagine being a category theorist” with a laughing-crying emoji, so I have no idea what happened to them.
[0] https://q.uiver.app/#q=WzAsNSxbMSw2LCJcXHRleHR7TmF0dXJhbCBEZ...
The Wikipedia page was too abstract for me to understand at a basic level [0].
This is a picture of a function f that takes inputs from A and produces outputs in B
f
A → B
f
A → B
↘ ↓ g
h C
Because paths through a diagram themselves compose like functions do, this notation turns out to be very natural. For example, associativity is inherent in the notation: A→B→C→D is the only way to express the composition of three functions, you can't even write the difference between (f∘g)∘h and f∘(g∘h).
It's only unwritable in a linear picture. If you wanted to make associativity visible, then you could express it in terms of commutativity using arrows that hop over nodes.
otherwise - very very very neat explanation, thanks a thousand times.
In general, a directed (multi)graph along with an account of which of its paths are and are not to be considered equivalent to each other (where this equivalence relation satisfies some basic nice properties) is known as a "category". This concept comes up ubiquitously in math/abstract logic/etc. Commutative diagrams are useful for quickly visually reasoning about equivalences of paths in such contexts.
It has various features to control and adjust these diagrams to be visually pleasing, by changing sizing/spacing/curviness/arrow style/etc of the elements within these diagrams. This is all much more convenient in its WYSIWYG interface than manually planning and coding these figures in LaTeX, as had previously been the standard way to create them for mathematical papers.
So n(g(f(•))), s(r(l(•))), s(m(f(•))) are all paths/function calls you could make to get from A to C'. Since the diagram is said to be commutative, those paths are all equal.
Being a monomoprishm, epimorphism, or isomorphism are all important properties of functions that say you're allowed to "cancel" on both sides of an equality. e.g. in general, if f(g(x))=f(h(x)), you can't conclude that g(x)=h(x). If f can be cancelled in that way, it's called a monomorphism. Similarly if g(f(x))=h(f(x)) lets you cancel the f to get g(x)=h(x), f is called an epimorphism. An isomorphism is both. This kind of thing let's you "walk backwards" along some paths in the diagram in certain situations.
One flavor of theorem you might see in category theory (like the example five lemma[0]) looks like "look at this diagram. if g is an epimorphism and h is a monomorphism then f is an isomorphism". So if I know I can cancel this way and that way, I learn I can cancel this other way.
[0] https://en.wikipedia.org/wiki/Five_lemma
> The five lemma states that, if the rows are exact, m and p are isomorphisms, l is an epimorphism, and q is a monomorphism, then n is also an isomorphism.
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.
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.
An example of a category is the "sets and functions" category. In that category, every conceivable set lives as an object (node) and every conceivable function between any two sets lives as an arrow between these two sets.
So, you can take an arrow from A to B and one from B to C and compose them like you would do with functions to get a function from A to C.
A commutative diagram would then be a subset of the whole category, where following all depicted paths between two sets X and Y would yield the same function if for each path you composed all the arrows belonging to it.
I haven't read anything on higher categories so I am not sure about pasting diagrams, but they are probably something along these lines, generalized in some way.
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.
BTW, a simpler definition of a (small) category is that it is a partial monoid.
(I’m not sure this ‘simpler definition’ is going to help!)
Your description was all abstraction, and I can't imagine would help anyone who didn't already know what we are talking about.
A concrete example would greatly help!
While I'm all for such convenience tools, I thought HN would be the place to find sympathy for the idea behind tikz-cd and its predecessors like xypic, that it's easier to write code that can be easily reproduced and programmatically manipulated than it is to try to draw (by hand, or with something like xfig), which was previously to that the standard. I guess preferences are cyclical!