Universe issues in algebraic geometry

Stream: mathlib4

[Kenny Lau]

Following a discussion between me and @Andrew Yang long time ago, basically we concluded that it might be better to only define the affine space A^n_S (over scheme S) for S : Scheme.{u} and n : Type u.

What do you guys think about this? I'm encountering similar issues when trying to define related spaces. Basically the biggest issue is that if S and n are in different universes, and we define A^n_S to be in Type (max u v), then it no longer has a canonical map to S,

and another technical issue is that Lean is very slow with universes unification.

[Kenny Lau]

How is this actually handled in mathematics (with Grothendieck universes?)

[Riccardo Brasca]

Kenny Lau said:

How is this actually handled in mathematics (with Grothendieck universes?)

I am afraid in math this is just ignored...

[Kenny Lau]

Yes, I'm sure 90% of the mathematicians would just ignore it. But what do the remaining 10% think? Or is it not an issue because Grothendieck universes are cumulative (so S actually lives in Type (max u v))?

[Riccardo Brasca]

Yes, that seems a reasonable answer

[Kenny Lau]

@Riccardo Brasca do you know anyone here who might be interested in this question?

[Edward van de Meent]

maybe it makes sense to define a ulift function/functor on Schemes?

[Edward van de Meent]

or does that run into issues?

[Kenny Lau]

ulift should be fine, it might also be the preferred solution. I was talking with someone else who suggested that in infinity category theory they also solved this issue by putting everything in the same universe.

[Robin Carlier]

To be more precise about the last statement: the currently most used model for infinity categories is quasicategories, which are certain kind of simplicial sets, to (formally) make sense of that you need to pick a universe for the category of sets. This is why the nerve of a Type u with a Category.{v} instance lives in SSet.{max u v}.

[Joël Riou]

Kenny Lau said:

Following a discussion between me and Andrew Yang long time ago, basically we concluded that it might be better to only define the affine space A^n_S (over scheme S) for S : Scheme.{u} and n : Type u.

That would be fine for me.
(And, unless there is no other option, I do not think we need do define a ulift functor for schemes)

[Antoine Chambert-Loir]

I find this very strange: this means that for a ring R : Type 1, there will be no affine plane Aff^2_R?

[Andrew Yang]

The plan is to use ULift (Fin 2)

[Antoine Chambert-Loir]

My point of view on universes is orthogonal to everything that I read here: it is that it is the duty of the formalizing process to make them invisible, not to restrict to adequate universes.

[Antoine Chambert-Loir]

It may be more difficult in some cases than in some other, but for an example that I PRed recently with Maria-Inés, see #26719

[Kevin Buzzard]

Why don't we just demand that n's universe is <= S's universe? Then there will be a map to S

[Kenny Lau]

if you don't put them in the same universe, then that's saying S : Scheme.{max u v} and n : Type v and that's more debt for the Lean universe handler

and also the fact that we want to generalise it to the projectivisation of an arbitrary module M over R, and if you do this approach (universe(M) <= universe(R)) then you'll find that actually all of the instances you care about attain the equality

[Kevin Buzzard]

I think that there will be plenty of people who have been conditioned to write S : Scheme.{u} and when they find they can't write affine 1-space without some uLift of Fin 1 to Type u then they will be in situation where an instance they care about does not attain the equality.

[Joël Riou]

I would say either we keep the current situation (with the affine space in max u v, which will work just fine when n : Type or n : Type u), or we should provide a special API for the n-dimensional affine space when n is a natural number.

[Kevin Buzzard]

Oh yes that's a good point! If we leave it as it is then it works fine for Fin n.

[Kenny Lau]

What do people think about allowing morphisms of schemes in different universes? That would make the situation closer to our existing situation with rings where tensor product can be taken of any two rings

[Joël Riou]

Scheme.{u} is a category. I do not think we want to have heterogeneous universes here. We have sufficiently many issues with universes; there is no need to create more!
Scheme.{0} should be good enough for the foreseable future (including FLT), I would say...

[Kevin Buzzard]

It will be enough for (the modernisation of) Wiles' paper, which is the first goal.