## Stream: maths

### Topic: limits in functor categories

#### Scott Morrison (Sep 05 2020 at 07:58):

First, to #xy my problem: now that we know that filtered colimits commute with finite limits in Type, I would like to conclude as cheaply as possible things like X ↦ X × X and X ↦ X × X × X preserved filtered colimits.

#### Scott Morrison (Sep 05 2020 at 08:00):

I was hoping that I could prove that PreservesFilteredColimits, the category of functors C ⥤ D bundled with a witness that the functor preserves filtered colimits, itself has_finite_limits.

#### Scott Morrison (Sep 05 2020 at 08:00):

(Assuming D has finite limits.)

#### Scott Morrison (Sep 05 2020 at 08:01):

Then I'd plan to specialize to C = D = Type u, and notice that X ↦ X × X is the product of the identity functor with itself, and so preserves filtered colimits, etc.

#### Scott Morrison (Sep 05 2020 at 08:01):

The problem I've run into is just that has_limits D is not enough to conclude has_limits (C ⥤ D) in our current setup --- or rather, we can do this, but only when C is a small category.

#### Scott Morrison (Sep 05 2020 at 08:02):

And hence I wouldn't be able to specialize to C = D = Type u.

#### Scott Morrison (Sep 05 2020 at 08:02):

maybe I am just being stupid about universes tonight (always?), but I'm confused about what I'm meant to be doing, so if anyone knows what I'm doing wrong please tell me about it!

#### Scott Morrison (Sep 05 2020 at 08:04):

(For what it's worth, I did prove earlier, directly, that products of functors which preserve filtered limits themselves preserve filtered limits, so I'm not stuck. I'd just like to derive this from the general machinery, and not have to do any further arguments about filtered categories.)

#### Scott Morrison (Sep 05 2020 at 08:05):

(I did get bored proving the same thing for equalizers directly, so I would like to conclude this from the #4046.)

#### Johan Commelin (Sep 05 2020 at 15:31):

Hmmm... I don't have a good solution... Refactoring to allow "big" limits sounds like it will cause a lot of pain in many other places.

#### Reid Barton (Sep 05 2020 at 15:41):

This is more like allowing "small" limits I guess. The category of functors from Type u to Type u only has u-small limits but its hom sets are bigger than that.

#### Reid Barton (Sep 05 2020 at 15:45):

But I think the statement "the category of filtered colimit-preserving functors C -> D has finite limits" isn't actually the statement you want, anyways. For one thing, a priori those limits could differ from the ones in the ambient category of all functors C -> D. But also, even if you know they're the same, you still need to then use the extra information that the latter ones can be computed objectwise.

#### Reid Barton (Sep 05 2020 at 15:47):

So I think what you want to say is really that an objectwise finite limit of filtered colimit-preserving functors is filtered colimit-preserving, or maybe even better, that given a cone on a finite diagram of filtered colimit-preserving functors which is objectwise a limit cone, the vertex functor is also colimit-preserving.

#### Reid Barton (Sep 05 2020 at 15:48):

The statement got a lot longer, but I think it's closer to both what you want to apply and what you want to prove (I could be wrong though).

#### Scott Morrison (Sep 06 2020 at 04:27):

Thanks, that's helpful. (For my original plan, I'd wanted to prove not just has_finite_limits but also a preserves_limits for the forgetful functor, but I agree this would be cumbersome to use.)

At some point we should work out how to formalise that Type u ⥤ Type u has u-small limits nicely, as it's not so great this is currently hard to state. Perhaps we just say for every J at the appropriate level, it has limits of shape ulift J (for some appropriate definition of ulift which I think doesn't currently exist).

#### Bhavik Mehta (Sep 11 2020 at 03:06):

I'm not sure to what extent this helps, but for what's currently in limits/functor_category (and I imagine for what's in the new version too), you can generalise where the category you called C isn't small, but instead just has its objects living in the same universe as the morphisms of D - this lets you use the stuff that's already there to get:

example : has_limits.{u+1} (Type u ⥤ Type (u+1)) := by apply_instance


for instance

Last updated: May 10 2021 at 06:13 UTC