Universe issues with concrete categories

Stream: mathlib4

[Markus Himmel]

Hi, could someone help me with !4#3073? The problem is in the following definition:

def limitπMonoidHom (F : J ⥤ MonCat.{max v u}) (j) :
    (Types.limitCone.{v, u}
      (F ⋙ forget.{(max v u) + 1, (max v u), (max v u)} MonCat.{max v u})).pt →*
      (F ⋙ forget.{(max v u) + 1, (max v u), (max v u)} MonCat.{max v u}).obj j
    := sorry

Even though I believe that I have provided all possible universe levels, I'm getting the following error message:

stuck at solving universe constraint
  max (v+1) (?u.10252+1) =?= max (u+1) (v+1)
while trying to unify
  (J ⥤ MonCat) J inst✝ (J ⥤ MonCat) (J ⥤ MonCat)
with
  J ⥤ MonCat

With pp.all, the error message becomes

stuck at solving universe constraint
  max (v+1) (?u.10252+1) =?= max (u+1) (v+1)
while trying to unify
  (@CategoryTheory.Functor.{v, max ?u.10252 v, v, max (?u.10252 + 1) (v + 1)} J inst✝ MonCat.{max v ?u.10252}
      MonCat.largeCategory.{max ?u.10252 v})
    J inst✝
    (@CategoryTheory.Functor.{v, max ?u.10252 v, v, max (?u.10252 + 1) (v + 1)} J inst✝ MonCat.{max v ?u.10252}
      MonCat.largeCategory.{max ?u.10252 v})
    (@CategoryTheory.Functor.{v, max ?u.10252 v, v, max (?u.10252 + 1) (v + 1)} J inst✝ MonCat.{max v ?u.10252}
      MonCat.largeCategory.{max ?u.10252 v})
with
  @CategoryTheory.Functor.{v, max u v, v, max (u + 1) (v + 1)} J inst✝ MonCat.{max v u} MonCat.largeCategory.{max u v}

I'm not really sure what to make of the first term though.

[Adam Topaz]

It seems to be an issue with the typeclass inference

[Adam Topaz]

Eg. this works:

def limitπMonoidHom (F : J ⥤ MonCat.{max v u}) (j : J) :
  letI α : Type _ := (Types.limitCone.{v, u} (F ⋙ forget MonCat)).pt
  letI β : Type _ := ((F ⋙ forget MonCat.{max v u}).obj j)
  letI : Monoid α := inferInstance
  letI : Monoid β := show Monoid (F.obj j) from inferInstance
  α →* β := sorry

[Adam Topaz]

And if you replace the show ... with just inferInstance, you get a similar error.

[Adam Topaz]

Or slightly cleaner:

def limitπMonoidHom (F : J ⥤ MonCat.{max v u}) (j : J) :
  letI : Monoid ((F ⋙ forget MonCat.{max v u}).obj j) :=
    show Monoid (F.obj j) from inferInstance
  (Types.limitCone.{v, u} (F ⋙ forget MonCat)).pt →*
    ((F ⋙ forget MonCat.{max v u}).obj j) := sorry

[Markus Himmel]

This works, thank you.

[Kevin Buzzard]

Unfortunately I don't think this idea scales. Here is what I think is the same problem, minimised from CategoryTheory.Sites.Limits.

-- lean 3
import category_theory.limits.creates
import category_theory.sites.sheafification

open category_theory category_theory.limits

universes w v u

variables {C : Type max v u} [category.{v} C] {J : grothendieck_topology C}

variables {D : Type w} [category.{max v u} D]

instance [has_colimits D] : has_colimits (Sheaf J D) := sorry

example [has_colimits D] : has_colimits (Sheaf J D) := infer_instance -- works

vs

-- lean 4
import Mathlib.CategoryTheory.Limits.Creates
import Mathlib.CategoryTheory.Sites.Sheafification

open CategoryTheory Limits

universe w v u

variable {C : Type max v u} [Category.{v} C] {J : GrothendieckTopology C}

variable {D : Type w} [Category.{max v u} D]

instance [HasColimits D] : HasColimits (Sheaf J D) := sorry

example [HasColimits D] : HasColimits (Sheaf J D) := inferInstance
/-
stuck at solving universe constraint
  max (max u v) w =?= max (max v w) ?u.569
while trying to unify
  HasColimitsOfSize (Sheaf J D)
with
  (HasColimits (Sheaf J D)) ((HasColimits (Sheaf J D)) C inst✝² J D inst✝¹)
    ((HasColimits (Sheaf J D)) C inst✝² J D inst✝¹)
scratch1.lean:14:0
stuck at solving universe constraint
  max u v =?= max v ?u.569
while trying to unify
  HasColimitsOfSize (Sheaf J D)
with
  (HasColimits (Sheaf J D)) ((HasColimits (Sheaf J D)) C inst✝² J D inst✝¹)
    ((HasColimits (Sheaf J D)) C inst✝² J D inst✝¹)
-/

Basically, the instances in CategoryTheory.Sites.Limits don't fire right now.

[Kevin Buzzard]

This workaround:

