Monoidal category tactics

Stream: metaprogramming / tactics

[Gareth Ma]

I was working on this, and came across a bug and two tactic suggestions - I might try to (re)learn tactics and write it myself if I feel like it..., but maybe someone is interested too...

Bug 1: coherence fails with "no goals to solve" when the proof is "too trivial".

import Mathlib.RepresentationTheory.Character

open CategoryTheory Category BraidedCategory MonoidalCategory

universe u
variable {C : Type u} [Category C] [MonoidalCategory C] [BraidedCategory C]

example (X Y : C) (f h : X ⟶ Y) (g : Y ⟶ X) : (f ≫ g) ≫ h = f ≫ g ≫ h := by
  coherence -- no

I think it's missing some try somewhere?

Feature 1: it would be great if theorems in monoidal categories can have their monoidalComp version automatically generated. Easiest example is look at yang_baxter and yang_baxter'. A TLDR is that ⊗≫ helps the user write cleaner equations by hiding associators and unitors, but as a result theorems that write out associators and units explicitly will duplicate it manually. So an attribute @[...] that generates it automatically would be great. Alternatively,

Feature 2: have a feature that expands / contracts these associators and unitors. e.g. turn the goal / hypothesis (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv into (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv and vice versa. Keeping track of associators confuses my brain :(

Hope this makes sense

[Gareth Ma]

Actually for feature 2, it seems simp [monoidalComp] works well for monoidalComp -> associators/unitors, but I don't think the other direction is there

[Kim Morrison]

If you want to try sprinkling try to fix bug 1, I'll happily merge. :-)