UnivLE in CategoryTheory.Sites.SheafOfTypes ?

Stream: maths

[Kevin Buzzard]

Now we have docs#UnivLE I thought I'd try and get it working in a use case coming from #5659 , but I've failed to. Here's an overview of what is going on in master right now.

In CategoryTheory.Sites.Sheaf we have a fully universe-polymorphic definition of a sheaf. More precisely we have our base category {C : Type u₁} [Category.{v₁} C] (J : GrothendieckTopology C) with a topology, that we're going to put a sheaf on, and this sheaf is going to be a sheaf of As, where (for much of the file) {A : Type u₂} [Category.{v₂} A] is another category.

However later on in this file we roll back on A a bit, and on line 457 we have a new A, with variable {A : Type u₂} [Category.{max v₁ u₁} A], so now we have lost a degree of freedom (v₂). We're still working with sheaves of As on category C but now we only have three universe variables to play with, not four. If you change that max v₁ u₁ to a general v₂ then you start to get errors later on in the file. What's going on here? The issue is that we're applying intermediate lemmas which have max v₁ u₁ built into them. If you chase everything back then you get to docs#CategoryTheory.Equalizer.FirstObj in CategoryTheory.Sites.SheafOfTypes, which mathematically is the $\prod_{i\in I}\mathcal{F}(U_i)$ in the displayed equation here on the Stacks project. We're taking a product in A indexed by a set called $I$ in Stacks, and in Lean $I$ is a union of a bunch of morphisms in C, indexed over a bunch of objects in C, so has type max v₁ u₁ in Lean. We need to ensure that we can manipulate objects of this size in A and the current practice (written before UnivLE) was just to put an explicit restriction on the morphism universe to make everything work.

The point of #5659 is to show that we went too far in this approach, and some lemmas where A had morphism universe max v₁ u₁ can be relaxed back to morphism universe v₂; in particular the function which I wanted to use to do a universe bump in my application, now is sufficiently universe polymorphic in #5659. The PR has been delegated so I could just merge what I have. However the PR was written before UnivLE existed, and Oliver raised the question of whether one could now do better. Instead of having max v₁ u₁ everywhere, can I move back to v₂ under some inequality hypotheses? I thought I'd give it a try, and basically edit #5659 if I can get it working, and just merge it if I can't.

Currently I can't, so I thought I'd ask before I gave up (note that I don't need this generalisation; the point of #5659 was to observe that we can remove some of these restrictions for free -- they're just not needed at all).

Probably the place to start is docs#CategoryTheory.Equalizer.FirstObj , in SheafOfTypes. Just before that declaration we have (P : Cᵒᵖ ⥤ Type max v₁ u₁) which should probably now be taking values in Type v₂. Now we also change FirstObj to be in Type v₂ and Lean (correctly) starts complaining that it can't unify universes. We fix this with e.g.

variable [UnivLE.{u₁,v₂}]
variable [UnivLE.{v₁,v₂}]
variable [UnivLE.{max u₁ v₁,v₂}]

which we were expecting, but then unfortunately the file doesn't compile. The first error is

failed to solve universe constraint
  v₂ =?= max (max ?u.175258 ?u.175259) ?u.175260
while trying to unify
  Type v₂ : Type (v₂ + 1)
with
  Type (max (max u₁ v₂) v₁) : Type (max (max (u₁ + 1) (v₂ + 1)) (v₁ + 1))

Now my understanding is that Lean's universe logic is not strong enough to deduce that max a b is either a or b, and without this assumption I don't think we have a hope of unifying v₂ with max (max u₁ v₂) v₁ because in theory it could be bigger than both (in the sense that there might be model of Lean's universes where this max max really is bigger than v₂). So am I now stuck? Is there a way around this? Let me again stress that this is not blocking anything, it is just idle thoughts about whether I can make #5659 better.

[Scott Morrison]

I haven't looked at the code at all, but just from reading your messages it seems you're using UnivLE "wrong" (or at least expecting more of it than I'd planend).

The rule should be: when you used to write X : Type u Y : Type (max u v), now write X : Type u Y : Type v [UnivLE.{u,v}].

Instead you're introducing a whole new universe v₂, replacing max v₁ u₁.

Does that make sense? If not I better look at the code. :-)

[Kevin Buzzard]

In my example v2 was max(v1,u1) + 1. I wanted to use a certain function to bump a universe level up from u to u+1 and v2 was literally not equal to max(v1,u1). But maybe you're right and I need to rethink. A short answer to your message is that your u is my max(v1,u1) and your v is my v2.

[Scott Morrison]

I am confused by seeing that you have introduced three UnivLE hypotheses. That is new! :-)

[Scott Morrison]

and one of them mentions a max.

[Kevin Buzzard]

I (think I) want to say "v2 is >= both u1 and v1", because I want to say "some construction in the theory of sheaves works", and the construction involves (1) making an object of size max(u1,v1) and then (2) doing something in A with this object which implies that the morphisms of A live in a universe big enough to contain this object.

[Kevin Buzzard]

The three hypotheses were all the ways I could think of to say "v2 is bigger than both u1 and v1"

[Kevin Buzzard]

def Presieve (X : C) :=
  ∀ ⦃Y⦄, Set (Y ⟶ X)

has type Type (max u₁ v₁) (a collection of sets of morphisms, indexed over a set of objects), and that is my "small" universe.