instance foo [HasColimits D] : HasColimits (Sheaf J D) := sorry

example [HasColimits D] : HasColimits (Sheaf J D) := foo.{_, _, u}

is no good, because it's not just a definition failing, it's an instance, so the instance will never fire.

[Reid Barton]

Yeah this new universe level normalization doesn't get along well with our "use max to encode inequality constraints" trick.

[Reid Barton]

What's the whole #print foo output with universes turned on?

[Kevin Buzzard]

def foo.{w, v, u} : ∀ {C : Type (max v u)} [inst : CategoryTheory.Category.{v, max u v} C]
  {J : @CategoryTheory.GrothendieckTopology.{v, max u v} C inst} {D : Type w}
  [inst_1 : CategoryTheory.Category.{max v u, w} D] [inst_2 : @CategoryTheory.Limits.HasColimits.{max u v, w} D inst_1],
  @CategoryTheory.Limits.HasColimits.{max u v, max (max w u v) v}
    (@CategoryTheory.Sheaf.{v, max u v, max u v, w} C inst J D inst_1)
    (@CategoryTheory.Sheaf.instCategorySheaf.{v, max u v, max u v, w} C inst J D inst_1) :=
@foo.proof_1.{v, u, w}

[Reid Barton]

max (max w u v) v

:thinking:

[Kevin Buzzard]

I think the real issue is that u never occurs alone, so max u v = max ? v doesn't have a unique solution (for example ? could be max u v)

[Reid Barton]

Yeah so u never appears alone... yes.

[Reid Barton]

In Lean 3 we got by with this because it didn't do this level normalization, and then when faced with unification problems like the one you suggest, it would just pick u as the solution (even though as you point out there are others) and it was generally correct to do so.

[Kevin Buzzard]

Are there situations where it's necessary to ensure that one universe is <= another?

[Reid Barton]

If we could express inequalities directly then we could state u >= v instead of introducing this max u v thing, and then u would appear alone all over the place.

[Kevin Buzzard]

I've changed the type of C to Type u and so far so good...

[Reid Barton]

Yes frequently, e.g., Type u has w-small colimits if w <= u.

[Reid Barton]

I am not entirely sure if they are needed in your snippet--I mean with the sorry filled in of course!

[Kevin Buzzard]

Yikes, so it's probably important in this file.

[Reid Barton]

Can you paste the #print foo output like above but if you change C to Type u?

[Kevin Buzzard]

def foo.{w, v, u} : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {J : @CategoryTheory.GrothendieckTopology.{v, u} C inst} {D : Type w}
  [inst_1 : CategoryTheory.Category.{max v u, w} D] [inst_2 : @CategoryTheory.Limits.HasColimits.{max u v, w} D inst_1],
  @CategoryTheory.Limits.HasColimits.{max u v, max (max (max w u) u v) v}
    (@CategoryTheory.Sheaf.{v, max u v, u, w} C inst J D inst_1)
    (@CategoryTheory.Sheaf.instCategorySheaf.{v, max u v, u, w} C inst J D inst_1) :=
@foo.proof_1.{u, v, w}

and inferInstance works now.

[Reid Barton]

FWIW I don't see why the C : Type (max v u) should have been needed here.

[Reid Barton]

On https://github.com/leanprover-community/mathlib/blob/4f4a1c875d0baa92ab5d92f3fb1bb258ad9f3e5b/src/category_theory/sites/limits.lean#L169 one could try changing it to C : Type u.

[Reid Barton]

That said, this issue will probably pop up again

[Kevin Buzzard]

I've just done the entire file in mathlib 4 and indeed C : Type u works fine and all the problems go away

[Reid Barton]

If it works here then I definitely wouldn't expect any (serious) issues in downstream modules

[Kevin Buzzard]

I should backport anyway, just to check.

[Kevin Buzzard]

I don't know this material too well by the way: are you happy with leaving [Category.{max v u} D]? I was a bit surprised by this -- it's the objects of C which had type max v u and the morphisms of D.

[Reid Barton]

I think this might be somewhat artificial to make sure that "HasColimits" refers to max v u-sized ones, which are the ones you need to construct the sheafification

[Reid Barton]

It's possible you could also generalize the morphism universe of D by using HasColimitsOfSize

[Adam Topaz]

IIRC a lot of this universe gymnastics was due to the universe restrictions we had in the limits library (which were later relaxed).

[Adam Topaz]

I don’t remember exactly, but I think the max v u for C in this case was a way to make things work with the universe restrictions that we had in colimits of functors and in sheafification(which has some colimits and limits under the hood). Again, I’m not surprised that all this can be generalized now that we can have arbitrary universes in indexing categories of (co)limits.

All that having been said, it would be SO MUCH nicer if we could have universe inequality.

[Kevin Buzzard]

We have u+1. Will this do in practice?

[Reid Barton]

Yeah I was wondering if that was the order of history here

[Yaël Dillies]

Kevin Buzzard said:

We have u+1. Will this do in practice?

That's a strict inequality, right? Looks like people here were talking about non strict ones. Do both occur?

[Kevin Buzzard]

Yeah, but in practice every category is either a small category or a large category, so u or u+1.