Braided left rigid categories are right rigid

Stream: mathlib4

[Gareth Ma]

This is both announcement(?) post and some questions.

I'm working on proving that braided left rigid (autonomous) categories are right rigid, following this and nlab that somehow doesn't show up on Google search. I proved half of it! By transcribing the nlab article carefully.

1. Is anyone working on related things (I should've asked before I proved it, but this result was needed in a completely different field)
2. Is it normal for category proofs to look so long and tedious in Lean? The longest line is 163 characters long even after hiding unitors and associators with ⊗≫
3. The coherence tactic has a bug that I will make another post in tactics channel

import Mathlib.CategoryTheory.Simple
import Mathlib.Order.BoundedOrder
import Mathlib.RepresentationTheory.Action.Limits
import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.RingTheory.SimpleModule

open CategoryTheory Category BraidedCategory MonoidalCategory

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

/- yang baxter but with β_.inv instead of β_.hom.
Maybe there is a proof via duality, but proving it directly is just copy and pasting -/
theorem yang_baxter_inv (X Y Z : C) :
    (α_ X Y Z).inv ≫ (β_ Y X).inv ▷ Z ≫ (α_ Y X Z).hom
      ≫ Y ◁ (β_ Z X).inv ≫ (α_ Y Z X).inv ≫ (β_ Z Y).inv ▷ X ≫ (α_ Z Y X).hom
        = X ◁ (β_ Z Y).inv ≫ (α_ X Z Y).inv
          ≫ (β_ Z X).inv ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ Y X).inv := by
  rw [← braiding_inv_tensor_left_assoc, ← cancel_mono (α_ Z Y X).inv]
  repeat rw [assoc]
  rw [Iso.hom_inv_id, comp_id, ← braiding_inv_naturality_right, braiding_inv_tensor_left]

theorem yang_baxter_inv' (X Y Z : C) :
    (β_ Y X).inv ▷ Z ⊗≫ Y ◁ (β_ Z X).inv ⊗≫ (β_ Z Y).inv ▷ X =
      𝟙 _ ⊗≫ (X ◁ (β_ Z Y).inv ⊗≫ (β_ Z X).inv ▷ Y ⊗≫ Z ◁ (β_ Y X).inv) ⊗≫ 𝟙 _ := by
  rw [← cancel_epi (α_ X Y Z).inv, ← cancel_mono (α_ Z Y X).hom]
  convert yang_baxter_inv X Y Z using 1
  all_goals coherence

/- Wow holy shit grhkm doing category theory -/
example [inst : ExactPairing X Y] : ExactPairing Y X where
  coevaluation' := η_ X Y ≫ (β_ Y X).inv
  evaluation' := (β_ X Y).hom ≫ ε_ X Y
  coevaluation_evaluation' := by
    /- Rearrange into _ = 𝟙 _ -/
    rw [Iso.eq_comp_inv, ← Iso.inv_comp_eq_id]
    monoidal_simps
    /- Whitney trick transcribed: https://ncatlab.org/toddtrimble/published/Whitney+trick -/
    calc
      _ = (λ_ X).inv ≫ (β_ X (𝟙_ C)).inv ≫ X ◁ η_ X Y ⊗≫ (β_ X X).hom ▷ Y ≫ (β_ X X).inv ▷ Y ⊗≫ X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X ≫ ε_ X Y ▷ X ≫ (λ_ X).hom := by
        simp [monoidalComp]
      _ = (λ_ X).inv ≫ η_ X Y ▷ X ⊗≫ (X ◁ (β_ X Y).inv ⊗≫ (β_ X X).inv ▷ Y ⊗≫ X ◁ (β_ Y X).inv) ⊗≫ (β_ X Y).hom ▷ X ≫ ε_ X Y ▷ X ≫ (λ_ X).hom := by
        rw [monoidalComp, ← braiding_inv_naturality_left_assoc _ X, braiding_inv_tensor_right]
        simp
        coherence
      _ = (λ_ X).inv ≫ η_ X Y ▷ X ⊗≫ ((β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ (β_ X Y).inv ▷ X) ≫ (β_ X Y).hom ▷ X ≫ ε_ X Y ▷ X ≫ (λ_ X).hom := by
        rw [yang_baxter_inv']
        simp [monoidalComp]
      _ = (λ_ X).inv ≫ η_ X Y ▷ X ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ ((β_ X Y).inv ▷ X ≫ (β_ X Y).hom ▷ X) ≫ ε_ X Y ▷ X ≫ (λ_ X).hom := by
        simp only [monoidalComp, assoc]
      _ = (λ_ X).inv ≫ η_ X Y ▷ X ⊗≫ (X ◁ ε_ X Y ≫ (β_ (𝟙_ C) X).inv) ≫ (λ_ X).hom := by
        rw [inv_hom_whiskerRight _ X, braiding_inv_naturality_right, braiding_inv_tensor_left]
        coherence
      _ = (λ_ X).inv ≫ (η_ X Y ▷ X ≫ (α_ X Y X).hom ≫ X ◁ ε_ X Y) ≫ (ρ_ X).hom := by
        rw [assoc, braiding_inv_tensorUnit_left, assoc, Iso.inv_hom_id, comp_id]
        coherence
      _ = _ := by
        rw [inst.evaluation_coevaluation]
        simp

  evaluation_coevaluation' := sorry

[Kim Morrison]

No, that doesn't look bad at all. :-) Excited to see this happening.

[Kim Morrison]

Since you've got another equally long sorry to go, I'd suggest making both preliminary lemmas.

[Gareth Ma]

Will do, thanks :) should be done soon, and I'll PR this first before the rest of the relevant work (on representation theory)

[Gareth Ma]

I golfed both proofs to 15 lines, and they're pretty much symmetric now. I don't see a way to do it via duality or something that's shorter. As a result, this works

image.png

[Gareth Ma]

todo -1

[Gareth Ma]

It's #14140 now. The naming is questionable so anyone that can help would be great :D

[Gareth Ma]

The next TODO for FdRep k G is proving it (or equivalently, that FGModuleCat k) has finite colimits, and also is abelian. Do you have any smart category theoretic proof for this that maybe comes from colimits of ModuleCat k? Or should I follow Mathlib/Algebra/Category/ModuleCat/Colimits.leanand construct the colimit kind of from scratch, as in endowing (is that the correct word) forget₂ (FGModuleCat R) (ModuleCat R) with the finitely generated structure? @Kim Morrison (since you added the TODO back in mathlib3)

[Gareth Ma]

Also it seems R has to be Noetherian for fg-R-mod to be abelian (stacks (5))

[Kim Morrison]

To be honest I've forgotten what I had in mind. It does seem like a bit of work to do directly. Does one take a free cover of all the modules in the diagram, tensor them together, and show that is a free cover of the colimit? Sounds unpleasant.

Actually, I guess one is meant to first do the TODO in ModuleCat/Colimits: give the better model of colimits as quotients of finitely supported functions. I think then it becomes pretty obvious that a finite colimit of finitely generated things is finitely generated.

[Gareth Ma]

Re first point: To my understanding that's basically what was done for limits of FGModuleCat. They first prove

instance {J : Type} [Finite J] (Z : J → ModuleCat.{v} k) [∀ j, FiniteDimensional k (Z j)] :
    FiniteDimensional k (∏ᶜ fun j => Z j : ModuleCat.{v} k) :=

then

/-- Finite limits of finite dimensional vectors spaces are finite dimensional,
because we can realise them as subobjects of a finite product. -/
instance (F : J ⥤ FGModuleCat k) :
    FiniteDimensional k (limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k)) : ModuleCat.{v} k) :=

