limits in functor categories

Stream: maths

[Scott Morrison]

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]

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]

(Assuming D has finite limits.)

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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

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

[Johan Commelin]

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]

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]

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]

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]

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]

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]

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