## Stream: Is there code for X?

### Topic: Functor commutes with finite (co)limits

#### 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

#### Adam Topaz (Dec 15 2020 at 17:55):

@Bhavik Mehta any hints?

#### 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


#### Bhavik Mehta (Dec 15 2020 at 17:56):

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

#### Bhavik Mehta (Dec 15 2020 at 17:56):

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

#### 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

#### 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]


which is ugly!

Yeah....

#### 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 _


#### 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

#### Adam Topaz (Dec 15 2020 at 18:00):

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

#### Bhavik Mehta (Dec 15 2020 at 18:01):

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

Oh ok.

#### Adam Topaz (Dec 15 2020 at 18:01):

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

#### 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], ...

#### Kevin Buzzard (Dec 15 2020 at 18:01):

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

yeah that

#### Bhavik Mehta (Dec 15 2020 at 18:02):

I think they're both unfortunate though

Fair point

#### Adam Topaz (Dec 15 2020 at 18:02):

Yeah I agree.

Last updated: May 19 2021 at 02:10 UTC