progress on universes

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

So as people who saw me waffling on on Friday will know, I kind of got obsessed with a universes issue. Dagur had clear ideas in his head about what he wanted source and target universes to be for the functor from e.g. compact Hausdorff spaces to condensed sets. However if you follow your nose and just apply Yoneda, this takes you from CompHaus.{u} to Condensed.{u} (Type u) and the latter category doesn't have limits because it's a small category. So Dagur wanted various variants on this functor with some u+1s in. Of course the first idea is to just write down the ULift functor Type u => Type (u+1) and then "use that Condensed is functorial". Of course you can push forward presheaves -- but what about sheaves? I was told that this was in the library and was called docs#CategoryTheory.sheafCompose , and indeed that looked good.

The problems began when I tried to apply this theorem:

variable {C : Type u₁} [Category.{v₁} C]
  {D : Type u₂} [Category.{v₂} D]
  (F : C ⥤ D)
  {J : GrothendieckTopology CompHaus.{0}}


set_option pp.universes true in
example [PreservesLimitsOfSize F] : Condensed.{0} C ⥤ Condensed.{0} D :=
  sheafCompose J F -- fails
/-
type mismatch
  sheafCompose.{0, 1, ?u.52605, ?u.52604} J ?m.52914
has type
  Functor.{1, 1, max ?u.52605 1, max ?u.52604 1} (Sheaf.{0, 1, 1, ?u.52605} J ?m.52610)
    (Sheaf.{0, 1, 1, ?u.52604} J ?m.52612) : Type (max 1 (max ?u.52605 1) ?u.52604 1)
but is expected to have type
  Functor.{max 1 v₁, max 1 v₂, max (max 1 v₁) u₁, max (max 1 v₂) u₂} (Condensed.{0, u₁, v₁} C)
    (Condensed.{0, u₂, v₂} D) : Type (max (max 1 v₁) (max 1 v₂) (max (max 1 v₁) u₁) (max 1 v₂) u₂)
-/

The universes don't add up. In fact if you switch universes on and look at sheafCompose you'll see that the morphism universes of both C and D have to be max u v where u,v are the universes for the base category with the topology -- but in particular they have to be equal to each other! Hence there is no way that you can use sheafCompose to go from Type u to Type (u+1) as Dagur wanted to do.

I took serious wrong turns twice when trying to fix this (first time I was beaten by the max u v = max u ? issue, second time I specialised to large categories too early), but I've finally got it working at least for the base category being CompHaus.{0}, which is a start. The product condition that one needs to ensure a functor F : C => D gives us Condensed.{0} C => Condensed.{0} D is PreservesLimitsOfSize.{1, 1, v₁, v₂, u₁, u₂} F, which perhaps implies some weird universe inequality of the form "if v1 and u1 are >= 1 then u2 had better be too" or some such thing?

I have had to generalise several definitions in mathlib, and I modified them by adding a prime. The primed definitions are more universe-general. I will try to PR something coherent to mathlib. I am hoping that this time the changes I'm proposing don't break a bunch of stuff (my last two attempts have been failures).

Here is the working gist, or look at the kb-condensed-functoriality branch of the Copenhagen repo.

[Kevin Buzzard]

#5659 it builds :-) Now I should be able to define the obvious functor from Condensed (Type u) to Condensed (Type max u v)!

[Kevin Buzzard]

On that branch, this code compiles:

import Mathlib.Condensed.Basic
import Mathlib.CategoryTheory.Sites.Whiskering

open CategoryTheory Limits

universe x v₂ v₁ u₂ u₁

variable {C : Type u₁} [Category.{v₁} C]
  {D : Type u₂} [Category.{v₂} D]
  (F : C ⥤ D)

def foo [PreservesLimitsOfSize F] : Condensed.{x} C ⥤ Condensed.{x} D :=
  sheafCompose _ F

set_option pp.universes true in
#check foo
/-
 ...
 [inst✝² : PreservesLimitsOfSize.{x + 1, x + 1, v₁, v₂, u₁, u₂} F]
 ...
-/

I think that instance is playing the role of x<=v1 etc. I had that code above on Thursday, but it just didn't compile back then because of the universe issue.

[Kevin Buzzard]

Next universe question: there's a ULift-type functor from CompHaus.{u} to CompHaus.{u+37}. Do we have that sheaves (of types, say) for the usual topology at level u+37 pull back to sheaves at level u? u is Scholze's kappa (I'm assuming we don't have to sheafify)

[Kevin Buzzard]

The theorem we need about ulift to prove that we can lift condensed sets is this:

import Mathlib.Condensed.Basic
import Mathlib.CategoryTheory.Sites.Whiskering

open CategoryTheory Limits

universe u

example (X : CompHaus.{u})
    (S : GrothendieckTopology.Cover.{u, u + 1} (coherentTopology.{u + 1, u} CompHaus.{u}) X)
      (P : CategoryTheory.Functor.{u, u, u + 1, u + 1} (Opposite.{u + 2} CompHaus.{u}) (Type u)) :
        PreservesLimit.{u + 1, u + 1, u, u + 17, u + 1, u + 18}
          (MulticospanIndex.multicospan.{u + 1, u, u + 1} (GrothendieckTopology.Cover.index.{u, u + 1, u, u + 1} S P))
          uliftFunctor.{u + 17, u} :=  sorry

(that's just an example of universes we'd like it to apply to)