Zulip Chat Archive

Stream: Is there code for X?

Topic: transport has_limits w.r.t. equivalence


view this post on Zulip Adam Topaz (Mar 15 2021 at 04:04):

Does mathlib know the following fact? If CC and DD are equivalent categories, and CC has (co)limits then DD has (co)limits.

view this post on Zulip Johan Commelin (Mar 15 2021 at 04:10):

This should be something like equivalence.preserves_limits

view this post on Zulip Johan Commelin (Mar 15 2021 at 04:10):

Ooh, that's not exactly it. I guess "creates limits"?

view this post on Zulip Adam Topaz (Mar 15 2021 at 04:12):

Yeah, we should have the fact that equivalences create limits.

view this post on Zulip Adam Topaz (Mar 15 2021 at 04:13):

But it seems like that's missing too. at least I can't find it.

view this post on Zulip Adam Topaz (Mar 15 2021 at 04:13):

I wanted this because I was going to make the has_limits/has_colimits instances for simplicial sets, but there were some stupid universe issues and I wanted to use the skeletal equivalence.

view this post on Zulip Scott Morrison (Mar 15 2021 at 06:10):

Eek. I'm not finding it either. @Bhavik Mehta?

view this post on Zulip Scott Morrison (Mar 15 2021 at 06:13):

(deleted)

view this post on Zulip Scott Morrison (Mar 15 2021 at 06:42):

#6687

view this post on Zulip Bhavik Mehta (Mar 15 2021 at 11:20):

docs#category_theory.adjunction.is_equivalence_creates_limits

view this post on Zulip Bhavik Mehta (Mar 15 2021 at 11:21):

It was already there

view this post on Zulip Scott Morrison (Mar 15 2021 at 11:31):

Oh, and even easier.

view this post on Zulip Scott Morrison (Mar 15 2021 at 11:31):

Scaling problems...

view this post on Zulip Bhavik Mehta (Mar 15 2021 at 11:34):

I think lots of the lemmas in that file can be hard to find, perhaps we should add something to the docstrings about them

view this post on Zulip Bhavik Mehta (Mar 15 2021 at 12:33):

Actually maybe it's sensible to move that file to limits.adjunction and possibly split some things off into limits.equivalence

view this post on Zulip Adam Topaz (Mar 15 2021 at 14:16):

Thanks @Bhavik Mehta I'm adding a def for transporting has_(co)limits instances across an equivalence.


Last updated: May 19 2021 at 02:10 UTC