Quiver: A Modern Commutative Diagram Editor(github.com)
github.com
Quiver: A Modern Commutative Diagram Editor
https://github.com/varkor/quiver
39 comments
In case anyone else is curious about this, I found the reference to be Kammler's "A First Course in Fourier Analysis".
You're right, thanks for pointing that out. I missed adding the reference: Kammler DW. A First Course in Fourier Analysis. 2nd ed. Cambridge University Press; 2008. Figure 1.19. This visualization of the relationships between time and frequency domains is a good illustration of Pontryagin duality applied to signal processing
In the same kind of vein: I was recently very impressed by this pretri net editor https://pes.vsb.cz/petrineteditor/#/model
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.
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.
Just used this a few days ago to draw a simple diagram [0] for my book [1]!
Unfortunately, because it is for category theory only, it doesn't have much support for prettifying your nodes, but you can do that with the latex, of course.
[0] https://q.uiver.app/#q=WzAsNSxbMSw2LCJcXHRleHR7TmF0dXJhbCBEZ...
[1] http://abstractionlogic.com
[0] https://q.uiver.app/#q=WzAsNSxbMSw2LCJcXHRleHR7TmF0dXJhbCBEZ...
[1] http://abstractionlogic.com
I was using https://tikzcd.yichuanshen.de/ last night, which is basically a less feature-filled version of this. It’s quite nice for doing simple diagrams, though.
Can anyone explain what "commutative and pasting diagrams" are to a humble (and not very good) software writer?
The Wikipedia page was too abstract for me to understand at a basic level [0].
[0]: https://en.wikipedia.org/wiki/Commutative_diagram
The Wikipedia page was too abstract for me to understand at a basic level [0].
[0]: https://en.wikipedia.org/wiki/Commutative_diagram
They're just a nice way of writing equations between functions (or other things that compose like functions).
This is a picture of a function f that takes inputs from A and produces outputs in B
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).
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).
is it common/allowed to have set types instead of the A/B/C symbols? or the A/B/C simply implies the sets differ, because functions did something to them? I mean - can you write N, R, C... ?
otherwise - very very very neat explanation, thanks a thousand times.
otherwise - very very very neat explanation, thanks a thousand times.
> 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.
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.
Each capital letter is a type and each lower case letter is a function from one type to another. You can trace a path in the diagram to talk about a bunch of function calls (e.g following f then g then n represents n(g(f(a)))). This is called a diagram. Then the statement that a diagram is commutative says that if you trace any two paths that share a start and end, they are equal.
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.
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.
I wouldn’t say that the paths are equal. They are different paths, because they consist of different edges going through different nodes. It’s the composite end-to-end functions that result from the paths that are equal.
Thank you. Very clear and simple. I love math conceptually, but I wish there were more resources expressing these concepts in plain English!
Wikipedia pages for niche STEM topics tend to be made by 1 or 2 people, obsessed with the topic, but often not very good at high level abstract communication. So you get a technically-correct mess like that article. If you are an expert in a niche stem topic, look up the wikipedia article for it, then use that experience to fight the Gell-Mann Amnesia effect for the rest. I use wikipedia for a lot of topics, but not topics like this. An LLM is a better bet these days.
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.
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.
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.
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.
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.
A commutative diagram is just a collection of nodes and directed edges between nodes (aka, a directed graph), but it's a directed graph along with the claim that any two paths in this graph which start at the same node and end at the same node are to be considered equivalent, in some sense.
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.
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.
Note that Quiver isn't really a tool just for drawing "commutative diagrams". It's a tool for drawing any labeled system of nodes and edges/arrows between nodes, whether or not this is to be interpreted as a commutative diagram. (It also allows drawing arrows which start or end at other arrows, rather than at nodes).
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.
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.
> 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.
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!
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!
[deleted]
[deleted]
It would help if you read the definition of a category. It is very abstract but also pretty simple with just a couple of axioms.
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.
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.
It would help if someone could tell what's wrong in my reply.
You made a completely obvious and true statement starting with "It would help..." That seems to be frowned upon on HN.
BTW, a simpler definition of a (small) category is that it is a partial monoid.
BTW, a simpler definition of a (small) category is that it is a partial monoid.
You mean a monoidoid.
(I’m not sure this ‘simpler definition’ is going to help!)
(I’m not sure this ‘simpler definition’ is going to help!)
d_tr(1)
I didn't downvote you, but honestly, it doesn't really help understand what commuting diagrams are. I use them all the time, and never use category theory.
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!
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!
Is there a possibility to export in a web-friendly format? I guess SVG would be it? If I ran quiver in localhost then sharing via a link is not an option.
Quiver was absolutely indispensable when I did a category theory course a few years ago. The UI was clean, intuitive, and featureful. Compared to banging one's head against Tikz, it's absolutely no contest.
Very nice product! In the past I usually wrote TikZ code by hand and it was pretty fast but now I forgot a lot of that stuff and this could be very useful for commutative diagrams.
There's a codegen tool waiting to be built here
I've used Quiver a number of times now, and all of them were great experiences. Kudos to the authors!
A Typst export option would be wonderful to have alongside the LaTeX one.
This is amazing!
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...