String Diagram Widget

This file provides meta infrastructure for displaying string diagrams for morphisms in monoidal categories in the infoview. To enable the string diagram widget, you need to import this file and inserting with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram] at the beginning of the proof. Alternatively, you can also write

open Mathlib.Tactic.Widget
show_panel_widgets [local StringDiagram]

to enable the string diagram widget in the current section.

We also have the #string_diagram command. For example,

#string_diagram MonoidalCategory.whisker_exchange

displays the string diagram for the exchange law of the left and right whiskerings.

String diagrams are graphical representations of morphisms in monoidal categories, which are useful for rewriting computations. More precisely, objects in a monoidal category is represented by strings, and morphisms between two objects is represented by nodes connecting two strings associated with the objects. The tensor product X ⊗ Y corresponds to putting strings associated with X and Y horizontally (from left to right), and the composition of morphisms f : X ⟶ Y and g : Y ⟶ Z corresponds to connecting two nodes associated with f and g vertically (from top to bottom) by strings associated with Y.

Currently, the string diagram widget provided in this file deals with equalities of morphisms in monoidal categories. It displays string diagrams corresponding to the morphisms for the left-hand and right-hand sides of the equality.

Some examples can be found in MathlibTest/StringDiagram.lean.

When drawing string diagrams, it is common to ignore associators and unitors. We follow this convention. To do this, we need to extract non-structural morphisms that are not associators and unitors from lean expressions. This operation is performed using the Tactic.Monoidal.eval function.

A monoidal category can be viewed as a bicategory with a single object. The program in this file can also be used to display the string diagram for general bicategories. With this in mind we will sometimes refer to objects and morphisms in monoidal categories as 1-morphisms and 2-morphisms respectively, borrowing the terminology of bicategories. Note that the relation between monoidal categories and bicategories is formalized in Mathlib/CategoryTheory/Bicategory/SingleObj.lean, although the string diagram widget does not use it directly.

Objects in string diagrams

structure Mathlib.Tactic.Widget.StringDiagram.AtomNode : Type

Nodes for 2-morphisms in a string diagram.

• vPos : ℕ

  The vertical position of the node in the string diagram.

• hPosSrc : ℕ

  The horizontal position of the node in the string diagram, counting strings in domains.

• hPosTar : ℕ

  The horizontal position of the node in the string diagram, counting strings in codomains.

• atom : BicategoryLike.Atom

  The underlying expression of the node.

structure Mathlib.Tactic.Widget.StringDiagram.IdNode : Type

Nodes for identity 2-morphisms in a string diagram.

• vPos : ℕ

  The vertical position of the node in the string diagram.

• hPosSrc : ℕ

  The horizontal position of the node in the string diagram, counting strings in domains.

• hPosTar : ℕ

  The horizontal position of the node in the string diagram, counting strings in codomains.

• id : BicategoryLike.Atom₁

  The underlying expression of the node.

inductive Mathlib.Tactic.Widget.StringDiagram.Node : Type

Nodes in a string diagram.

• atom : AtomNode → Node
• id : IdNode → Node

def Mathlib.Tactic.Widget.StringDiagram.Node.e : Node → Lean.Expr

The underlying expression of a node.

def Mathlib.Tactic.Widget.StringDiagram.Node.srcList : Node → List (Node × BicategoryLike.Atom₁)

The domain of the 2-morphism associated with a node as a list (the first component is the node itself).

def Mathlib.Tactic.Widget.StringDiagram.Node.tarList : Node → List (Node × BicategoryLike.Atom₁)

The codomain of the 2-morphism associated with a node as a list (the first component is the node itself).

def Mathlib.Tactic.Widget.StringDiagram.Node.vPos : Node → ℕ

The vertical position of a node in a string diagram.

def Mathlib.Tactic.Widget.StringDiagram.Node.hPosSrc : Node → ℕ

The horizontal position of a node in a string diagram, counting strings in domains.

def Mathlib.Tactic.Widget.StringDiagram.Node.hPosTar : Node → ℕ

The horizontal position of a node in a string diagram, counting strings in codomains.

structure Mathlib.Tactic.Widget.StringDiagram.Strand : Type

Strings in a string diagram.

• hPos : ℕ

  The horizontal position of the strand in the string diagram.

• startPoint : Node

  The start point of the strand in the string diagram.

• endPoint : Node

  The end point of the strand in the string diagram.

• atom₁ : BicategoryLike.Atom₁

  The underlying expression of the strand.

def Mathlib.Tactic.Widget.StringDiagram.Strand.vPos (s : Strand) : ℕ

The vertical position of a strand in a string diagram.

def Mathlib.Tactic.BicategoryLike.WhiskerRight.nodes (v h₁ h₂ : ℕ) : WhiskerRight → List Widget.StringDiagram.Node

The list of nodes associated with a 2-morphism. The position is counted from the specified natural numbers.

def Mathlib.Tactic.BicategoryLike.HorizontalComp.nodes (v h₁ h₂ : ℕ) : HorizontalComp → List Widget.StringDiagram.Node

The list of nodes associated with a 2-morphism. The position is counted from the specified natural numbers.

def Mathlib.Tactic.BicategoryLike.WhiskerLeft.nodes (v h₁ h₂ : ℕ) : WhiskerLeft → List Widget.StringDiagram.Node

The list of nodes associated with a 2-morphism. The position is counted from the specified natural numbers.

def Mathlib.Tactic.BicategoryLike.topNodes {ρ : Type} [MonadMor₁ (CoherenceM ρ)] (η : WhiskerLeft) : CoherenceM ρ (List Widget.StringDiagram.Node)

The list of nodes at the top of a string diagram.

