Functor commutes with finite (co)limits

Stream: Is there code for X?

[Adam Topaz]

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

[Adam Topaz]

@Bhavik Mehta any hints?

[Bhavik Mehta]

My usual go-to is something like:

(J : Type v₁) [small_category J] [fin_category J] :
preserves_limits_of_shape J F

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

[Bhavik Mehta]

which is ugly!

[Adam Topaz]

Yeah....

[Bhavik Mehta]

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 _

[Bhavik Mehta]

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

[Adam Topaz]

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

[Bhavik Mehta]

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

[Adam Topaz]

Oh ok.

[Adam Topaz]

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

[Bhavik Mehta]

As in, you could alternatively do Π (J : Type v) [𝒥 : small_category J] , by exactI Π [fin_category J], ...

[Kevin Buzzard]

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

[Kevin Buzzard]

yeah that

[Bhavik Mehta]

I think they're both unfortunate though

[Kevin Buzzard]

Fair point

[Adam Topaz]

Yeah I agree.