Definition of (category theory) monad

Stream: mathlib4

[Gareth Ma]

The assoc field of Monad is defined as

assoc : ∀ X, toFunctor.map (NatTrans.app μ X) ≫ μ.app _ = μ.app _ ≫ μ.app _ := by aesop_cat

Why is this definition used instead of the more natural / correct

whiskerLeft _ μ ≫ μ = whiskerRight μ _ ≫ μ

[Kenny Lau]

(you need \ggg right?)

[Gareth Ma]

No because \mu is a natural transformation

[Aaron Liu]

You are abusing the defeq that functor composition is associative

[Gareth Ma]

Yes

[Gareth Ma]

But they're defeq and Mathlib/CategoryTheory does that all the time anyways?

[Gareth Ma]

Or is it maybe because it was ported from Lean 3 and back then it wasn't defeq (I have no idea)

[Gareth Ma]

Okay a better question, is it a good idea to change this?

[Aaron Liu]

no the reason is that abusing defeq is bad

[Aaron Liu]

even though it's already done in a lot of places

[Gareth Ma]

How is it bad? Plus it's not even abusing defeq, and if you don't like it / want to recover the current definition just ext or ext1 or something

[Aaron Liu]

Gareth Ma said:

Plus it's not even abusing defeq

what?

[Robin Arnez]

I would consider the definition of defeq abuse to be "doesn't typecheck at reducible transparency":

import Mathlib

open CategoryTheory

variable {C : Type*} [Category.{v} C]

open private Lean.Meta.checkAux from Lean.Meta.Check

open Functor in
def test (x : Monad C) : whiskerLeft _ x.μ ≫ x.μ = whiskerRight x.μ _ ≫ x.μ := by
  sorry

open Lean Meta

/--
error: Application type mismatch: In the application
  x.whiskerLeft x.μ ≫ x.μ = Functor.whiskerRight x.μ x.toFunctor ≫ x.μ
the argument
  Functor.whiskerRight x.μ x.toFunctor ≫ x.μ
has type
  (x.toFunctor ⋙ x.toFunctor) ⋙ x.toFunctor ⟶ x.toFunctor : Type (max u_1 v)
but is expected to have type
  x.toFunctor ⋙ x.toFunctor ⋙ x.toFunctor ⟶ x.toFunctor : Type (max v u_1)
-/
#guard_msgs in
run_meta
  let val ← getConstVal ``test
  let type := val.type
  withReducible <| Lean.Meta.checkAux type

The problem here is that many tactics like simp operate on reducible transparency, so they might run into problems when trying to operate.

[Adam Topaz]

@Gareth Ma you could take a look at how we define docs#Mon_class (and also how Comon_class is used to define comonads in a bicategory in mathlib)

[Adam Topaz]

Note in particular the explicit use of associators and unitors

[Gareth Ma]

For monoidal categories it makes sense since that’s data

[Gareth Ma]

But here it’s defeq right

[Gareth Ma]

(I hope I’m understanding your point correctly, I’m on phone right now but I can double check later)

[Gareth Ma]

Or another question, is it a good idea to change the Monad assoc definition from the current one to what I suggested (with whiskering) but with associators added in

[Gareth Ma]

Functor.assoc or something iirc

[Aaron Liu]

I don't think we have the associators and unitor natural transformations for functor composition

[Aaron Liu]

I guess it's just eqToHom

[Joël Riou]

We used to abuse defeq for associators/unitors, but it turns out it is better practice to insert associators in definitions. Here it would be ok to make a lemma for this compatibility at the level of natural transformations, adding a different constructor, or even changing the definition.

[Gareth Ma]

No it's CategoryTheory.Functor.associator

[Aaron Liu]

Gareth Ma said:

No it's CategoryTheory.Functor.associator

Oh I must have missed it

[Gareth Ma]

Joël Riou said:

We used to abuse defeq for associators/unitors, but it turns out it is better practice to insert associators in definitions. Here it would be ok to make a lemma for this compatibility at the level of natural transformations, adding a different constructor, or even changing the definition.

So changing Monad.assoc definition to whiskerLeft _ μ \ggg Functor.associator something ≫ μ = whiskerRight μ _ ≫ Functor.associator something \ggg μ would fit what you're saying right

[Gareth Ma]

(Whatever the correct statement is)

[Adam Topaz]

Sure, I think such a defitinion could be made. But does this give any advantage?

[Adam Topaz]

