universe restriction on limit

Stream: maths

[Andrew Yang]

The current limit API only allows one to talk about diagrams F: J ⥤ C with [category.{v v} J] and [category.{v u} C]. I could understand that one would rarely talk about big limits, but I suppose one would at times want to talk about smaller limits?
For example, the functor categories Type u ⥤ Type u should have all limits of size u, but not of size u+1. However I could not really state this since the hom-sets of Type u ⥤ Type u are large of size u+1 as well.

In case I am #xy-ing myself, this is what I was trying to do when I was stopped by this:
I was trying to define open subfunctors, and I would need to say that the pullback of F ⟶ G and hₓ ⟶ G is representable, but Lean does not know that such a pullback exists, since the proof that functor categories has limits is based on the pointwise limit and thus requires that the source category be smaller than the target so that the hom-sets of C ⥤ D is as big as the of D.

There are some alternatives to this, such as

1. Showing that C ⥤ Dhas limits of shape J if D has limits of shape J' and J ≌ J'.
2. Sticking a ulift_functor in the representable API.
3. Spell out the definition of the pullback in the definition of open subfunctors explicitly.

Though I do not know what the better way out of this is.

[Kyle Miller]

This might not be too related, but I had an issue where I wanted nonemptiness of limits of F : J ⥤ Type v with no universe constraints on J, though I was happy enough working with F.sections.nonempty. It has to do this song-and-dance to lift everything up to a common type universe to apply a theorem about limit cones and then lower it back down.

[Junyan Xu]

I think the universe restriction on J is also what prevents us from stating the sheaf condition on sites using limits, analogous to the opens_le_covercondition in Top.
Actually the limit definition unfolds exactly to the Hom functor definition currently in mathlib, with family_of_elements.sieve_compatible stating precisely the commutativity of triangles in the limit diagram (though for presieves/pretopologies there seems not to exist a categorical way to state the compatibility condition). I wonder why the sites side doesn't have the limit condition even for C small; it does have the equalizer condition which requires pullbacks in C and products in A.

Sheaves on sites don't require any relationships among the four universes of the two categories, while for presheaves in Top, the topological space and the morphisms in the category of values are required to lie in the same universe, which don't seem very consistent to me. Not thinking they should be changed now, just writing down some universe peculiarities I observed!

[Johan Commelin]

There was a little bit of discussion about universes and limits here as well: https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/finite.20powers.20.28biproducts.29
But not really any useful insights, I fear.

[Johan Commelin]

Over there I said:

Should we add an extra universe variable to the limit API? So that you can talk about limits of arbitrary size?
And then instances that say if you have all limits of shape D in universe v, then you also have all limits of shape D in universe 0.
Idem for going from v+1 to v.

I'm not sure if this will actually work. @Mario Carneiro @Reid Barton What do you think?

[Andrew Yang]

Junyan Xu said:

Sheaves on sites don't require any relationships among the four universes of the two categories, while for presheaves in Top, the topological space and the morphisms in the category of values are required to lie in the same universe, which don't seem very consistent to me. Not thinking they should be changed now, just writing down some universe peculiarities I observed!

I think it can be generalized easily as well. There were also requirements about the universes of sheaves on sites, but was just removed one or two weeks ago.
However, some important constructions (such as pullbacks) still require such restrictions, so I did not try to generalize them in the Top library.

[Andrew Yang]

There is also this

Bhavik Mehta said:

I started a refactor to mathlib generalising the universe variables for limits a few weeks ago, basically allowing us to talk about non-small limits as well - it mostly went pretty smoothly and I'm hoping to PR it soon

But this was a long while ago, so I wonder if there were some obstacles that prevented us from doing so.

[Reid Barton]

As far as I can recall we didn't have any concrete reason for the restriction on the universe level of the indexing category, we just thought we could avoid working with extra universe variables because the case of v-small limits is the main one, but we didn't think about examples like u-small limits in Type u -> Type u.

[Reid Barton]

Johan Commelin said:

Over there I said:

Should we add an extra universe variable to the limit API? So that you can talk about limits of arbitrary size?
And then instances that say if you have all limits of shape D in universe v, then you also have all limits of shape D in universe 0.
Idem for going from v+1 to v.

