Zulip Chat Archive

Stream: Is there code for X?

Topic: Isomorphisms of categories


view this post on Zulip 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?

view this post on Zulip Simon Hudon (Aug 12 2020 at 22:25):

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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Aug 12 2020 at 22:37):

Probably not. You could add it easily enough.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 13 2020 at 16:14):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 13 2020 at 16:46):

Tags: just

view this post on Zulip 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.)

view this post on Zulip Adam Topaz (Aug 14 2020 at 22:44):

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


Last updated: May 16 2021 at 05:21 UTC