rigid (autonomous) categories

Stream: maths

[Jakob von Raumer]

https://github.com/javra/mathlib/blob/a9c23f53a33b464beec1132bad625d3f7aef1fa1/src/category_theory/monoidal/rigid.lean

[Jakob von Raumer]

Maybe that's interesting to any of the category theory formalisers here. Proving that adjoint mates of morphisms compose already seems super hard. Certainly makes the case that one carefully has to prove a lot of "sliding" lemmas for monoidal categories and/or write more tactics to somehow tackle these kinds of equalities.

[Scott Morrison]

@Jakob von Raumer, have a look at branch#rigid for my attempt at this. I also discovered that it is disappointingly hard. :-)

[Jakob von Raumer]

I now finished some of the complicated proofs, but I think it's an

[Jakob von Raumer]

I think its's not disappointingly hard but it's a nice challenge to come up with the infrastructure on both sides of the tactic monad to tackle those kinds of rewriting arguments...

[Kyle Miller]

I know it's sweeping a lot of coherence theorems under the rug, but it's funny how straightforward the string diagram version of the proof is in comparison:

image.png

Something I've wondered about is having some tool like Globular that could deal with more abstract diagrams (like the ^* operator applied to a diagram) and which could input and output data that could be pasted into a tactic proof. It seems like no one should ever have to manually insert associators or left/right unitors... I've heard that in Metamath they take a similar approach to automation, where you can use tools to create proofs.

