Documentation

Mathlib.Tactic.Widget.StringDiagram

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

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.

  • The underlying expression of the node.

Instances For

    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.

    • The underlying expression of the node.

    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

          Strings in a string diagram.

          Instances For

            The vertical position of a strand in a string diagram.

            Equations
            • s.vPos = s.startPoint.vPos
            Instances For

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

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

                Equations
                Instances For

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

                  Equations
                  Instances For

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

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

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

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

                        Equations
                        Instances For

                          A type for Penrose variables.

                          • ident : String

                            The identifier of the variable.

                          • indices : List

                            The indices of the variable.

                          • The underlying expression of the variable.

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

                            The penrose variable associated with a node.

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

                              The penrose variable associated with a strand.

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

                                Widget for general string diagrams #

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

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

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

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

                                      Penrose dsl file for string diagrams.

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

                                        Penrose sty file for string diagrams.

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

                                          Given an expression, return the kind of the context.

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

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

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

                                              Help function for displaying two string diagrams in an equality.

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

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

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

                                                    The Expr presenter for displaying string diagrams.

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

                                                      The RPC method for displaying string diagrams.

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

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

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

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