Zulip Chat Archive

Stream: Is there code for X?

Topic: Functor commutes with finite (co)limits


view this post on Zulip Adam Topaz (Dec 15 2020 at 17:55):

What's the idiomatic way to say that a functor commutes with finite (co)limits?
I would like to be able to formulate the following definition in lean:
https://stacks.math.columbia.edu/tag/0034

view this post on Zulip Adam Topaz (Dec 15 2020 at 17:55):

@Bhavik Mehta any hints?

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:56):

My usual go-to is something like:

(J : Type vā‚) [small_category J] [fin_category J] :
preserves_limits_of_shape J F

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:56):

I should let you know that I'm trying to define flat functors as well

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:56):

in this branch: https://github.com/leanprover-community/mathlib/tree/flat

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:57):

I also suspect it might be nice to have abbreviations for preserves_terminal, preserves_binary_products etc

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:57):

in particular if you want to assume that F preserves finite limits the assumption you need is

  [āˆ€ (J : Type vā‚) [š’„ : small_category J] [@fin_category J š’„],
      @preserves_limits_of_shape _ _ _ _ J š’„ F]

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:58):

which is ugly!

view this post on Zulip Adam Topaz (Dec 15 2020 at 17:58):

Yeah....

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:59):

but the definition of having finite limits is:

def has_finite_limits : Prop :=
Ī  (J : Type v) [š’„ : small_category J] [@fin_category J š’„], @has_limits_of_shape J š’„ C _

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 17:59):

so we could just hide this like that and not have to worry about the ugliness in practice

view this post on Zulip Adam Topaz (Dec 15 2020 at 18:00):

Why do we need to tell lean about the small_category instance explicitly?

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 18:01):

I think it's a general thing about registering new instances inside binders

view this post on Zulip Adam Topaz (Dec 15 2020 at 18:01):

Oh ok.

view this post on Zulip Adam Topaz (Dec 15 2020 at 18:01):

Thanks. I'll play around with this for a bit.

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 18:01):

As in, you could alternatively do Ī  (J : Type v) [š’„ : small_category J] , by exactI Ī  [fin_category J], ...

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 18:01):

You might be able to sneak in a cunning by exactI after [small_category J]

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 18:01):

yeah that

view this post on Zulip Bhavik Mehta (Dec 15 2020 at 18:02):

I think they're both unfortunate though

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 18:02):

Fair point

view this post on Zulip Adam Topaz (Dec 15 2020 at 18:02):

Yeah I agree.


Last updated: May 19 2021 at 02:10 UTC