def Mathlib.Tactic.BicategoryLike.NormalExpr.nodesAux {ρ : Type} [MonadMor₁ (CoherenceM ρ)] (v : ℕ) : NormalExpr → CoherenceM ρ (List (List Widget.StringDiagram.Node))

The list of nodes at the top of a string diagram. The position is counted from the specified natural number.

def Mathlib.Tactic.BicategoryLike.NormalExpr.nodes {ρ : Type} [MonadMor₁ (CoherenceM ρ)] (e : NormalExpr) : CoherenceM ρ (List (List Widget.StringDiagram.Node))

The list of nodes associated with a 2-morphism.

@[deprecated List.consecutivePairs (since := "2026-02-26")]

def Mathlib.Tactic.BicategoryLike.pairs {α : Type u_1} (l : List α) : List (α × α)

Alias of List.consecutivePairs.

def Mathlib.Tactic.BicategoryLike.NormalExpr.strands {ρ : Type} [MonadMor₁ (CoherenceM ρ)] (e : NormalExpr) : CoherenceM ρ (List (List Widget.StringDiagram.Strand))

The list of strands associated with a 2-morphism.

structure Mathlib.Tactic.Widget.StringDiagram.PenroseVar : Type

A type for Penrose variables.

• ident : String

  The identifier of the variable.

• indices : List ℕ

  The indices of the variable.

• e : Lean.Expr

  The underlying expression of the variable.

@[implicit_reducible]

instance Mathlib.Tactic.Widget.StringDiagram.instToStringPenroseVar : ToString PenroseVar

def Mathlib.Tactic.Widget.StringDiagram.Node.toPenroseVar (n : Node) : PenroseVar

The penrose variable associated with a node.

def Mathlib.Tactic.Widget.StringDiagram.Strand.toPenroseVar (s : Strand) : PenroseVar

The penrose variable associated with a strand.

Widget for general string diagrams

def Mathlib.Tactic.Widget.StringDiagram.addPenroseVar (tp : String) (v : PenroseVar) : ProofWidgets.Penrose.DiagramBuilderM Unit

Add the variable v with the type tp to the substance program.

def Mathlib.Tactic.Widget.StringDiagram.addConstructor (tp : String) (v : PenroseVar) (nm : String) (vs : List PenroseVar) : ProofWidgets.Penrose.DiagramBuilderM Unit

Add constructor tp v := nm (vs) to the substance program.

def Mathlib.Tactic.Widget.StringDiagram.mkStringDiagram (nodes : List (List Node)) (strands : List (List Strand)) : ProofWidgets.Penrose.DiagramBuilderM PUnit.{1}

Construct a string diagram from a Penrose substance program and expressions embeds to display as labels in the diagram.

def Mathlib.Tactic.Widget.StringDiagram.dsl : String

Penrose dsl file for string diagrams.

def Mathlib.Tactic.Widget.StringDiagram.sty : String

Penrose sty file for string diagrams.

inductive Mathlib.Tactic.Widget.StringDiagram.Kind : Type

The kind of the context.

• monoidal : Kind
• bicategory : Kind
• none : Kind

def Mathlib.Tactic.Widget.StringDiagram.Kind.name : Kind → Lean.Name

The name of the context.

def Mathlib.Tactic.Widget.StringDiagram.mkKind (e : Lean.Expr) : Lean.MetaM Kind

Given an expression, return the kind of the context.

def Mathlib.Tactic.Widget.StringDiagram.stringM? (e : Lean.Expr) : Lean.MetaM (Option ProofWidgets.Html)

Given a 2-morphism, return a string diagram. Otherwise none.

def Mathlib.Tactic.Widget.StringDiagram.mkEqHtml (lhs rhs : ProofWidgets.Html) : ProofWidgets.Html

Help function for displaying two string diagrams in an equality.

def Mathlib.Tactic.Widget.StringDiagram.stringEqM? (e : Lean.Expr) : Lean.MetaM (Option ProofWidgets.Html)

Given an equality between 2-morphisms, return a string diagram of the LHS and RHS. Otherwise none.

def Mathlib.Tactic.Widget.StringDiagram.stringMorOrEqM? (e : Lean.Expr) : Lean.MetaM (Option ProofWidgets.Html)

Given an 2-morphism or equality between 2-morphisms, return a string diagram. Otherwise none.

def Mathlib.Tactic.Widget.StringDiagram.stringPresenter : ProofWidgets.ExprPresenter

The Expr presenter for displaying string diagrams.

def Mathlib.Tactic.Widget.StringDiagram.rpc (props : ProofWidgets.PanelWidgetProps) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

The RPC method for displaying string diagrams.

def Mathlib.Tactic.Widget.StringDiagram : ProofWidgets.Component ProofWidgets.PanelWidgetProps

Display the string diagrams if the goal is an equality of morphisms in a monoidal category.

def Mathlib.Tactic.Widget.stringDiagram : Lean.ParserDescr

Display the string diagram for a given term.

Example usage:

/- String diagram for the equality theorem. -/
#string_diagram MonoidalCategory.whisker_exchange

/- String diagram for the morphism. -/
variable {C : Type u} [Category.{v} C] [MonoidalCategory C] {X Y : C} (f : 𝟙_ C ⟶ X ⊗ Y) in
#string_diagram f

def Mathlib.Tactic.Widget.elabStringDiagramCmd : Lean.Elab.Command.CommandElab

Display the string diagram for a given term.

Example usage:

/- String diagram for the equality theorem. -/
#string_diagram MonoidalCategory.whisker_exchange

/- String diagram for the morphism. -/
variable {C : Type u} [Category.{v} C] [MonoidalCategory C] {X Y : C} (f : 𝟙_ C ⟶ X ⊗ Y) in
#string_diagram f