Universes

Stream: mathlib4

[Antoine Chambert-Loir]

Consider the following definition of a polynomial map between two modules (in forthcoming work by @María Inés de Frutos Fernández and me) :

/-- A polynomial map M → N between A-modules is a functorial family
  of maps R ⊗[A] M → R ⊗[A] N, for all A-algebras R -/
@[ext]
structure PolynomialMap (R : Type u) [CommSemiring R]
    (M : Type _) [AddCommMonoid M] [Module R M]
    (N : Type _) [AddCommMonoid N] [Module R N] where
  toFun (S : Type u) [CommSemiring S] [Algebra R S] : S ⊗[R] M → S ⊗[R] N
  isCompat {S : Type u} [CommSemiring S] [Algebra R S]  {S' : Type u} [CommSemiring S'] [Algebra R S'] (φ : S →ₐ[R] S') :
    φ.toLinearMap.rTensor N ∘ toFun S = toFun S' ∘ φ.toLinearMap.rTensor M

To make the definition work, it is necessary to limit the quantification and insist that S has Type u, and indeed Lean can decide that for themself as you observe when you replace S : Type u by S : Type _.

My issue is that I want to plugin general stuff with S = MvPolynomial ι R, and the universe builder imposes ι : Type u: Lean does not realize that this would work if, eg, ι := Fin n for a natural integer n, or more generally if ι : Type v with max u v = u. In have played a little bit with docs#ULift.down, but that becomes ugly.

Are there tricks to do that ?

One thing I can imagine, given f : PolynomialMap R M N, is constructing more general versions of toFun and isCompat which hold for any universes, but I don't know whether there are techniques for that.

[Antoine Chambert-Loir]

(For this I need, given S : Type vand any finitely generated subalgebra A of S, to define an algebra S' : Type u which is isomorphic to A.)

[Johan Commelin]

@Antoine Chambert-Loir I'm looking at https://www2.math.uu.se/~qimh/Polynomial%20Maps.pdf which defines the notion of numerical map. It is strongly related to polynomial map, but not exactly the same. However, it doesn't rely on any universes.

[Johan Commelin]

Would that notion work for you? It requires working with binomial rings, which might be a problem for your applications??

[Antoine Chambert-Loir]

I didn't know of that reference, which is nice, and which deserves to be formalizes as well. However, we want polynomial maps to study the divided power algebra, as in Roby's paper, and we will need more than that.

[Johan Commelin]

That is what I feared...

[Antoine Chambert-Loir]

On the other hand, the following thing “should” be known (and is mathematically obvious, and is implicitely used in everything about essentially small categories) :

import Mathlib.RingTheory.FiniteType

example {R : Type u} [CommSemiring R]
  (S : Type v) [CommSemiring S] [Algebra R S] [Algebra.FiniteType R S] :
  ∃ (A : Type u), ∃ (_ : CommSemiring A), ∃ (_ : Algebra R A),  ∃ (_: A ≃ₐ[R] S), True := by
  sorry

[Johan Commelin]

Yes, certainly

[Johan Commelin]

And it's also mathematically obvious that you only need to consider finite type R-algebras in the definition of polynomial maps.

[Johan Commelin]

So one thing you could do, is keep the current definition, with its restrictive universes, and then prove a lemma that deduces the more general statement for S that live in an arbitrary universe.

[Antoine Chambert-Loir]

Yes, I think I'll do that. (And my example is almost done, thanks to docs#Algebra.FiniteType.iff_quotient_mvPolynomial'')

[Kevin Buzzard]

Whenever I see this sort of thing (mathematicians doing serious things and being delayed because of spurious universe issues) my immediate thought is to just ignore the universes and make things less polymorphic. I bet my bottom dollar that nobody is ever going to come along in a few years' time and say "oh no, I desperately need this for different universes in my application", so my feeling is that it's just generalisation for navel-gazing's sake. Before I started on this lean thing I'd never heard of universes (full disclosure, this is a lie but I'm pretending it's true to make my point), and I cannot imagine an application of crystalline cohomology which would ever go outside Type. The community has this attitude that "they're there so we must ensure that we work in full generally" but as I've said many times, when I teach I just don't bother the students with the idea of universes at all and part of me can't see the point of them.

In short Antoine I would not be at all worried about you being not maximally universe polymorphic, this is already happening in the category of modules etc and nobody noticed in LTE.

[Antoine Chambert-Loir]

Yes, but if I do this less polymorphic, everything will have to be in Type.

[Ruben Van de Velde]

And? :)

