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 test/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 (see the wip PR https://github.com/leanprover-community/mathlib4/pull/12107). 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, 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 : Mathlib.Tactic.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 : Mathlib.Tactic.BicategoryLike.Atom₁

  The underlying expression of the node.

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

Nodes in a string diagram.

• atom: Mathlib.Tactic.Widget.StringDiagram.AtomNode → Mathlib.Tactic.Widget.StringDiagram.Node
• id: Mathlib.Tactic.Widget.StringDiagram.IdNode → Mathlib.Tactic.Widget.StringDiagram.Node

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

The underlying expression of a node.

Equations

• (Mathlib.Tactic.Widget.StringDiagram.Node.atom n).e = n.atom.e
• (Mathlib.Tactic.Widget.StringDiagram.Node.id n).e = n.id.e

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

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

Equations

• (Mathlib.Tactic.Widget.StringDiagram.Node.atom n).srcList = List.map (fun (f : Mathlib.Tactic.BicategoryLike.Atom₁) => (Mathlib.Tactic.Widget.StringDiagram.Node.atom n, f)) n.atom.src.toList
• (Mathlib.Tactic.Widget.StringDiagram.Node.id n).srcList = [(Mathlib.Tactic.Widget.StringDiagram.Node.id n, n.id)]

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

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

Equations

• (Mathlib.Tactic.Widget.StringDiagram.Node.atom n).tarList = List.map (fun (f : Mathlib.Tactic.BicategoryLike.Atom₁) => (Mathlib.Tactic.Widget.StringDiagram.Node.atom n, f)) n.atom.tgt.toList
• (Mathlib.Tactic.Widget.StringDiagram.Node.id n).tarList = [(Mathlib.Tactic.Widget.StringDiagram.Node.id n, n.id)]

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

The vertical position of a node in a string diagram.

Equations

• (Mathlib.Tactic.Widget.StringDiagram.Node.atom n).vPos = n.vPos
• (Mathlib.Tactic.Widget.StringDiagram.Node.id n).vPos = n.vPos

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

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

Equations

• (Mathlib.Tactic.Widget.StringDiagram.Node.atom n).hPosSrc = n.hPosSrc
• (Mathlib.Tactic.Widget.StringDiagram.Node.id n).hPosSrc = n.hPosSrc

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

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

Equations

• (Mathlib.Tactic.Widget.StringDiagram.Node.atom n).hPosTar = n.hPosTar
• (Mathlib.Tactic.Widget.StringDiagram.Node.id n).hPosTar = n.hPosTar

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

Strings in a string diagram.

• hPos : ℕ

  The horizontal position of the strand in the string diagram.

• startPoint : Mathlib.Tactic.Widget.StringDiagram.Node

  The start point of the strand in the string diagram.

• endPoint : Mathlib.Tactic.Widget.StringDiagram.Node

  The end point of the strand in the string diagram.

• atom₁ : Mathlib.Tactic.BicategoryLike.Atom₁

  The underlying expression of the strand.

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

The vertical position of a strand in a string diagram.

Equations

• s.vPos = s.startPoint.vPos

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.BicategoryLike.HorizontalComp.nodes v h₁ h₂ (Mathlib.Tactic.BicategoryLike.HorizontalComp.of η) = Mathlib.Tactic.BicategoryLike.WhiskerRight.nodes v h₁ h₂ η

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

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

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.BicategoryLike.WhiskerLeft.nodes v h₁ h₂ (Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η) = Mathlib.Tactic.BicategoryLike.HorizontalComp.nodes v h₁ h₂ η

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The list of nodes associated with a 2-morphism.

Equations

• One or more equations did not get rendered due to their size.
• (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e_1 α).nodes = pure []

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

pairs [a, b, c, d] is [(a, b), (b, c), (c, d)].

Equations

• Mathlib.Tactic.BicategoryLike.pairs l = l.zip (List.drop 1 l)

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

The list of strands associated with a 2-morphism.

Equations

• One or more equations did not get rendered due to their size.

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.

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

Equations

• One or more equations did not get rendered due to their size.

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

The penrose variable associated with a node.

Equations

• n.toPenroseVar = { ident := "E", indices := [n.vPos, n.hPosSrc, n.hPosTar], e := n.e }

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

The penrose variable associated with a strand.

Equations

• s.toPenroseVar = { ident := "f", indices := [s.vPos, s.hPos], e := s.atom₁.e }

Widget for general string diagrams

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Widget.StringDiagram.mkStringDiagram (nodes : List (List Mathlib.Tactic.Widget.StringDiagram.Node)) (strands : List (List Mathlib.Tactic.Widget.StringDiagram.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.

Equations

• One or more equations did not get rendered due to their size.

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

Penrose dsl file for string diagrams.

Equations

• One or more equations did not get rendered due to their size.

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

Penrose sty file for string diagrams.

Equations

• One or more equations did not get rendered due to their size.

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

The kind of the context.

• monoidal: Mathlib.Tactic.Widget.StringDiagram.Kind
• bicategory: Mathlib.Tactic.Widget.StringDiagram.Kind
• none: Mathlib.Tactic.Widget.StringDiagram.Kind

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

The name of the context.

Equations

• Mathlib.Tactic.Widget.StringDiagram.Kind.monoidal.name = `monoidal
• Mathlib.Tactic.Widget.StringDiagram.Kind.bicategory.name = `bicategory
• Mathlib.Tactic.Widget.StringDiagram.Kind.none.name = default

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

Given an expression, return the kind of the context.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Help function for displaying two string diagrams in an equality.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

The Expr presenter for displaying string diagrams.

Equations

• One or more equations did not get rendered due to their size.

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

The RPC method for displaying string diagrams.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.