!4#5519 - Algebra.Category.FGModuleCat.Limits

Stream: mathlib4

[Thomas Murrills]

I took a look at the help-wanted's, and I think that the error here might be a subtle universe error. Changing J from: Type to : Type v makes that instance work out (but breaks other definitions); but I think the root of the issue here is a maybe-unnecessary coincidence in universe levels arising from the use of ModuleCat.piIsoPi.

In that file (Algebra.Category.ModuleCat.Products), we define things under the assumptions

variable {ι : Type v} (Z : ι → ModuleCat.{v} R)

But the universe of ι should not always need to coincide with the universe v in ModuleCat.{v}—in parts of that file (and in the file being ported, with ι = J) we actually have

ModuleCat.of.{v,u} R (∀ i : ι, Z i) : ModuleCat.{v, u} R

so the type of the argument of Z only needs to live in a universe ≤ v, not necessarily v itself. Of course, trying to change things in the obvious way makes a bunch of other things break (whether asking for J : Type v or ι : Type v'); I just wanted to share the observation in case it helps someone more familiar with these issues figure it out. :)

[Thomas Murrills]

(I don't really understand how the errors emerge either; if you try to phrase the needed inequality as variable {ι : Type v} (Z : ι → ModuleCat.{max v v', u} R), then you hit errors like stuck at solving universe constraint max v ?u.3769 =?= max v v'—which looks very solvable, but I suppose something must be pushing the MCtx depth somewhere, and I'm not sure what...)

[Kevin Buzzard]

Lean 3 used to be able to solve this universe constraint by setting ?u.3769=v', but Lean 4 (implicitly) is imagining that there could in theory be more solutions if v' <= v (which is something which cannot even be expressed in Lean :-/ ). Right now we're working around this nonsense using the TypeMax hack :-/

[Scott Morrison]

No, Lean 4 is just unwilling to solve max u v =?= max u ?_ or max u v =?= max ?_ u. I have a patched version of Lean 4 (set your lean-toolchain to semorrison/lean4:release-20230620-max to try it out) that makes the most conservative possible change to allow this.

I've been meaning to write up an argument for adopting this change (see branch#forward_port_19153_hack, which works with this patch, and branch#forward_port_19153, which doesn't!) but haven't quite got there. :-)

[Kevin Buzzard]

Is it possible to check that your hack solves this problem?

[Scott Morrison]

Set your lean-toolchain to semorrison/lean4:release-20230620-max, and recompile (possibly via CI).

[Scott Morrison]

I tracked this down: there was a mysterious mis-port of a universe level in #3515 that then caused this problem. Fixing the underlying problem made this go away.

#5519 should be ready for review now.