## Stream: maths

### Topic: Highest universe level encountered in practice

#### Roman Bars (Mar 02 2021 at 04:10):

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

#### Mario Carneiro (Mar 02 2021 at 04:11):

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

#### Mario Carneiro (Mar 02 2021 at 04:12):

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

#### Mario Carneiro (Mar 02 2021 at 04:13):

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 (Mar 02 2021 at 04:15):

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 (Mar 02 2021 at 04:20):

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 (Mar 02 2021 at 04:23):

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 (Mar 02 2021 at 04:27):

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 (Mar 02 2021 at 05:55):

@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 (Mar 02 2021 at 05:58):

That would still only be Type 1 though, right?

#### Johan Commelin (Mar 02 2021 at 06:02):

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

#### Johan Commelin (Mar 02 2021 at 06:03):

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

#### Mario Carneiro (Mar 02 2021 at 06:03):

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

#### Johan Commelin (Mar 02 2021 at 06:03):

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

#### Johan Commelin (Mar 02 2021 at 06:04):

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

#### Mario Carneiro (Mar 02 2021 at 06:04):

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

#### Mario Carneiro (Mar 02 2021 at 06:05):

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 (Mar 02 2021 at 06:06):

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

#### Mario Carneiro (Mar 02 2021 at 06:07):

and it would be inconsistent to reflect it as a nat

#### Damiano Testa (Mar 02 2021 at 06:25):

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 (Mar 02 2021 at 06:26):

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 (Mar 02 2021 at 06:30):

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 (Mar 02 2021 at 06:37):

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 (Mar 02 2021 at 08:00):

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 (Mar 02 2021 at 08:02):

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 (Mar 02 2021 at 08:04):

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

#### Kevin Buzzard (Mar 02 2021 at 08:05):

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

#### Damiano Testa (Mar 02 2021 at 08:15):

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 (Mar 02 2021 at 08:16):

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

#### Kevin Buzzard (Mar 02 2021 at 08:27):

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

#### Damiano Testa (Mar 02 2021 at 08:44):

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 (Mar 02 2021 at 08:46):

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).

Last updated: May 10 2021 at 07:15 UTC