Documentation

KernelHom.Tactic.Hom.KernelDiagram

Kernel Diagram Widget #

This file provides meta infrastructure for displaying string diagrams for s-finite kernels in the infoview. To enable the kernel diagram widget, you need to import this file and inserting with_panel_widgets [KernelDiagram] at the beginning of the proof. Alternatively, you can also write

show_panel_widgets [local KernelDiagram]

to enable the string diagram widget in the current section.

We also have the #kernel_diagram command. For example,

#string_diagram ProbabilityTheory.Kernel.deterministic_comp_copy

This is an adaptation of the string diagram widget where kernels are transformed into morphisms of the SFinKer monoidal category using the kernel_hom tactic.

source
def Mathlib.Tactic.Widget.StringDiagram.Node.toPenroseVar_kernel (n : Node) :
Lean.MetaM PenroseVar

The kernelized penrose variable associated with a node.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Tactic.Widget.StringDiagram.mkKernelDiagram (nodes : List (List Node)) (strands : List (List Strand)) :
    ProofWidgets.Penrose.DiagramBuilderM PUnit.{1}

    Construct a kernelized 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
      source
      def KernelDiagram.KernelM? (e : Lean.Expr) :
      Lean.MetaM (Option ProofWidgets.Html)

      Given a kernel expression, return a string diagram. Otherwise none.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def KernelDiagram.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.
        Instances For
          source
          def KernelDiagram.kernelEqM? (e : Lean.Expr) :
          Lean.MetaM (Option ProofWidgets.Html)

          Given an equality between kernels, 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
            source
            def KernelDiagram.kernelMorOrEqM? (e : Lean.Expr) :
            Lean.MetaM (Option ProofWidgets.Html)

            Given a kernel or equality between kernels, return a string diagram. Otherwise none.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def KernelDiagram.rpc (props : ProofWidgets.PanelWidgetProps) :
              Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

              The RPC method for displaying kernel diagrams.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def KernelDiagram :
                ProofWidgets.Component ProofWidgets.PanelWidgetProps

                Display the kernel diagrams if the goal is an equality of s-finite kernels.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def kernelDiagram :
                  Lean.ParserDescr

                  Display the kernel diagram for a given term.

                  Example usage:

                  /- Kernel diagram for an equality theorem. -/
#kernel_diagram ProbabilityTheory.Kernel.deterministic_comp_copy
                  Equations
                  Instances For
                    source
                    def elabKernelDiagramCmd :
                    Lean.Elab.Command.CommandElab

                    Display the kernel diagram for a given term.

                    Example usage:

                    /- Kernel diagram for an equality theorem. -/
#kernel_diagram ProbabilityTheory.Kernel.deterministic_comp_copy
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For