I don't think these instances will work, but the first one might be okay...

[Johan Commelin]

They would at least work as defs, right?

[Johan Commelin]

Which would already be an improvement over the current situation.

[Reid Barton]

Or lemmas :wink:

[Adam Topaz]

@Junyan Xu It's possible to state the sheaf condition as a limit, but one does indeed need to be careful with universes. I did it for LTE here: https://github.com/leanprover-community/lean-liquid/blob/f2031f391913325f7265cf3e2592d155c6cfc073/src/for_mathlib/sheafification/plus_sheaf_condition.lean#L42

[Adam Topaz]

Like Andrew said above, the universe restrictions on sheaves was just removed recently, and I guess the specialization to Top wasn't generalized yet. More precisely, in the file topology/sheaves/sheaf_condition/sites.lean, it should be possible to have the universes of the category C be completely unrelated to the ones for X : Top.{v}.

[Junyan Xu]

@Adam Topaz I looked at the file and I see that indeed the universe of the category D of values must be set at max v u because of the universe constraint on limit (which can be traced back to cone), so the sheaf condition via limit is less general/applicable than the ones in mathlib, and I imagine you may need to lift the universe when you apply the results in the file.

And it seems to me that you can simply take the full subcategory of the overcategory C/X with objects the arrows in the sieve as the diagram category, which inherits the functor P to D, instead of constructing a complicated multicospan diagram in many steps as you did in plus.lean. In the pretopology case, I believe using the sieves generated by the covering presieves is sufficient (direct analogue of opens_le_cover).

[Adam Topaz]

@Junyan Xu I think the limits end up being the same. The benefit of the multiequalizer thing is that it's as close to being defeq to the sheaf condition as you can get.

[Adam Topaz]

There is one additional annoying thing about trying to use limits over the subcategory assocaited to a a sieve, and that is that the natural category structure you obtain for S a sieve on X : C : Type u with category.{v} C has universe level category.{v}, which means that to take a limit you need your target category D to be category.{v} as well, unless you want to deal with all that as_small nonsense. This is bad in most applications, especially in LTE, where we want sheaves on Profinite.{u} which is a large category, hence you want to take sheaves valued in a category D with a category.{u+1} instance.

[Adam Topaz]

Of course, if we do end up relaxing all these universe restrictions, that might change!

[Junyan Xu]

Adam Topaz said:

the natural category structure you obtain for S a sieve on X : C : Type u with category.{v} C has universe level category.{v}

If we're talking about the over category C/X (or its subcategory), it seems to me that the type of morphisms is indeed : Type v, but the type of objects is : Type (max v u) because an object includes an object in C : Type u and a morphism in _ : Type v, and I see that we need to ulift the morphisms to use the category as an indexing category. Am I missing something? For the multicospan indexing category, the type of objects is also : Type (max v u), but the morphisms are now an inductive type with objects as arguments of the constructor, so the type of morphisms is now naturally (at least) : Type (max v u) as well, which is convenient.

I agree that the multiequalizer formulation is closer to the sheaf condition in terms of compatible, which may simplify the proof of the equivalence between the limit condition and the sheaf condition (is_sheaf_iff_multifork); however if you apply compatible_iff_sieve_compatible then I think the over category formulation becomes the closer one, and it might simplify the proofs in plus.lean (I'm not sure how much the proofs depend on the shape of the diagram), modulo the morphism lifting issue.

[Andrew Yang]

I have been experimenting with some universe generalizations over at #10243.
I've only generalized the essential parts of the limit API, and the rest of them (shapes, preserves, etc.) remains intact.
There are lots of minor fixes (type/universe annotations) here and there, and hopefully I have highlighted the consequential changes in the comments of the PR.

TL; DR:
I've added has_limits_of_size.{v₁ u₁} C, and has_limits is now an alias for has_limits_of_size.{v v} C.

This unlocks

instance functor_category_has_limits_of_size [has_limits_of_size.{v₁ u₁} C] :
  has_limits_of_size.{v₁ u₁} (K ⥤ C)

and also notations like

noncomputable example [has_finite_products C] (X : C) : C := ∏ (λ (i : fin 5), X)