[HN Gopher] Quiver: A Modern Commutative Diagram Editor
___________________________________________________________________
Quiver: A Modern Commutative Diagram Editor
Author : peterkos
Score : 309 points
Date : 2024-12-27 05:27 UTC (17 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| sebmellen wrote:
| 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
| solomonb wrote:
| 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.
| ndriscoll wrote:
| 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.
| Chinjut wrote:
| 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.
| Chinjut wrote:
| 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.
| JadeNB wrote:
| > 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!
| qbit42 wrote:
| Quiver exports to tikz-cd for what it's worth. Not sure
| how readable the code tends to be though
| JadeNB wrote:
| Sure, no knock on the tool; it's good for people to
| choose where they want to spend their technical
| understanding. Just funny to be old enough to have seen
| some cycles firsthand.
| edflsafoiewq wrote:
| 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 f A - B
|
| and this diagram f A - B \ | g
| h C
|
| just means g [?] f = h, ie. doing f then g is the same as doing
| h. Since you write the domain and codomain of each function, it
| makes it easier to see when the functions can compose (ie. when
| it type checks).
|
| 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).
| JadeNB wrote:
| > 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.
| larodi wrote:
| 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.
| d_tr wrote:
| 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.
| d_tr wrote:
| It would help if someone could tell what's wrong in my reply.
| keithalewis wrote:
| 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.
| d_tr wrote:
| I have to admit that my first assumption was that it was
| a couple of insecure morons, I won't lie. Thanks.
| keithalewis wrote:
| It only takes one woke gatekeeper with karma to downvote
| on HN.
| xanderlewis wrote:
| You mean a monoidoid.
|
| (I'm not sure this 'simpler definition' is going to
| help!)
| CJefferson wrote:
| 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!
| geor9e wrote:
| 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.
| ndriscoll wrote:
| 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.
| sebmellen wrote:
| Thank you. Very clear and simple. I love math conceptually,
| but I wish there were more resources expressing these
| concepts in plain English!
| layer8 wrote:
| 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.
| rhymer wrote:
| This tool is fantastic! I was able to generate a Fourier-Poisson
| cube [0] in about 10 minutes, and the UI is incredibly intuitive.
|
| 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...
| atkirtland wrote:
| In case anyone else is curious about this, I found the
| reference to be Kammler's "A First Course in Fourier Analysis".
| rhymer wrote:
| 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
| 3PS wrote:
| 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.
| ChadNauseam wrote:
| 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.
| ljouhet wrote:
| https://statebox.org/what-is/ leads to https://typedefs.com/
| practal wrote:
| 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
| sundarurfriend wrote:
| A Typst export option would be wonderful to have alongside the
| LaTeX one.
| xanderlewis wrote:
| 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.
| pizza wrote:
| There's a codegen tool waiting to be built here
| atheiste wrote:
| 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.
| vouaobrasil wrote:
| 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.
| instakill wrote:
| This is amazing!
| dccsillag wrote:
| I've used Quiver a number of times now, and all of them were
| great experiences. Kudos to the authors!
___________________________________________________________________
(page generated 2024-12-27 23:00 UTC)