Strong monads

Stream: mathlib4

[Jad Ghalayini]

Does it make sense to add a PR for a StrongMonad C class, which extends Monad C with data ensuring the monad is strong w.r.t. a MonoidalCategory C?

[Jad Ghalayini]

We'd also want an instance or somesuch stating that type-monads are always strong

[Jad Ghalayini]

Alright here's what I've got so far:

import Mathlib.CategoryTheory.Monad.Basic
import Mathlib.CategoryTheory.Monoidal.Category
import Mathlib.CategoryTheory.Monoidal.Types.Basic

namespace CategoryTheory

variable {C : Type u} [Category C] [MonoidalCategoryStruct C]

open MonoidalCategory

class LeftStrength (T : Monad C) where
  leftStrength : ∀(X Y : C), X ⊗ (T.obj Y) ⟶ T.obj (X ⊗ Y)
  leftStrength_naturality : ∀(X Y X' Y' : C) (f : X ⟶ X') (g : Y ⟶ Y'),
    (f ⊗ (T.map g)) ≫ leftStrength X' Y' = leftStrength X Y ≫ T.map (f ⊗ g)
  leftUnitor_leftStrength : ∀(X : C),
    (λ_ (T.obj X)).inv ≫ leftStrength (𝟙_ C) X = T.map (λ_ X).inv
  leftStrength_associator : ∀(X Y Z : C),
    leftStrength (X ⊗ Y) Z ≫ T.map (α_ X Y Z).hom
      = (α_ X Y (T.obj Z)).hom ≫ X ◁ leftStrength Y Z ≫ leftStrength X (Y ⊗ Z)
  η_leftStrength : ∀(X Y : C), X ◁ T.η.app Y ≫ leftStrength X Y = T.η.app (X ⊗ Y)
  μ_leftStrength : ∀(X Y : C),
    X ◁ T.μ.app Y ≫ leftStrength X Y
      = leftStrength X (T.obj Y) ≫ T.map (leftStrength X Y) ≫ T.μ.app (X ⊗ Y)

attribute [reassoc] LeftStrength.leftStrength_naturality
attribute [reassoc] LeftStrength.leftUnitor_leftStrength
attribute [reassoc] LeftStrength.leftStrength_associator
attribute [reassoc] LeftStrength.η_leftStrength
attribute [reassoc] LeftStrength.μ_leftStrength

class RightStrength (T : Monad C) where
  rightStrength : ∀(X Y : C), T.obj X ⊗ Y ⟶ T.obj (X ⊗ Y)
  rightStrength_naturality : ∀(X Y X' Y' : C) (f : X ⟶ X') (g : Y ⟶ Y'),
    ((T.map f) ⊗ g) ≫ rightStrength X' Y' = rightStrength X Y ≫ T.map (f ⊗ g)
  rightUnitor_rightStrength : ∀(X : C),
    (ρ_ (T.obj X)).inv ≫ rightStrength X (𝟙_ C) = T.map (ρ_ X).inv
  rightStrength_associator : ∀(X Y Z : C),
    rightStrength X (Y ⊗ Z) ≫ T.map (α_ X Y Z).inv
      = (α_ (T.obj X) Y Z).inv ≫ rightStrength X Y ▷ Z ≫ rightStrength (X ⊗ Y) Z
  η_rightStrength : ∀(X Y : C), T.η.app X ▷ Y ≫ rightStrength X Y = T.η.app (X ⊗ Y)
  μ_rightStrength : ∀(X Y : C),
    T.μ.app X ▷ Y ≫ rightStrength X Y
      = rightStrength (T.obj X) Y ≫ T.map (rightStrength X Y) ≫ T.μ.app (X ⊗ Y)

attribute [reassoc] RightStrength.rightStrength_naturality
attribute [reassoc] RightStrength.rightUnitor_rightStrength
attribute [reassoc] RightStrength.rightStrength_associator
attribute [reassoc] RightStrength.η_rightStrength
attribute [reassoc] RightStrength.μ_rightStrength

class Strength (T : Monad C) extends LeftStrength T, RightStrength T where
  leftStrength_rightStrength : ∀(X Y Z : C),
    leftStrength X Y ▷ Z ≫ rightStrength (X ⊗ Y) Z
      = (α_ X (T.obj Y) Z).hom
      ≫ X ◁ rightStrength Y Z
      ≫ leftStrength X (Y ⊗ Z)
      ≫ T.map (α_ X Y Z).inv

