Automation for Markov/Monoidal Category Theory

Stream: new members

[Dario Stein]

Hi all :-)

I am pretty new to Lean and Mathlib, and wanted to start formalizing some work around Markov categories with are symmetric monoidal categories with a bit of extra structure which enables them to express concepts from probability theory. I wanted to ask some beginner's questions how to best go about it. Here's my start so far

import Mathlib.CategoryTheory.Category.Init
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.Combinatorics.Quiver.Basic
import Mathlib.Tactic.Common

import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.Monoidal.Category
import Mathlib.CategoryTheory.Monoidal.Braided.Basic

open CategoryTheory
open CategoryTheory.Iso
open MonoidalCategory
open SymmetricCategory

universe v u

section

variable {C : Type u} [Category.{v} C] [MonoidalCategory C] [SymmetricCategory C]

def inner_swap (X Y : C) : (X ⊗ X) ⊗ (Y ⊗ Y) ≅ (X ⊗ Y) ⊗ (X ⊗ Y) :=
  calc
    (X ⊗ X) ⊗ (Y ⊗ Y) ≅ X ⊗ (X ⊗ (Y ⊗ Y)) := by exact α_ X X (Y ⊗ Y)
                    _ ≅ X ⊗ ((X ⊗ Y) ⊗ Y) := by exact (refl X ⊗ (symm (α_ X Y Y)))
                    _ ≅ X ⊗ ((Y ⊗ X) ⊗ Y) := by exact (refl X ⊗ (β_ X Y ⊗ refl Y))
                    _ ≅ X ⊗ (Y ⊗ (X ⊗ Y)) := by exact (refl X ⊗ (α_ Y X Y))
                    _ ≅ (X ⊗ Y) ⊗ (X ⊗ Y) := by exact (symm (α_ X _ _))

end

class MarkovCategory (C : Type u) [Category.{v} C] [MonoidalCategory C] [SymmetricCategory C] where
  /-- copy map -/
  copy (X : C) : X ⟶ X ⊗ X
  /-- delete map -/
  del (X : C) : X ⟶ 𝟙_C

  /-- laws -/
  copy_unit_l (X : C) : copy X ≫ (del X ⊗ 𝟙 X) ≫ (λ_ X).hom = 𝟙 X
  copy_unit_r (X : C) : copy X ≫ (𝟙 X ⊗ del X) ≫ (ρ_ X).hom = 𝟙 X
  copy_assoc (X : C) : copy X ≫ (𝟙 X ⊗ copy X) = copy X ≫ (copy X ⊗ 𝟙 X) ≫ (α_ X X X).hom
  copy_comm (X : C) : copy X ≫ (β_ X X).hom = copy X
  copy_tensor (X Y : C) : copy (X ⊗ Y) = (copy X ⊗ copy Y) ≫ (inner_swap X Y).hom
  del_unique {X : C} (f : X ⟶ 𝟙_C) : f = del X

section Examples

variable {C : Type u} [Category.{v} C] [MonoidalCategory C] [SymmetricCategory C] [MarkovCategory C]

open MarkovCategory

-- prove some lemmas
lemma semicartesian {X : C} (f g : X ⟶ 𝟙_C) : f = g := by
  rw [del_unique f, ← del_unique g]

lemma del_natural {X Y : C} (f : X ⟶ Y) : f ≫ del Y = del X := by
  apply semicartesian

-- important definition
def deterministic {X Y : C} (f : X ⟶ Y) := f ≫ copy Y = copy X ≫ (f ⊗ f)

-- more simple lemmas
lemma id_deterministic {X : C} : deterministic (𝟙 X) := by
  unfold deterministic
  simp

lemma del_deterministic {X : C} : deterministic (del X) := by
  unfold deterministic
  sorry -- getting ugly

lemma copy_deterministic {X : C} : deterministic (copy X) := by
  unfold deterministic
  rw [copy_tensor]
  unfold inner_swap
  simp
  sorry -- very ugly

end Examples

As I am still learning my way around the system. Here are some questions and observations; please let me know how I can improve my code, or how to proceed more generally:

• MathLib uses Iso instead of plain morphisms, so I have to write a lot of .hom and .inv when working with monoidal coherence
• Iso is a Trans instance, so I can at least use calc to define maps such as inner_swap. Still a bit painful, is there a better way?
• In all but the simplest lemmas, my proof obligations become littered with coherence maps like

copy X ≫
    (copy X ⊗ copy X) ≫
      (α_ X X (X ⊗ X)).hom ≫ X ◁ (α_ X X X).inv ≫ X ◁ (β_ X X).hom ▷ X ≫ X ◁ (α_ X X X).hom ≫ (α_ X X (X ⊗ X)).inv =
  copy X ≫ (copy X ⊗ copy X)

Not only are the statements messy to prove (I expected as much), but they are even messy to write down. Tactic support would be nice. It there any way to ease that burden, or do I just need to get used to this?

• I found tactics aesop_cat and coherence which provide some automation. Are there more powerful ones, and how can I find them?
• Should every module (Monoidal, Braided, Markov Categories etc) strive to come with their own automations/tactic support? How should I employ simp and reassoc annotations, and how can I use make use of them?

[Yuma Mizuno]

The monoidalComp denoted by ⊗≫ is useful:

(copy X ≫ (copy X ⊗ copy X) ⊗≫ X ◁ (β_ X X).hom ▷ X ⊗≫ 𝟙 _ : X ⟶ (X ⊗ X) ⊗ X ⊗ X) = copy X ≫ (copy X ⊗ copy X)

[Yuma Mizuno]

and recently I'm developing tactics for monoidal categories #mathlib4 > Proof producing coherence tactic for monoidal categories.

[Yuma Mizuno]

In my opinion, it would be nice to have own tactic at least for symmetric braided categories, and maybe braided too.

[Yuma Mizuno]

By the way, mathlib already has definitions like docs#CategoryTheory.tensor_μ, docs#Comon_.

[Dario Stein]

Thanks!

Yuma Mizuno said:

In my opinion, it would be nice to have own tactic at least for symmetric braided categories, and maybe braided too.

I agree that would be awesome! I know the datastructures involved in normalizing such terms, but I have no idea about how to write tactics in practice ;)