[Antoine Chambert-Loir]

As Kevin says, nothing but the fact that this disturbs me.

[Kevin Buzzard]

If lean didn't have universes then we'd be in this situation anytway and no mathematician would be remotely bothered

[Kevin Buzzard]

Another alternative is to define copies of the naturals, integers, reals, and Fin n in an arbitrary universe, using ULift. I would imagine that people would be happy with this. That way you can just stick to one universe u and probably nobody will notice you're not being maximally polymorphic. The fact that nobody did this yet makes me think that secretly nobody actually cares

[Kevin Buzzard]

Good luck deciding whether the canonical 37-dimensional real vector space in universe u is supposed to be ULift (Fin 37 -> Real) or (Ulift (Fin 37)) -> Ulift Real.

[Yaël Dillies]

Correct answer: "canonical is meaningless" :wink:

[Anne Baanen]

Additionally, it is very much possible to retrofit more universe polymorphism once it's actually needed. For example, I recall that a lot of linear algebra definitions, especially on the dimension, started out with the field and the vector space living in the same Type u and this went well for years until we needed to change it.

[Antoine Chambert-Loir]

But here, there will be an issue, because a polynomial map is a functor, and it is not a priori clear that it suffices to define that functor on a given universe. (Although, as discussed above, in the present case, it does, but this requires a theorem.)

[Joël Riou]

Kevin Buzzard said:

I cannot imagine an application of crystalline cohomology which would ever go outside Type.

I do not agree! If X is a k-scheme.{0}, then the underlying category of the crystalline site X/W_n is not a small category, it may only be "essentially small" (for the étale site, it is not even be essentially small, unless we assume X is Noetherian and take a variant where we take only finite type étale maps to X instead of "locally of finite type").

If C : Type u is an abelian category (with morphisms in Type v), then the hom sets in the derived category will tend to be in Type (max u v) instead of Type v. (Then, if C is a category of sheaves on the typical algebraic geometry site, we go out of Type 0, see the file AlgebraicGeometry.Sites.BigZariski.) In certain circumstances, it is possible to show that some homs (e.g. Ext-groups) are small, but it is far from easy. (For example, if C is a Grothendieck abelian category, the homs in the derived category should be Small.{v}.)

When formalizing the localization of categories, I had to find a predicate which does not require to "quantify over all universes" in order to get a reasonably good API.

I am not saying that we should be universe polymorphic everywhere it is possible, and certainly in the first attempts to formalize a theorem, it is advisable to not care too much about it, but eventually some not-very-rewarding tasks of this type have to be done.

[Kevin Buzzard]

I definitely agree that for big sites you need to be careful with universes! But it is not clear to me that you ever need to do commutative algebra with a module whose underlying type is not a set (i.e. in Type 0), even if you're thinking about the (big) crystalline site.

[Joël Riou]

Actually, what I am saying is that even what we call the "small" étale/crystalline site does not have to be "small" in the type theoretical sense!

In mathlib, the small Zariski site shall definitely be small: for a topological space X : Type u, the type Opens X is also Type u because it is implemented using Set X. If instead, we had defined an open of X to be a topological space U : Type u equipped a map f : U → X that happens to be an open immersion, then this category of "open immersions to X" would be equivalent to Opens X, but it would be Type (u + 1)! (Anyway, I would agree that for coherent cohomology, Type 0 should be enough.)

Now, consider the small crystalline site attached to some X. However it is defined, it involves a nil-immersion of an open U of X to some scheme Y. Even if we choose U : Opens X (rather than saying U ⟶ X is any open immersion), we have to "choose" Y, and the consequence is that the underlying category of the small crystalline site shall be at least Type (u + 1). Similar remarks apply to the small étale site. (In case of the crystalline site, it might be possible to show that the category is essentially u-small, but still the natural universe parameter is greater than u.)

[Kevin Buzzard]

Yeah I definitely agree that we need universes to deal with what is going on there. But what I'm saying is that when you're actually doing commutative algebra rather than category theory, the objects are all sets.

