String diagrams

Stream: general

[Yuma Mizuno]

String diagrams are graphical representations of morphisms in monoidal categories, which are extremely useful for rewriting computations. They are also related to e.g. knot theory.

I have written a program that draws string diagrams from lean expressions. This is avalable in branch#ymizuno-string.
string.png

The program depends on ProofWidgets, and in particular inspired by CommDiag.lean, which is written by @Wojciech Nawrocki.

I will be happy if this helps anyone in writing proofs involving monoidal categories. Suggestions and comments are welcome!

[Bolton Bailey]

I have been interested in using string diagrams for cryptography. Can you tell me: Is it possible to replicate the proof depicted in figure 6 of this paper using this string diagram system?

[Yuma Mizuno]

Bolton Bailey said:

I have been interested in using string diagrams for cryptography. Can you tell me: Is it possible to replicate the proof depicted in figure 6 of this paper using this string diagram system?

Yes, I think it's possible. In fact, my main motivation was to provide a tool to help with such "graphical rw".

[Kyle Miller]

It would be neat if this let you work with string diagrams in a similar manner as Globular. (https://ncatlab.org/nlab/show/Globular http://globular.science/)

Globular uses a different sort of formalization (associative n-categories), but, at least, a nice feature would be if you could select certain elements of the string diagram and have the tool insert all the coherence maps, etc., to bring them all "into one place" so that you can rewrite that subdiagram.

[Kim Morrison]

I think globular has been replaced by homotopy.io

[Bolton Bailey]

I am currently livestreaming my attempt at the diagrammatic proof from the paper I linked. I have come to the following goal:

C: Type u
inst✝¹: Category.{v, u} C
inst✝: MonoidalCategory C
XYZ: C
R: (V₁ V₂ : C) → V₁ ⊗ V₂ ⟶ V₂ ⊗ V₁
V₁V₂V₃V₄V₅V₆V₇V₈V₉: C
⊢ (V₅ ⊗ V₆) ⊗ V₇ ⊗ V₈ ⟶ (V₅ ⊗ V₇) ⊗ V₆ ⊗ V₈

I want to do this in the obvious way: Using R to switch theV6 and V7 with lots of associativity on either side. Is there a tactic that solves this kind of category theoretic goal?

[Yaël Dillies]

The tactic that uses the attribute reassoc although I have forgotten its name

[Bolton Bailey]

ac_change?

[Kevin Buzzard]

Does this thread help? (tl;dr: slice)

[Bolton Bailey]

Kevin Buzzard said:

Does this thread help? (tl;dr: slice)

This seems like it is more for categorical composition than monoidal-categorical tensoring

[Yuma Mizuno]

Bolton Bailey said:

I am currently livestreaming my attempt at the diagrammatic proof from the paper I linked. I have come to the following goal:

C: Type u
inst✝¹: Category.{v, u} C
inst✝: MonoidalCategory C
XYZ: C
R: (V₁ V₂ : C) → V₁ ⊗ V₂ ⟶ V₂ ⊗ V₁
V₁V₂V₃V₄V₅V₆V₇V₈V₉: C
⊢ (V₅ ⊗ V₆) ⊗ V₇ ⊗ V₈ ⟶ (V₅ ⊗ V₇) ⊗ V₆ ⊗ V₈

I want to do this in the obvious way: Using R to switch theV6 and V7 with lots of associativity on either side. Is there a tactic that solves this kind of category theoretic goal?

We can use docs#Mathlib.Tactic.Coherence.monoidalComp to do this.

import Mathlib.Tactic.CategoryTheory.Coherence

open CategoryTheory
open scoped MonoidalCategory

universe v u

variable {C : Type u} [Category.{v} C] [MonoidalCategory C]

def R' (V₅ V₆ V₇ V₈ : C) (R : (V₁ V₂ : C) → V₁ ⊗ V₂ ⟶ V₂ ⊗ V₁) :
    (V₅ ⊗ V₆) ⊗ V₇ ⊗ V₈ ⟶ (V₅ ⊗ V₇) ⊗ V₆ ⊗ V₈ :=
  𝟙 _ ⊗≫ V₅ ◁ R V₆ V₇ ▷ V₈ ⊗≫ 𝟙 _

[Yuma Mizuno]

By the way the string diagram widget does not support monoidalComp at the moment, so we need to expand it to show the string diagram.

[Yuma Mizuno]

The following works in branch#ymizuno-string.

import Mathlib.Tactic.Widget.StringDiagram
import ProofWidgets.Component.Panel.SelectionPanel
import Mathlib.Tactic.CategoryTheory.Coherence

/-! ## Example use of string diagram widgets -/

section MonoidalCategory

open ProofWidgets
open CategoryTheory
open MonoidalCategory

universe v u

variable {C : Type u} [Category.{v} C] [MonoidalCategory C]

example (V₅ V₆ V₇ V₈ : C) (R : (V₁ V₂ : C) → V₁ ⊗ V₂ ⟶ V₂ ⊗ V₁)
    (x : (V₅ ⊗ V₆) ⊗ V₇ ⊗ V₈ ⟶ (V₅ ⊗ V₇) ⊗ V₆ ⊗ V₈) :
    𝟙 _ ⊗≫ V₅ ◁ R V₆ V₇ ▷ V₈ ⊗≫ 𝟙 _ = x := by
  simp [Mathlib.Tactic.Coherence.monoidalComp, id_tensorHom, tensorHom_id]
  with_panel_widgets [SelectionPanel]
    -- -- Place your cursor here and shif-click the LHS.
    sorry

2024-02-17-184401.png

[Bolton Bailey]

It should still be able to capture the leftmost side of diagram six though right?

[Bolton Bailey]

Wait, I got it to work!!

[Bolton Bailey]

Screenshot-2024-02-17-at-4.01.56-AM.png

[Bolton Bailey]

That's so cool!!

[Bolton Bailey]

Ok, I am realizing now that I didn't need to spend four hours on the constructions of the individual string manipulations if I just wanted to see this, but still it's very satisfying.

[Bolton Bailey]

Ah, but I can see those manipulations written out as well by shift-clicking!

[Bolton Bailey]

Screenshot-2024-02-17-at-4.08.04-AM.png
Screenshot-2024-02-17-at-4.09.22-AM.png
Screenshot-2024-02-17-at-4.08.54-AM.png
Screenshot-2024-02-17-at-4.10.01-AM.png

[Bolton Bailey]

Time well-spent! Thanks this has been super fun!

[Bolton Bailey]

Here is the code #10655

[Bolton Bailey]

... and here's the VOD when it uploads https://youtu.be/ueFbfwVzBfI

[Johan Commelin]

This looks really cool! Congrats!

It's a private video... and I don't have a google account, so I can't watch it.

[Bolton Bailey]

Thanks, I have now set the video to public (it's still uploading though, so I think it'll be another few minutes before it's available).

[Bolton Bailey]

(Oh right, google makes you sign in to watch age restricted videos, that's annoying. I had age-restricted it because I swore once or twice, but it wasn't "gratuitous" so I've turned off the restriction, hopefully that makes it possible to view without a google account. It looks like the video file will process for an hour or so as well)

[Eric Wieser]

(It's now available, but only in very low quality; it's also 4h30, which is why uploading is taking a while!)

[Yuma Mizuno]

I opened a PR #10581 to share the issues I am aware of. I would be happy to receive someone's help.

[Bolton Bailey]

Yeah, the low quality is unfortunate - the video on my computer is better. Google says that it might still be processing the higher quality versions.

[Bolton Bailey]

Ok video seems to have a higher quality option now.

Going over it, it was overall a very good proving session. One thing I was caught up on for around three and a half minutes was this error, where it is highlighting the first line of the composition in red, when it feels like it should be highlighting the () at the bottom in red.

[Dean Young]

@Yuma Mizuno this is really cool. Is it possible to modify this to work for Mathlib 4's strict bicategories?

[Yuma Mizuno]

Dean Young said:

Yuma Mizuno this is really cool. Is it possible to modify this to work for Mathlib 4's strict bicategories?

Yes, it's pretty straightforward. I wish I will do it in the near future.

[Dean Young]

@Yuma Mizuno @Shanghe Chen and I are very interested

[Yuma Mizuno]

Now the string diagram widget for bicategories are available in #12107! You can use it by importing

import Mathlib.Tactic.Widget.StringDiagram
import ProofWidgets.Component.Panel.SelectionPanel
import ProofWidgets.Component.Panel.GoalTypePanel

open ProofWidgets

and inserting with_panel_widgets [SelectionPanel] or with_panel_widgets [GoalTypePanel] at the beginning of the proof you are interested in.
2024-04-13-20-14-41.mp4

[Mario Carneiro]

@Bolton Bailey said:

One thing I was caught up on for around three and a half minutes was this error, where it is highlighting the first line of the composition in red, when it feels like it should be highlighting the () at the bottom in red.

Can you make a MWE of this issue? Smaller versions of the example seem to behave as desired, for example

#check
  (1 + 1
    + 2 : Nat) =
  () -- error highlight is here

By the way, you note in the video that it's weird that the error highlight doesn't encompass the whole expression. It actually does, you can tell because it shows the error message when your cursor is anywhere in the expression, but the red squiggle
itself is truncated to the first line because it can be distracting and confusing to have a giant red squiggle over everything

[Bolton Bailey]

I made a #mwe at the time, it's in this thread (note I posted the video back in February)

[Bolton Bailey]

Kyle Miller said at the time he was working on a fix. Based on how the MWE in the thread now seems to have the right error, it looks like he did fix it. Thanks @Kyle Miller !