Universes restriction in Rep

Stream: mathlib4

[Riccardo Brasca]

Currently, the category docs#Rep wants the ring k and the group G to live in the same universe. In particular, in the case k is ℤ we have that G has to live in Type, for example in docs#Rep.ofAlgebraAut. This has the unpleasant consequence that all our cohomology computations, for example Hilbert's theorem 90, docs#sgroupCohomology.H1ofAutOnUnitsUnique is now restricted to K and L in Type.

Is this an accident or has someone already thought about this? Note that Hilbert's theorem 90 can be reformulated in very concrete terms, and it has nothing to do with cohomology or universes (see exists_div_of_norm_eq_one not yet in the docs).

[Eric Wieser]

abbrev Rep.{u, uk, uG} (k : Type uk) (G : Type uG) [Ring k] [Monoid G] :=
  Action (ModuleCat.{u} k) G

at least as a definition seems to work fine

[Eric Wieser]

Given it's an abbrev, I don't see what benefit the restriction would bring

[Yaël Dillies]

I am not sure where the universe restriction stemmed from, but it was very helpful at the CFT workshop in Oxford this summer to steer our many Lean beginners away from universe headaches

[Riccardo Brasca]

Well, I surely don't want to give universes headaches to beginners, but mathlib should be as general as possible, especially since later headaches are surely worse...

[Riccardo Brasca]

I am having a look at #33608, but it doesn't seem completely trivial.

[Riccardo Brasca]

I am not sure how to generalize the Type u in

/-- The monoidal functor sending a type `H` with a `G`-action to the induced `k`-linear
`G`-representation on `k[H].` -/
def linearization : (Action (Type u) G) ⥤ (Rep k G) :=
  (ModuleCat.free k).mapAction G

[Edward van de Meent]

I think the main hindrance is that ModuleCat.free isn't maximally universe polymorphic:

import Mathlib

universe u v w -- declare universes ahead of time for good ordering
namespace CategoryTheory


variable {k : Type v} [CommRing k] {G : Type w} [Monoid G]

/-- info: Rep.{u} (k G : Type u) [Ring k] [Monoid G] : Type (u + 1) -/
#guard_msgs in
#check Rep

-- a copy of the definition, with distinct universe variables
abbrev Rep' (k : Type v) (G : Type w) [Ring k] [Monoid G] := Action (ModuleCat.{u} k) G

/--
info: CategoryTheory.Rep'.{u, v, w} (k : Type v) (G : Type w) [Ring k] [Monoid G] : Type (max (max (max (u + 1) v) w) u)
-/
#guard_msgs in
#check Rep'

#check ModuleCat.free k

-- again a copy of the definition in Mathlib, but more polymorphism
noncomputable def _root_.ModuleCat.free' (R : Type v) [Ring R] : Type u ⥤ ModuleCat.{max u v} R where
  obj X := ModuleCat.of R (X →₀ R)
  map {_ _} f := ModuleCat.ofHom <| Finsupp.lmapDomain _ _ f
  map_id := by intros; ext : 1; exact Finsupp.lmapDomain_id _ _
  map_comp := by intros; ext : 1; exact Finsupp.lmapDomain_comp _ _ _ _

