Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Quiver: A Modern Commutative Diagram Editor

github.com

Post reply on HN
Print view View original

31–40 of 40 posts

Re: Quiver: A Modern Commutative Diagram Editor

#31

Post by JadeNB »

qbit42 wrote: post #30
JadeNB wrote: post #29

Earlier quoted context omitted.

> 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 progr…

Quiver exports to tikz-cd for what it’s worth. Not sure how readable the code tends to be though

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.

Re: Quiver: A Modern Commutative Diagram Editor

#32

Post by ljouhet »

ChadNauseam wrote: post #14

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 conc…

https://statebox.org/what-is/ leads to https://typedefs.com/

Re: Quiver: A Modern Commutative Diagram Editor

#33

Post by geor9e »

sebmellen wrote: post #2

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

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.

Re: Quiver: A Modern Commutative Diagram Editor

#34

Post by rhymer »

atkirtland wrote: post #26
rhymer wrote: post #9

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...

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

Re: Quiver: A Modern Commutative Diagram Editor

#35

Post by ndriscoll »

solomonb wrote: post #3
sebmellen wrote: post #2

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

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 com…

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.

Re: Quiver: A Modern Commutative Diagram Editor

#36

Post by ndriscoll »

sebmellen wrote: post #2

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

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.

Re: Quiver: A Modern Commutative Diagram Editor

#37

Post by sebmellen »

ndriscoll wrote: post #36
sebmellen wrote: post #2

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

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(•)…

Thank you. Very clear and simple. I love math conceptually, but I wish there were more resources expressing these concepts in plain English!

Re: Quiver: A Modern Commutative Diagram Editor

#38

Post by layer8 »

ndriscoll wrote: post #36
sebmellen wrote: post #2

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

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(•)…

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.

Re: Quiver: A Modern Commutative Diagram Editor

#39

Post by larodi »

edflsafoiewq wrote: post #5
sebmellen wrote: post #2

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

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 (i…

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.

Re: Quiver: A Modern Commutative Diagram Editor

#40

Post by solomonb »

ndriscoll wrote: post #35
solomonb wrote: post #3

Earlier quoted context omitted.

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 com…

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 eq…

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.

Post reply on HN