Isomorphisms of categories

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have isomorphisms of categories?

Yes, I know "equivalence" is the correct thing, but sometimes categories are actually isomorphic. Do I have to use isomorphisms in the categories of categories?

[Simon Hudon]

Are the isomorphisms in Cat, the category of categories, not satisfactory?

[Adam Topaz]

It's okay (again, if you don't care about universes). But there are other things that I'm not sure about. E.g. does mathlib know how to produce an equivalence of categories from an isomorphism in Cat?

[Scott Morrison]

Probably not. You could add it easily enough.

[Scott Morrison]

However, something to think about:

1. perhaps the equations between functors in an isomorphism of categories hold definitionally --- now there's a danger that much later down the line Lean will slow down because it's relying on definitional equality, and so a "heavy refl" could appear at any time
2. alternatively, perhaps the equations only hold propositionally --- now there's the danger that after you convert your isomorphism to an equivalence, the unit and counit (which contain data, and might need things proved about them) will have definitions involving eq.rec, which is hard to reason about

[Scott Morrison]

I'm not truly confident that this is the case, but my feeling is that going directly to constructing an equivalence insulates you from both of these unhappy possibilities.

[Scott Morrison]

and that this is the reason why we don't already have something like this --- too often providing API that talks about equality of functors results in eq.rec terms appearing later, or heavy refl, so we tend to just avoid providing such API.

[Adam Topaz]

I didn't consider the slowdown issues. Thanks! I think for now I'll just define the two functors (which obviously compose to identities!), and provide an equivalence.

[Kevin Buzzard]

I have occasionally seen isomorphisms of large categories in the wild but I'm not sure they were ever useful, they were more of a quirky observation. Lenstra once asked me a question about being up an equivalence to an isomorphism and I found an obstruction in an $H^3$ IIRC

[Adam Topaz]

@Kevin Buzzard @Scott Morrison @Simon Hudon : #3762
The final equivalence is really an isomorphism:

def Monad_Mon_equiv : equivalence (Monad C) (Mon_ (C ⥤ C)) :=
{ functor := Monad_to_Mon _,
  inverse := Mon_to_Monad _,
  unit_iso := eq_to_iso (eq.symm to_of_mon_end),
  counit_iso := eq_to_iso of_to_mon_end }

[Adam Topaz]

Okay, I ended up adding the construction of an equivalence of categories given an isomorphism in Cat:
https://github.com/leanprover-community/mathlib/blob/c4136fdd683abfb6272d55f11fc033ca1c7bc229/src/category_theory/category/Cat.lean#L54
The Monad <-> Monoid equivalence is now an actual isomorphism in Cat:
https://github.com/leanprover-community/mathlib/blob/c4136fdd683abfb6272d55f11fc033ca1c7bc229/src/category_theory/monad/equiv_mon.lean#L177
I think this PR is ready for review.

[Adam Topaz]

Also, the most important question-- am I allowed to put :burrito: in the docstring?

[Kevin Buzzard]

Adam Topaz said:

Also, the most important question-- am I allowed to put :burrito: in the docstring?

I definitely think you should tag it burrito in case people search for it.

[Reid Barton]

Tags: just

[Jalex Stark]

(maybe reid's comment was entirely a joke, but anyway I'll point out that just_ification would be perfectly unambiguous, though also inscrutable to the uninformed.)

[Adam Topaz]

I'm still looking out for that "nlab-just" tactic...