Zulip Chat Archive

Stream: Is there code for X?

Topic: Isomorphisms of categories


Adam Topaz (Aug 12 2020 at 22:23):

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 (Aug 12 2020 at 22:25):

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

Adam Topaz (Aug 12 2020 at 22:29):

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 (Aug 12 2020 at 22:37):

Probably not. You could add it easily enough.

Scott Morrison (Aug 12 2020 at 22:39):

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 (Aug 12 2020 at 22:40):

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 (Aug 12 2020 at 22:41):

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 (Aug 12 2020 at 22:50):

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 (Aug 13 2020 at 07:09):

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 H3H^3 IIRC

Adam Topaz (Aug 13 2020 at 14:34):

@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 (Aug 13 2020 at 15:58):

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 (Aug 13 2020 at 16:14):

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

Kevin Buzzard (Aug 13 2020 at 16:43):

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 (Aug 13 2020 at 16:46):

Tags: just

Jalex Stark (Aug 14 2020 at 22:42):

(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 (Aug 14 2020 at 22:44):

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


Last updated: Dec 20 2023 at 11:08 UTC