and finally prove that forget2 creates limits.

Re second point: I will have to look at the relevant API closely. Sorry if this is trivial, my category theory is uh not good. Are the "finitely supported functions" here by identifying $\coprod_{i \in \mathrm{ob}(J)} M_i = \bigoplus_{i \in \mathrm{ob(J)}} M_i$ as functions $i \in \mathrm{ob(J)} \to_0 M_i$, then doing colimits as the giant quotient construction $\coprod_i M_i / \sim$ (as sets, like constructing colimits from coequalisers)?

[Gareth Ma]

Lol I traced all the way back on how these colimits come to be (FGModuleCat <- ModuleCat <- AddCommGrp <- MonCat (approach-wise, not dependent)), and in the end I found yet another TODO

TODO:
In fact, in `AddCommGrp` there is a much nicer model of colimits as quotients
of finitely supported functions, and we really should implement this as well (or instead).

So if I can actually figure out this TODO, then I have to refactor all those files :octopus:
Upside is I understand AddCommGrp way better so that's easier...

[Gareth Ma]

https://gist.github.com/grhkm21/5b2d938753c0ce0900d21c93a39e3b7d Okay I proved it. Do you mind taking a look and see if it looks correct? And should I replace the existing code with this (of course reproving existing lemmas) or put it in a separate file

[Gareth Ma]

@Kim Morrison

[Gareth Ma]

Hey if you don't mind can you also explain why here HasFiniteColimits the type of J should be fixed at Type 0?
image.png

[Gareth Ma]

(deleted)

[Gareth Ma]

I found out about hasFiniteColimits_of_hasFiniteColimits_of_size but I don't quite understand why the above is defined like that ^

[Kim Morrison]

I'm sorry, I probably don't have time to look at this in the immediate future. If you put it up as a PR hopefully someone can give a review!

[Gareth Ma]

Okok sorry for bothering

[Kim Morrison]

No bother at all, I wish I had the time! :-)

[Robert Maxton]

Gareth Ma said:

Hey if you don't mind can you also explain why here HasFiniteColimits the type of J should be fixed at Type 0?
image.png

Kind of spitballing here (brought here by your related coherence post), but I believe this is a consequence of why Type u + 1 exists at all: namely, it must exist in order so that Type u itself can have a Type, and more specifically so that functions that take Type us as parameters have somewhere to live. But conversely while you can always put something in Type 1 for giggles if you like, there will always be something in Type 0 isomorphic to it unless it's either quantifying somehow over Type 0 itself, or nontrivially derived from something else that is (and if the proof is at all similar to the similar proof in computability theory/reverse mathematics then even bounded foralls won't require the universe bump). And there are an infinite number of Type 0s, so if you only care about finite categories with no enriched structure then you will necessarily catch all of them, up to isomorphism, by checking only Type 0.

[Robert Maxton]

So the proof rightly assumes no stricter requirements than it actually needs and only requires that you prove existence of colimits for Type 0 specifically.