Monads and comonads are inherently a 2-categorical thing, and IMO the right abstraction is at that level.

[Gareth Ma]

It’s what’s found in textbooks, you can recover the existing one with ext, but going the other way around seems more annoying (I used fun x -> congrArg (fun a -> a.app X or something)

[Adam Topaz]

I think if you want to work at the level of natural transformations without applying them to a particular object, then you should formulate things in terms of bicategories

[Adam Topaz]

cf docs#CategoryTheory.Bicategory.Comonad

[Gareth Ma]

Okay I will try that out then. I know it’s the natural place to do monad stuff but I just didn’t want to touch/learn it :) Thanks for the comments

[Gareth Ma]

So eg the statement “if a category has all limits then the codensity monad of a functor exists” should be in Bicategory?

[Robin Arnez]

For an example of defeq abuse, here:

import Mathlib

theorem List.findFinIdx?_cons_eq_some_succ_iff (p : α → Bool) (x : α) (l : List α) (i : Fin l.length) :
    (x :: l).findFinIdx? p = some i.succ ↔ p x = false ∧ l.findFinIdx? p = some i := by
  rw [findFinIdx?_cons]
  split
  · simp_all [(Fin.succ_ne_zero _).symm]
  · simp_all only [Option.map_eq_some_iff, Fin.succ_inj, exists_eq_right, Bool.not_eq_true, true_and]

-- basically the same statement
example (p : α → Bool) (x : α) (l : List α) (i : Fin l.length) :
    some i.succ = (x :: l).findFinIdx? p ↔ p x = false ∧ l.findFinIdx? p = some i := by
  rw [eq_comm]
  simp only [List.findFinIdx?_cons_eq_some_succ_iff] -- fails!!!

[Adam Topaz]

Gareth Ma said:

So eg the statement “if a category has all limits then the codensity monad of a functor exists” should be in Bicategory?

I think this is a statement about Kan extensions

[Gareth Ma]

Yes

[Robin Arnez]

In this example, the defeq abuse of (x :: l).length = l.length + 1 causes problems because the Eq in the statement is about Fin (x :: l).length and we use it on Fin (l.length + 1) later

[Gareth Ma]

Codensity monad = Right Kan extension of F along F exists

[Aaron Liu]

import Mathlib

universe u v

open CategoryTheory

def CategoryTheory.Monad.mk' {C : Type u} [Category.{v} C] (T : C ⥤ C) (η : 𝟭 C ⟶ T) (μ : T ⋙ T ⟶ T)
    (mul_assoc : CategoryTheory.Functor.whiskerRight μ T ≫ μ =
      (T.associator T T).hom ≫ CategoryTheory.Functor.whiskerLeft T μ ≫ μ)
    (one_mul : CategoryTheory.Functor.whiskerLeft T η ≫ μ = T.rightUnitor.hom)
    (mul_one : CategoryTheory.Functor.whiskerRight η T ≫ μ = T.leftUnitor.hom) : Monad C :=
  { T with
    μ, η
    assoc X := by simpa using congr(($mul_assoc).app X)
    left_unit X := congr(($one_mul).app X)
    right_unit X := congr(($mul_one).app X) }

[Gareth Ma]

Where can I learn more about the $ notation

[Gareth Ma]

Wth is that

[Aaron Liu]

it's a monad

[Aaron Liu]

see, there's the associativity, and there's the left and right unit equations

[Ruben Van de Velde]

The one in congr? That's part of the congr syntax itself

[Aaron Liu]

oh this works too

import Mathlib

universe u v

open CategoryTheory

def CategoryTheory.Monad.mk' {C : Type u} [Category.{v} C] (T : C ⥤ C) (η : 𝟭 C ⟶ T) (μ : T ⋙ T ⟶ T)
    (mul_assoc : CategoryTheory.Functor.whiskerRight μ T ≫ μ =
      (T.associator T T).hom ≫ CategoryTheory.Functor.whiskerLeft T μ ≫ μ)
    (one_mul : CategoryTheory.Functor.whiskerLeft T η ≫ μ = T.rightUnitor.hom)
    (mul_one : CategoryTheory.Functor.whiskerRight η T ≫ μ = T.leftUnitor.hom) : Monad C where
  toFunctor := T
  μ
  η
  assoc X := by simpa using congr(($mul_assoc).app X)
  left_unit X := congr(($one_mul).app X)
  right_unit X := congr(($mul_one).app X)

[Aaron Liu]

those lines with one character are so weird