/-- The monoidal functor sending a type `H` with a `G`-action to the induced `k`-linear
`G`-representation on `k[H].` -/
noncomputable def linearization' : (Action (Type _) G) ⥤ (Rep'.{_} k G) :=
  (ModuleCat.free'.{u} k).mapAction G

set_option pp.universes true
#check linearization' -- `Action (Type u) G ⥤ Rep'.{max u v, v, w} k G`

end CategoryTheory

[Edward van de Meent]

all of which is to say, either a separate universe level, or the same universe level as k or G (presumably the first) when the prior is too general to be useful (in which case, because it's likely a net slowdown and doesn't have mathematical benefits, we don't want it)

[Riccardo Brasca]

Well the problem is that modifying free breaks essentially everything in the rest of the file, and I am afraid that in fixing it we will just find another problem. But let me see...

[Riccardo Brasca]

#33608 now compiles: it is still not enough, but it is a start. The next step is to generalize the monoidal structure on ModuleCat.{v}, but let's see how is the bench.

Tagging the usual suspects @Kevin Buzzard @Andrew Yang

[Riccardo Brasca]

Note that we can just say that all our concrete statements are about number fields or similar objects, so we may just ignore Type 37 and be happy with Type.

[Riccardo Brasca]

Bench is very bad :(

[Kevin Buzzard]

I suspect that many slow files in the algebra side of mathlib are because lean is being slow at solving universe problems. Can you make things better by giving more explicit universes?

[Riccardo Brasca]

I can try tomorrow, but I am wondering if the headache is worth or not. Currently Hilbert's theorem 90 is the statement

groupCohomology.exists_div_of_norm_eq_one {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
  [IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} (hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) {x : L}
  (hx : (Algebra.norm K) x = 1) : ∃ y, y / g y = x

and I have no idea if having K L : Type* is interesting or not. The theorem looks really less general, in the sense I am not sure we can deduce the general version by the current one (surely one can assume that L is in the same universe as K since the extension is finite, but K is a real issue).

[Kevin Buzzard]

Before I got interested in lean I had no interest in higher universes at all, and all the analysts are proving things about $\R$ and $\mathbb{C}$ and not Ulift.{u} Real so somehow they managed to get away with working in Type whereas whenever I suggest we do this in algebra I'm always told that we should use the full functionality of the system :-/

It wouldn't surprise me if you can prove the general theorem from the Type version; this feels like how EGA reduces everything to the Noetherian case. Given L/K a finite extension in some arbitrary universes, and x in L, find L0 and K0 finitely generated over their prime subfields and L0 containing x, with the same Galois group (this is exactly the kind of thing that one can do), find isomorphic fields in Type and etc etc. In fact I suspect that it's quite rare in practice that you can find a reasonable statement in algebra which can't be deduced from a result in Type.

[Riccardo Brasca]

I agree it's possible, it's just not super easy.

[Kevin Buzzard]

One could imagine a tactic doing it. One thing that really struck me about FLT was realising that all the groups, rings and fields which show up really are in Type.

[Riccardo Brasca]

I am thinking about sections of a sheaf obtained via sheafification, that I guess lives in a bigger universe, but I don't have a concrete example. Of course all our concrete case are doable in Type, but if you use the general construction the result may be in Type 1: well, you know very well the story about FLT and large cardinals :)

[Violeta Hernández]

I'm glad people care about non-zero universes because that means I can call ordinals a well-order and surreals a linearly ordered field without having to CAPITALIZE EVERYTHING LIKE CONWAY DOES FOR SOME REASON

[Scott Carnahan]

Waterhouse 1975 has an example of a presheaf on affine schemes that has no flat sheafification in the same universe. If you happen to want general sheafification to be a functor, then you need to raise the universe level.

[Nailin Guan]

Kevin Buzzard 說：

One could imagine a tactic doing it. One thing that really struck me about FLT was realising that all the groups, rings and fields which show up really are in Type.

I think it is really hard to have a tactic for this, since I have in mind that some categorical constructions aren't just trivially stable under change universes. Anyway, I remember some universe level of totally unrelated things need to be the same in Rep related stuffs, this indeed need some generalization.

[Kevin Buzzard]

Yes I totally agree that once you go to categories, you need universes.

[Scott Carnahan]

I suppose I should mention that Waterhouse's paper (Basically bounded functors and flat sheaves) does not really advocate raising the universe level. Instead, his position is more or less that we shouldn't consider "all presheaves", because there is a very well-behaved subcategory of presheaves for which sheafification is a functor to the same universe level, and this subcategory contains everything relevant to geometry.

[Violeta Hernández]

So we want to prove some theorems on nimbers and this universe restriction has come to bite us.

[Kevin Buzzard]

Well one option is to reopen Riccardo's PR, and argue that the bench isnt really bad because we're adding lots of new theorems (namely more polymorphic versions of current theorems). Maybe this is a bullet we have to bite.

[Edward van de Meent]

also, it's possible that the bench will improve now that #lean4 > kernel universe normalization issue is getting traction

[Kevin Buzzard]

Nothing has changed there yet (but I agree that it might cause an improvement if something is changed)

[Riccardo Brasca]

Note that my PR doesn't compile, I stopped fixing it at some point because of the bench.

[Riccardo Brasca]

There was something not completely trivial about ModuleCat being monoidal.

[Violeta Hernández]

Riccardo Brasca said:

I can try tomorrow, but I am wondering if the headache is worth or not. Currently Hilbert's theorem 90 is the statement

groupCohomology.exists_div_of_norm_eq_one {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
  [IsGalois K L] [IsCyclic Gal(L/K)] {g : Gal(L/K)} (hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) {x : L}
  (hx : (Algebra.norm K) x = 1) : ∃ y, y / g y = x

and I have no idea if having K L : Type* is interesting or not.

For context, we need the additive version of Hilbert 90 in order to prove that the nimbers 2^2^n are fields, and nimbers are a type alias of docs#Ordinal and thus come with a universe bump. The fields are finite, yes, but using Shrink here just introduces new headaches.