Quiver - Trình chỉnh sửa sơ đồ giao hoán hiện đại

 (github.com/varkor)
1 điểm bởi GN⁺ 2024-12-28 | 1 bình luận | Chia sẻ qua WhatsApp
  • Quiver là trình chỉnh sửa để tạo sơ đồ giao hoán và sơ đồ dán bằng giao diện đồ họa, hỗ trợ kết xuất chất lượng cao để hiển thị trên màn hình và xuất sang LaTeX·Typst
  • Việc tạo và chỉnh sửa sơ đồ nhanh hơn nhiều so với viết LaTeX hoặc Typst thủ công; khi đã quen, tốc độ thao tác có thể gần như dùng bút và giấy
  • Có thể xử lý các sơ đồ phức tạp như pullback, pushout, adjunction, higher cell, đồng thời cung cấp lưới linh hoạt tự điều chỉnh theo kích thước nhãn và các kiểu mũi tên có thể kết hợp
  • Có thể thao tác bằng cả kéo thả chuột lẫn phím tắt, hỗ trợ chọn nhiều mục, hoàn tác·làm lại, macro người dùng, xuất sơ đồ nhúng HTML, pan·zoom
  • Khi xuất sang LaTeX hoặc Typst, liên kết tới sơ đồ cũng được chèn kèm để sau này có thể mở lại chỉnh sửa hoặc chia sẻ với người khác

Quiver làm gì

  • Quiver là trình chỉnh sửa đồ họa hiện đại để tạo sơ đồ giao hoán và sơ đồ dán
  • Kết xuất các sơ đồ chất lượng cao, đẹp khi xem trên màn hình; có thể xuất LaTeX thông qua tikz-cd, và xuất Typst thông qua fletcher
  • Có thể dùng thử trực tiếp trên web tại q.uiver.app
  • Cách sử dụng hiệu quả cũng như cách tạo và chỉnh sửa sơ đồ chỉ bằng bàn phím được tổng hợp trong hướng dẫn Quiver

Tính năng vẽ sơ đồ

  • Cung cấp giao diện hiệu quả và trực quan để tạo các sơ đồ giao hoán phức tạp và sơ đồ dán
  • Các ví dụ được hỗ trợ gồm
    • sơ đồ có pullback và pushout
    • adjunction
    • higher cell
  • Việc bố trí đối tượng dựa trên lưới linh hoạt điều chỉnh theo kích thước nhãn
  • Mũi tên có thể kết hợp nhiều kiểu khác nhau
  • Có thể dùng màu cho nhãn và mũi tên
  • Được thiết kế để trông đẹp cả trong ảnh chụp màn hình, đồng thời kết quả xuất ra LaTeX·Typst cũng giống sơ đồ gốc nhất có thể

Cách nhập liệu và quy trình chỉnh sửa

  • Có thể tạo và chỉnh sửa sơ đồ bằng cách nhấp·kéo chuột
  • Cung cấp bộ phím tắt cho phép thực hiện mọi thao tác, nên cũng có thể chỉnh sửa chủ yếu bằng bàn phím
  • Có thể chọn nhiều phần tử cùng lúc để thay đổi hàng loạt một cách dễ dàng và nhanh chóng
  • Hệ thống lịch sử cho phép hoàn tác·làm lại thao tác
  • Hỗ trợ pan và zoom để xử lý các sơ đồ lớn
  • Cung cấp căn chỉnh nhãn thông minh và edge offset

Xuất và tái sử dụng

  • Có thể xuất sơ đồ sang LaTeX hoặc Typst
  • Kết quả xuất có chứa liên kết để quay lại sơ đồ đó
    • Có thể mở lại khi cần chỉnh sửa về sau
    • Có thể chia sẻ với người khác
  • Cũng hỗ trợ xuất sơ đồ có thể nhúng vào HTML
  • Macro tùy chỉnh của người dùng có thể được dùng bằng cách dán URL của tệp chứa \newcommand
  • Tích hợp với trình chỉnh sửa có thể xem trong tài liệu Editor integration và Quiver wiki