attribute [reassoc] Strength.leftStrength_rightStrength

open LeftStrength RightStrength

@[reassoc]
theorem Strength.rightStrength_leftStrength {T : Monad C} [Strength T] (X Y Z : C) :
  X ◁ rightStrength Y Z ≫ leftStrength X (Y ⊗ Z)
    = (α_ X (T.obj Y) Z).inv ≫ leftStrength X Y ▷ Z ≫ rightStrength _ Z ≫ T.map (α_ X Y Z).hom
  := by simp [leftStrength_rightStrength_assoc]

instance Strength.ofType.{v} {T : Monad (Type v)} : Strength T := /- snip -/

class CommutativeMonad (T : Monad C) extends Strength T where
  is_commutative : ∀(X Y : C),
    leftStrength (T.obj X) Y ≫ T.map (rightStrength X Y) ≫ T.μ.app (X ⊗ Y)
      = rightStrength X (T.obj Y) ≫ T.map (leftStrength X Y) ≫ T.μ.app (X ⊗ Y)

end CategoryTheory

How does this look for a start?

[Jad Ghalayini]

Also, any idea where we might put the analogue of CommutativeMonad for regular type-valued monads?

[Jad Ghalayini]

Here's what that would look like btw:

import Mathlib.Tactic.Convert

class SeqComm (f : Type u → Type v) [Applicative f] : Prop where
  seq_comm {α β : Type u} (l : f α) (r : f β) :
    Prod.mk <$> l <*> r = (λr (l : α) => (l, r)) <$> r <*> l

theorem SeqComm.bind_pair_comm {m : Type u → Type v} [Monad m] [LawfulMonad m] [SeqComm m]
  {α β : Type u} (l : m α) (r : m β) :
  (do let l <- l; let r <- r; return (l, r)) = (do let r <- r; let l <- l; return (l, r)) := by
  convert SeqComm.seq_comm l r using 1 <;>
  simp [seq_eq_bind_map]

theorem SeqComm.bind_comm {m : Type u → Type v} [Monad m] [LawfulMonad m] [SeqComm m]
  {α β : Type u} (l : m α) (r : m β) (f : α → β → m γ) :
  (do let l <- l; let r <- r; f l r) = (do let r <- r; let l <- l; f l r) := calc
  _ = (do let l <- l; let r <- r; pure (l, r)) >>= (λ(l, r) => f l r) := by simp
  _ = _ := by rw [bind_pair_comm]; simp

Then any monad satisfying SeqComm (e.g. Option) would satisfy CommutativeMonad as well

[Bhavik Mehta]

I'd say strong monads are worth having from a mathematical point of view. I don't know if CommutativeMonad for type-valued monads are worth having: my inclination is that those would be valuable only if they're useful from a programming point of view.

[Jad Ghalayini]

Bhavik Mehta said:

I'd say strong monads are worth having from a mathematical point of view. I don't know if CommutativeMonad for type-valued monads are worth having: my inclination is that those would be valuable only if they're useful from a programming point of view.

Commutative monads should be useful for reasoning about programs since they allow re-ordering statements which do not share variables; a few good examples of such monads are Option, ReaderT, and WriterT when the underlying monoid is commutative.

For math, commutative monads give a lot of useful theorems; my goal is to show that strong monads induce a premonoidal category (PR https://github.com/leanprover-community/mathlib4/pull/21488) while commutative monads induce a monoidal category. Going further, a lot of linear algebra can be very elegantly derived from the fact that the free vector space monad is commutative; would be fun to see how this looks in general

[Bhavik Mehta]

I completely agree there are a lot of interesting theorems that could be proved for commutative monads!

[Jad Ghalayini]

Think it's worth it to put in a PR with what I've got now?

[Jad Ghalayini]

So just the strong monad stuff, and some little lemmas?

[Bhavik Mehta]

I'd say the strong monad stuff is worth a PR, yeah.

[Kim Morrison]

I'm a bit confused why everything is a class above.

[Jad Ghalayini]

@Kim Morrison tbf the main application I was thinking of was automatically instantiating things for monads over Set, and other similar cases

[Jad Ghalayini]

Eventually what I would like are theorems relating strong monads to monoidal/premonoidal categories