[Kevin Buzzard]

The one possible counterexample I know to this would be defining etale or crystalline cohomology via some non-set limit over covers and you'll end up with abelian groups in a larger universe. And then I'm in two minds about whether we work to prove that they descend to a smaller universe (fortunately we still seem pretty far from this discussion!). But when doing the actual lifting calculations you're still working with two schemes in Type.

[Kevin Buzzard]

Looking forward to AIM :-)

[Antoine Chambert-Loir]

Kevin Buzzard said:

Good luck deciding whether the canonical 37-dimensional real vector space in universe u is supposed to be ULift (Fin 37 -> Real) or (Ulift (Fin 37)) -> Ulift Real.

Well, after having thought about it, I believe it should be the latter.

[Kevin Buzzard]

In which case you can at least move from your initial worry ("everything needs to be in Type and that feels weird") to perhaps something that will worry you less and which is already happening in some places in category theory ("everything needs to be in the same universe u") by using a universe-polymorphic Fin n.

[Eric Wieser]

Good luck persuading core that docs#Fin and docs#Nat should be universe polymorphic.

[Eric Wieser]

(I'm not convinced it's a good idea myself, but I doubt my attempt to make IO universe polymorphic is going to go anywhere either)

[Eric Wieser]

One obvious downside to making Nat universe-polymorphic is that you need a definition Nat.universeJump, and a theorem about every single operation that you might perform on Nat commutes with it. Things aren't quite as bad with ULift.up, as at least we don't have to show that factorial commutes with it

[Kevin Buzzard]

I was imagining doing this in mathlib, and just for Fin n for now, which would solve Antoine's original problem.

[Geoffrey Irving]

Could I get the beginners explanation for why the solution isn't to make Type n a subtype of Type (n+1)? Is it just that dependent type theories (and inference algorithms) are generally allergic to subtyping, even in very regular cases?

[Kevin Buzzard]

Good luck persuading core of that too:-)

[Anatole Dedecker]

IIRC some implementations of CIC do that (I’m tempted to say that’s the case in Coq, but the truth is that universe management in Coq seems to be quite different to what it is in Lean, and comes with its own problems)

[Mario Carneiro]

Coq definitely has universe cumulativity. It also has both "parametric universes" i.e. constants with universe arguments like lean, as well as "symbolic universes" (forget the actual name) which are constants that have "fixed" but abstract universes, as though you defined a constant u : Universe and used it in a given definition. This latter category has no equivalent in lean; Coq has to maintain a partial ordering on all symbolic universes and every use of a constant or implicit application of cumulativity introduces a new ordering constraint, and Coq will give an error if the partial order ever becomes inconsistent. (This all seems quite nightmarish and I'm glad Lean steered clear of it.)

[David Michael Roberts]

Yaël Dillies said:

Correct answer: "canonical is meaningless" :wink:

Canonical answer, even.

[David Michael Roberts]

I was going to say something about sheafification on the fpqc site of a field being universe raising as well as being possibly dependent on the choice of larger universe, but apparently this is just ignored by people actually doing algebraic geometry :-)

[Antoine Chambert-Loir]

(there's no “ironic” emoji, alas...)

[Kevin Buzzard]

Joel's comments indicate that there are people doing algebraic geometry here who understand this sort of thing all too well! Fortunately (unfortunately?) we're still not at the point where we have to worry about this in Mathlib's development of algebraic geometry. Roll on AIM!

[Joël Riou]

Antoine Chambert-Loir said:

My issue is that I want to plugin general stuff with S = MvPolynomial ι R, and the universe builder imposes ι : Type u: Lean does not realize that this would work if, eg, ι := Fin n for a natural integer n, or more generally if ι : Type v with max u v = u. In have played a little bit with docs#ULift.down, but that becomes ugly.

Could you try ι : Type because then Lean should be able to see that MvPolynomial ι R is in Type u?

[Antoine Chambert-Loir]

But if I use ι : Type in the general function, I won't be able to apply it when ι is another universe.
I decided to take the steepest way, namely agreeing that PolynomialMap restricts universes (as it must), but I will provide the general theorem without any restriction. And then ι will be allowed to live in any universe it pleases them.