Điều kiện build và chạy

  • Sau khi chạy make trên dòng lệnh, có thể mở src/index.html trong trình duyệt để kiểm tra kết quả build
  • Nếu phiên bản Make hoặc Bash không phù hợp, có thể tải thủ công bản phát hành KaTeX mới nhất và đặt dưới src/KaTeX/
  • Nếu đường dẫn KaTeX không đúng, lỗi tải KaTeX sẽ xảy ra
  • Quiver phải được chạy thông qua localhost
  • Nếu đã cài Python, có thể chạy make serve trong thư mục Quiver rồi mở localhost:8000 trong trình duyệt
  • Nếu gặp vấn đề khi build, có thể mở GitHub issue kèm nội dung sự cố

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-12-28
Ý kiến trên Hacker News

  • Công cụ này thật sự tuyệt vời. Tôi đã tạo được khối lập phương Fourier-Poisson [0] chỉ trong khoảng 10 phút, và UI cũng rất trực quan
    Việc thiết kế tập trung vào biểu đồ giao hoán thay vì canvas tự do là một lựa chọn xuất sắc, giúp công cụ gọn gàng và dễ dùng. Giá mà hồi viết luận văn tôi có công cụ này thì chắc đã tiết kiệm được rất nhiều thời gian
    [0] https://q.uiver.app/#q=WzAsOCxbMCwxLCJnIFxcdGV4dHsgb24gfVxcb...

    • Với những ai quan tâm đến phần này, A First Course in Fourier Analysis của Kammler có vẻ là tài liệu tham khảo phù hợp

  • Cùng mạch này, gần đây tôi thấy trình chỉnh sửa Petri net này khá ấn tượng: https://pes.vsb.cz/petrineteditor/#/model
    Petri net rất thú vị. Nếu biến máy trạng thái hữu hạn thành đa luồng thì cảm giác sẽ gần như thế này
    Lần đầu tôi biết đến Petri net là khi đọc bài viết của một tổ chức tên “statebox”. Statebox quan tâm đến Petri net, biểu đồ giao hoán và nhiều khái niệm trong lý thuyết phạm trù; sau khi đọc vài bài báo, tôi bị cuốn hút đến mức từng mơ được làm việc ở đó. Tiếc là hiện trang chủ chỉ còn dòng “imagine being a category theorist” cùng emoji cười ra nước mắt, nên tôi không biết đã xảy ra chuyện gì

  • Vài ngày trước, tôi đã dùng công cụ này để vẽ một biểu đồ đơn giản [0] đưa vào sách của mình [1]
    Đáng tiếc là vì nó chuyên cho lý thuyết phạm trù nên không hỗ trợ nhiều việc trang trí node cho đẹp, nhưng dĩ nhiên vẫn có thể xử lý bằng LaTeX
    [0] https://q.uiver.app/#q=WzAsNSxbMSw2LCJcXHRleHR7TmF0dXJhbCBEZ...
    [1] http://abstractionlogic.com

  • Tối qua tôi đang dùng https://tikzcd.yichuanshen.de/; nó giống như một phiên bản ít tính năng hơn của công cụ này. Dù vậy, để tạo biểu đồ đơn giản thì vẫn khá ổn

  • Bạn có thể giải thích cho một nhà phát triển phần mềm khiêm tốn và trình độ cũng không mấy cao như tôi biết biểu đồ giao hoán và biểu đồ dán là gì không?
    Bài Wikipedia quá trừu tượng để hiểu ở mức cơ bản [0]
    [0]: https://en.wikipedia.org/wiki/Commutative_diagram

    • Nó chỉ là một cách viết cho đẹp các phương trình giữa các hàm, hoặc những thứ khác có thể hợp thành như hàm
      Nếu có f trên A → B thì đó biểu thị hàm f nhận đầu vào từ A và tạo đầu ra thuộc B
      Một sơ đồ trong đó A → B là f, từ đó B → C là g, và A → C là h có nghĩa là g ∘ f = h, tức là làm f rồi làm g thì giống với làm h. Vì viết kèm miền xác định và đối miền của từng hàm, nên dễ thấy các hàm có thể hợp thành hay không, tức là có qua được kiểm tra kiểu hay không
      Bản thân các đường đi trong sơ đồ cũng hợp thành như hàm, nên ký pháp này khớp một cách rất tự nhiên. Ví dụ, luật kết hợp được tích hợp sẵn vào chính ký pháp, nên A→B→C→D là cách biểu diễn duy nhất của việc hợp thành ba hàm, và thậm chí không thể viết ra sự khác biệt giữa (f∘g)∘h và f∘(g∘h)
    • Biểu đồ giao hoán là một tập các cạnh có hướng giữa các nút, tức một đồ thị có hướng, kèm thêm khẳng định rằng bất kỳ hai đường đi nào bắt đầu từ cùng một nút và kết thúc ở cùng một nút đều được xem là tương đương theo một nghĩa nào đó
      Nói chung, nếu một đa đồ thị có hướng được gắn kèm mô tả về những đường đi nào trong đó tương đương hay không tương đương với nhau, và quan hệ tương đương này thỏa một vài tính chất cơ bản, thì nó được gọi là một phạm trù. Khái niệm này xuất hiện rất thường xuyên trong toán học, logic trừu tượng, v.v. Trong bối cảnh đó, biểu đồ giao hoán hữu ích để suy luận nhanh bằng trực quan về tính tương đương của các đường đi
    • Mỗi chữ hoa là một kiểu, và mỗi chữ thường là một hàm từ kiểu này sang kiểu khác. Nếu đi theo một đường trong sơ đồ, ta có thể nói về nhiều lời gọi hàm. Ví dụ, đi theo f rồi g rồi n biểu thị n(g(f(a))). Đó là sơ đồ; còn nói sơ đồ giao hoán nghĩa là nếu đi theo bất kỳ hai đường nào có cùng điểm bắt đầu và điểm kết thúc thì chúng bằng nhau
      Vì vậy n(g(f(•))), s(r(l(•))), s(m(f(•))) đều là các đường đi từ A đến C' và cũng là các lời gọi hàm; vì đã nói sơ đồ giao hoán nên tất cả các đường đi này đều bằng nhau
      Đơn cấu, toàn cấu, đẳng cấu đều là những tính chất quan trọng của hàm, cho phép “khử” một hạng nào đó ở hai vế của đẳng thức. Ví dụ, nói chung từ f(g(x))=f(h(x)) không thể kết luận g(x)=h(x). Nếu có thể khử f theo cách này thì gọi là đơn cấu. Tương tự, nếu trong g(f(x))=h(f(x)) có thể khử f để thu được g(x)=h(x) thì f là toàn cấu. Đẳng cấu thỏa cả hai. Nhờ các tính chất này, trong một số tình huống có thể “đi ngược” một phần các đường đi trong sơ đồ
      Một dạng định lý có thể thấy trong lý thuyết phạm trù là kiểu như five lemma[0]: “hãy nhìn sơ đồ này. Nếu g là toàn cấu và h là đơn cấu thì f là đẳng cấu”. Tức là nếu biết có thể khử ở phía này và phía kia, thì ta cũng biết có thể khử ở một phía khác
      [0] https://en.wikipedia.org/wiki/Five_lemma

      five lemma nói rằng nếu các hàng là dãy khớp, m và p là đẳng cấu, l là toàn cấu và q là đơn cấu, thì n cũng là đẳng cấu

    • Đó là cách cho thấy hai đường đi qua sơ đồ là giống nhau theo một nghĩa nào đó. Các điểm ở góc là đối tượng, còn mũi tên là cấu xạ
      Nếu muốn nghĩ đơn giản, có thể xem đối tượng là kiểu, và mũi tên là hàm giữa các kiểu
      Bắt đầu từ góc trên bên trái, đi theo hai đường và kiểm tra kiểu. Nếu sơ đồ kiểm tra kiểu đúng thì nói là giao hoán, và hai đường đi tương đương theo một nghĩa nào đó. Ý nghĩa cụ thể phụ thuộc vào nhiều chi tiết bị lược bỏ ở đây
    • Đọc định nghĩa về phạm trù sẽ có ích. Nó rất trừu tượng, nhưng khá đơn giản vì chỉ có vài tiên đề
      Một ví dụ về phạm trù là phạm trù “tập hợp và hàm”. Trong phạm trù đó, mọi tập hợp có thể nghĩ tới đều là đối tượng, tức nút, và mọi hàm có thể nghĩ tới giữa hai tập hợp bất kỳ đều là mũi tên giữa hai tập hợp đó
      Vì vậy nếu lấy một mũi tên từ A đến B và một mũi tên từ B đến C rồi hợp thành chúng như hàm, ta sẽ nhận được một hàm từ A đến C
      Có thể xem biểu đồ giao hoán là một tập con của toàn bộ phạm trù, và đó là trường hợp khi đi theo mọi đường được vẽ giữa hai tập hợp X và Y rồi hợp thành các mũi tên trên từng đường thì đều cho ra cùng một hàm
      Tôi chưa từng đọc về phạm trù bậc cao nên không chắc về biểu đồ dán, nhưng có lẽ rất có thể đó là một sự tổng quát hóa ý tưởng này theo cách nào đó

  • Có thể xuất ra định dạng thân thiện với web không? Có lẽ SVG là đúng. Nếu chạy quiver trên localhost thì chia sẻ bằng liên kết không phải là một lựa chọn

  • Khi học môn lý thuyết phạm trù vài năm trước, Quiver thực sự là thứ không thể thiếu. UI gọn gàng, trực quan và tính năng cũng đủ dùng. So với việc vật lộn với TikZ thì không có gì phải bàn

  • Đây là một sản phẩm rất tốt. Trước đây tôi thường viết tay mã TikZ và cũng khá nhanh, nhưng giờ đã quên nhiều rồi nên có vẻ công cụ này sẽ rất hữu ích cho biểu đồ giao hoán

  • Ở đây ẩn chứa một công cụ sinh mã đáng để làm

  • Tôi đã dùng Quiver nhiều lần và lần nào trải nghiệm cũng tốt. Những người tạo ra nó thật tuyệt