(Edit: Scott's mentioned this before, of course :smile:. I also just learned about homotopy.io by looking for previous mentions of Globular.)

[Scott Morrison]

Nicely done, @Jakob von Raumer!

[Jakob von Raumer]

@Kyle Miller Yes, I'd really like to have a widget for string diagram rewriting proofs! I already tried to motivate my students to do it as a master thesis, but I haven't found anyone so far. I'm not sure if it's worth pursuing in Lean 3 or if it's better to use the widget infrastructure @Wojciech Nawrocki is implementing in Lean 4.

Homotopy.io has one huge advantage when visualising the diagrams: They work in a strictly associative setting. I'm not entirely sure how applying an associator would change the visual representation...

[Scott Morrison]

When I last thought about this I was thinking about formalizing Jamie's definition of quasi-strict n-categories.

[Scott Morrison]

Much more approachable would be to just do the n=2 case, or perhaps just the monoidal category (2-category with only one 0-morphism) case.

[Jakob von Raumer]

@Markus Himmel said about his formalisation of the coherence theorem for monoidal categories that he doesn't think it's much easier to reason about strict monoidal categories, because you end up having transport terms all over the place...

[Kyle Miller]

@Jakob von Raumer Maybe this is too limiting, but I was imagining a tool for monoidal categories that pretends you're in a strictly associative setting, but then under-the-hood it would reassociate and introduce identities for you. You'd give the tool a list of allowed coupons and their signatures, and the data structure of a diagram is compatible compositions of products of coupons. Sometimes you'd want to bind wires together into a product wire, but that can be done with additional coupons, like one with two input wires for objects $x$ and $y$ and one output wire for object $x\otimes y$.

A while back I made some tool in LaTeX and python for drawing string diagram proofs for bialgebras:

image.png

All it does is draw things, and it's not very sophisticated (all wires are labeled by the same object), but I thought I'd show how these diagrams are written using a mini-language for compositions of coupons:

  \begin{align*}
    \pyc{diag("S; S")}
    &= \pyc{diag("m*; e* S; e S; m")}
    = \pyc{diag("m*; m* S; id S S; m id; m")}
      = \pyc{diag("m*; id m*; id S S; id id S; id m; m")}\\
    &=\pyc{diag("m*; id S; id m*; id sw; id id S; id m; m")}
      =\pyc{diag("m*; id S; id m*; id S id; id sw; id m; m")}
      =\pyc{diag("m*; id S; id m*; id S id; id m; m")} \\
    &= \pyc{diag("m*; id S; id e*; id e; m")}
      = \pyc{diag("id")}
  \end{align*}

Ideally, this could have a graphical editor to help you move things around and apply axioms/2-morphisms.

[Jakob von Raumer]

Yes, that's roughly what I was imagining

[Kyle Miller]

If there were also a way to group coupons into subdiagrams (which can be thought of as composite coupons) then that would at least give a way to say where axioms can be applied. It's not as elegant as Globular, which seems to be able to efficiently compute where axioms can be applied without this additional structure, but at least it would be workable.

[Jakob von Raumer]

I'm formalising all these things with equalities, but I guess the formalisation should actually be agnostic as to whether it really is a category or a 2-category, meaning instead of rw we'd need a version of rw that builds 2-cells using whiskering...

[Scott Morrison]

Oh --- when I was talking about 2-categories above, I just meant to say that monoidal categories are precisely the 2-categories with a unique 0-morphism (and then shifting everything down a level). I wasn't intending to replace equality with some "richer" 2-morphism structure.

[Scott Morrison]

Jamie's version of monoidal categories is actually very simple: you no longer have a tensor-product-of-morphisms operation, but only composition and tensoring-with-identities, and these operations are strictly associative. You just have one interesting axiom, the exchange relation which lets you slide one coupon vertically past another one.

[Scott Morrison]

You can represent diagrams of this form as a list of triples (each triple corresponds to a horizontal slice of a diagram). Each triple contains a list of objects (the strings to the left of the coupon), a morphism (the coupon), and another list of objects (the strings to the right of the coupon).

[Scott Morrison]

Composition of diagrams is just concatenation of lists.

[Scott Morrison]

Globular / homotopy.io (at least when restricted to two dimensional diagrams) only have one "click-and-drag" operation, i.e. the exchange relation swapping the heights of two adjacent slices (when they don't obstruct each other).

[Scott Morrison]

Without aspiring (immediately) to have a widget interface, it could be really nice to write some tactics for working with this representation of monoidal diagrams. The key piece would be something that can take an expression in the usual (composition + tensor product) language of monoidal categories, and "look for it" in a Jamie-style diagram. (And then have a rewriter, that can rewrite a Jamie-style diagram by an equation written in the usual langauge.)

[Scott Morrison]

Does that make any sense? I feel the need to draw pictures and gesture at them. :-)

[Jakob von Raumer]

Scott Morrison said:

Oh --- when I was talking about 2-categories above, I just meant to say that monoidal categories are precisely the 2-categories with a unique 0-morphism (and then shifting everything down a level). I wasn't intending to replace equality with some "richer" 2-morphism structure.

I know, but the things I'm working with right now suggest them to be 2-cells instead. :shrug:

[Jakob von Raumer]

Scott Morrison said:

Without aspiring (immediately) to have a widget interface, it could be really nice to write some tactics for working with this representation of monoidal diagrams. The key piece would be something that can take an expression in the usual (composition + tensor product) language of monoidal categories, and "look for it" in a Jamie-style diagram. (And then have a rewriter, that can rewrite a Jamie-style diagram by an equation written in the usual langauge.)

Do you mean to use these tactics with a strictly associative tensor product, or to try and "bake the associators in"?

[Jakob von Raumer]

I'm just starting to prove that the left adjoint mate of the right adjoint mate of a morphism is the morphism itself, again a "sliding" proof:

tactic failed, there are unsolved goals
state:
C : Type u₁,
_inst_1 : category C,
_inst_2 : monoidal_category C,
W X Y Z : C,
WX : exact_pairing W X,
YZ : exact_pairing Y Z
⊢ (𝟙 (Z ⊗ X) ⊗ η_ W X) ≫
      (𝟙 (Z ⊗ X) ⊗ 𝟙 W ⊗ (λ_ X).inv) ≫
        (𝟙 (Z ⊗ X) ⊗ 𝟙 W ⊗ η_ Y Z ⊗ 𝟙 X) ≫
          (𝟙 (Z ⊗ X) ⊗ 𝟙 W ⊗ (α_ Y Z X).hom) ≫
            (𝟙 (Z ⊗ X) ⊗ (α_ W Y (Z ⊗ X)).inv) ≫
              (α_ (Z ⊗ X) (W ⊗ Y) (Z ⊗ X)).inv ≫
                ((α_ (Z ⊗ X) W Y).inv ⊗ 𝟙 (Z ⊗ X)) ≫
                  (((α_ Z X W).hom ⊗ 𝟙 Y) ⊗ 𝟙 (Z ⊗ X)) ≫
                    (((𝟙 Z ⊗ ε_ W X) ⊗ 𝟙 Y) ⊗ 𝟙 (Z ⊗ X)) ≫
                      (((ρ_ Z).hom ⊗ 𝟙 Y) ⊗ 𝟙 (Z ⊗ X)) ≫ (ε_ Y Z ⊗ 𝟙 (Z ⊗ X)) =
    (α_ Z X (𝟙_ C)).hom ≫ ((λ_ Z).inv ⊗ (ρ_ X).hom) ≫ (α_ (𝟙_ C) Z X).hom

What struck me as useful is that we do not only generate reassociated lemmas in the category composition but generate versions that can be used to rewrite when additional terms are tensored to the left and right of the lemmas, to prevent having to conjugate with tensor_comp every time...

[Jakob von Raumer]

Scott Morrison said:

Without aspiring (immediately) to have a widget interface, it could be really nice to write some tactics for working with this representation of monoidal diagrams. The key piece would be something that can take an expression in the usual (composition + tensor product) language of monoidal categories, and "look for it" in a Jamie-style diagram. (And then have a rewriter, that can rewrite a Jamie-style diagram by an equation written in the usual langauge.)

Is the proof that the category of Jamie-Style categories is equivalent to monoidal categories a done deal?

[Scott Morrison]

Hmm, very good question.

[Jakob von Raumer]

Scott Morrison said:

You can represent diagrams of this form as a list of triples (each triple corresponds to a horizontal slice of a diagram). Each triple contains a list of objects (the strings to the left of the coupon), a morphism (the coupon), and another list of objects (the strings to the right of the coupon).

Just to make sure that I'm on the same page, you mean that the sliding of morphisms $f : A \to B$ and $g : C \to D$ would be represented by something like $[([A],g,[]),([],f,[D])] = [([],f,[C]),([B],g,[])]$?

[Scott Morrison]

Yes.

[Scott Morrison]

The point is that by not allowing exactly-side-by-side morphisms (as are produced by \otimes), we can drastically reduce the number of axioms needed to describe a monoidal category.

[Jakob von Raumer]

Yes, but it solves a provlem which is orthogonal to the one of having to deal with associators, right?

[Scott Morrison]

I guess so. This formulation is (besides other things) strictifying the tensor product on objects, so I guess is no more helpful than strictification.

[Jakob von Raumer]

Doesn't it require strictification first? Or are we able to go back and forth between Jamie-style categories and monoidal categories without strictification by removing/adding the associators?

[Jakob von Raumer]

Do you think the rigid categories should be PR'ed? Or should I first instantiate them with FinVec? (Which needs a construction of the coevaluation map first...)

[Scott Morrison]

I would be very happy to have them PR'd even without an example, but FinVec would be lovely as well. (Small digestible PRs are great: big PRs are prone to either very long review, or not-that-great-a-job reviews.)

[Jakob von Raumer]

Scott Morrison said:

I would be very happy to have them PR'd even without an example, but FinVec would be lovely as well. (Small digestible PRs are great: big PRs are prone to either very long review, or not-that-great-a-job reviews.)

FinVect is done :octopus:

[Jakob von Raumer]

Can someone give me the rights to write on branches of mathlib?

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Jakob von Raumer]

Thanks!

[Jakob von Raumer]

PR'ed

[Jakob von Raumer]

No idea on how to prevent the linter from complaining about reassoc creating non-simp-nf lemmas

[Alex J. Best]

What about swapping the order of the attributes simp and reassoc? so that reassoc comes first

[Jakob von Raumer]

Ah, that could work. Or adding the simp attribute after the declaration