Highest universe level encountered in practice

Stream: maths

[Roman Bars]

What's the highest universe level you can think of that is necessary to formalize some non-artificial mathematical statement?

[Mario Carneiro]

Type 1 is the highest I have ever seen for non-artificial things

[Mario Carneiro]

Specifically, ordinal,cardinal, pSet and Set all live in Type 1

[Mario Carneiro]

I think it is best to think in ZFC terms, with things in Type 0 being "small" and things in Type 1 being "large", and don't even contemplate going higher

[Mario Carneiro]

It's generally a bad idea to use universe bumping constructions because they can't be iterated, so we do a fair bit of work to keep things "small", resulting in size considerations not unlike those you find in ZFC formalization

[Mario Carneiro]

The biggest blocker to formalizing cardinals without type 1 is that you have to take a quotient, so you really have to apply quotient.{1} unless you want setoid hell. But if you are okay with this, then cardinals are just types with an equivalence relation on them (and actually we already have such a thing, it's what data.equiv does), and you can construct ordinals in a similar way as an equivalence relation on bundled well orders, and then you don't need to leave Type 0 to do ordinals and cardinals

[Mario Carneiro]

The story with Set is similar, it's a quotient of pSet so maybe you can just live without it. But pSet is really a higher universe inductive:

/-- The type of pre-sets in universe `u`. A pre-set
  is a family of pre-sets indexed by a type in `Type u`.
  The ZFC universe is defined as a quotient of this
  to ensure extensionality. -/
inductive pSet : Type (u+1)
| mk (α : Type u) (A : α → pSet) : pSet

This quantifies over all types in the universe in order to populate the inductive, which gives it a lot of unique properties (like having an inaccessible cardinality), so I'm pretty sure you can't do this in Type 0 (not least because this inductive can be turned into a model of ZFC).

[Mario Carneiro]

I would be curious to see how large universes actually get in mathlib though, with a definition like "what is the highest substitution of a concrete universe level to a universe variable", and I wouldn't be too surprised if the answer is 2 or 3

[Johan Commelin]

@Roman Bars We haven't yet formalised etale cohomology. Once we do that, we'll have to decide whether we want it to be elegant or ugly. The elegant definition bumps universes up by 1.

[Mario Carneiro]

That would still only be Type 1 though, right?

[Johan Commelin]

Unless you start with an algebro-geometric object in Type 1.

[Johan Commelin]

I don't know whether these cohomology constructions are ever iterated...

[Mario Carneiro]

As I mention above, if the answer is "yes" then you will have to go with the ugly definition

[Johan Commelin]

Maybe in things like the minimal model program? Where you iterate things like taking canonical models, resolution of singularities, blow-ups, etc...

[Johan Commelin]

Some of those steps make use of cohomology to create a new ring/variety.

[Mario Carneiro]

The ability to iterate a construction a fixed finite number of times is almost useless for most mathematical applications

[Mario Carneiro]

if you want to iterate enough to eliminate all singularities, even if you know that finitely many iterations suffice, that's not good enough unless you know that e.g. 4 iterations suffice

[Mario Carneiro]

because the number of iterations here isn't a nat, it's encoded in universe level arithmetic

[Mario Carneiro]

and it would be inconsistent to reflect it as a nat

[Damiano Testa]

In fact, when resolving singularities by blow-ups, you can run into a situation where you do one blow up and then you can get any finite number of isolated singularities in the resulting blow up. Of course, on any given example you can then resolve each by a finite number of blow ups, but there is no a priori upper bound on the number.

However, if you have a bounded family of varieties, then I think that there is a bound on the number of blow ups, as a function of the family. These bounds tend to be gigantic, though.

[Damiano Testa]

This, however, does not necessarily mean that to "resolve singularities" you need to have these unbounded construction. It is simply saying that it is sufficient to do this! It is possible that there are different strategies for resolution that do not depend on doing blow ups...

[Mario Carneiro]

However, if you have a bounded family of varieties, then I think that there is a bound on the number of blow ups, as a function of the family. These bounds tend to be gigantic, though.

Right, this is the kind of not-useful bound I mean. If you translate this to a lean proof, the proof itself is required to be at least as large as the bound you want, meaning that if the bound depends on the instance itself then a finite fragment of mathlib is only going to be able to prove properties about a small fraction of all varieties and only with stupidly long proofs

[Johan Commelin]

What this means is that at some point we might want to do some careful universe lowering for some cohomology theories, because we might actually need it. But for now I wouldn't worry about this, because it's quite far down the road.

[Damiano Testa]

Somehow, in my mind, statements about "universe issues" are classified as "if you have them, you are not thinking about the right question". It would be great if there were a tactic for alerting you of this fact! :upside_down:

[Kevin Buzzard]

What do you think about the definition of the Picard group of a scheme as the units in the "Picard monoid" of isomorphism classes of quasicoherent sheaves under \tensor ?

[Kevin Buzzard]

Even adding in some finiteness condition on the scheme and sheaves still doesn't stop you temporarily popping into a higher universe

[Kevin Buzzard]

We ran into this sort of thing in the perfectoid project when defining the adic space as equivalence classes of valuations

[Damiano Testa]

I like the definition of Picard group! As I am learning Lean, I also realize that what is more important is how to relate it to other equivalent versions. In the case of Picard groups, the "divisors up to linear equivalence" point of view is also very useful.

[Damiano Testa]

This other approach might involve fewer universe jumps, but I do not really have a feeling for these universe issues.

[Kevin Buzzard]

So ring-theoretically the divisor rather than sheaf approach is of course like using ideals rather than modules

[Damiano Testa]

Yes, it is more "intrinsic", since you can work inside the ring itself, rather than "moving out" to modules. Honestly, my intuition for universes is closer to how I would think about first- and second- order sentences and range of quantification. Maybe this is not the right perspective.

[Kevin Buzzard]

Ideals do seem like a natural concept though. With valuations one seemed to have to move to some rather strange preorder -- two valuations v and w on a ring R are equivalent iff v(r)<=v(s) <-> w(r)<=w(s).