!4#4949 Algebra.Category.Module.FilteredColimits

Stream: mathlib4

[Riccardo Brasca]

!4#4949 has a universes related error et the end that I am not sure I understand... maybe someone used to universes can have a look.

The Module instance also needs to be fixed, but I didn't try very hard.

[Ruben Van de Velde]

All the universe errors I've hit after were the result of errors or sorries earlier on the file, so I'd try dealing with those first

[Scott Morrison]

Yeah, although filtered colimits in the category of modules (in which for some reason the ring and module are allowed to live in different universes) are ripe for universe problems. :-)

[Ruben Van de Velde]

That's why I've mostly avoided category theory, but still worth looking at the earlier issues first :)

[Riccardo Brasca]

I've fixed all the problems up to colimitCoconeIsColimit, where universes show up. Now I really need help :)

[Riccardo Brasca]

The error is

stuck at solving universe constraint
  max (v+1) (?u.60462+1) =?= max (u+1) (v+1)
while trying to unify
  (ModuleCat R ⥤ TypeMax) (ModuleCat R) (moduleCategory R) (ModuleCat R ⥤ TypeMax) (ModuleCat R ⥤ TypeMax)
with
  ModuleCat R ⥤ Type (max u v)

that doesn't look very good. Maybe I made some mistake earlier in the file.

[Ruben Van de Velde]

Do you need to introduce some TypeMax?

[Riccardo Brasca]

I really don't know. At the moment I just copied what is in the mathlib3 version

[Ruben Van de Velde]

My understanding is that (some?) Type. {max u v} need to become TypeMax, which is new relative to lean 3

[Riccardo Brasca]

Well, I prefer to not write this by myself since I don't really understand it, so I will leave the PR help-wanted.

[Scott Morrison]

I'm having a look now.

[Scott Morrison]

I really wish Lean would just go ahead and solve stuck at solving universe constraint max (v+1) (?u.60659+1) =?= max (u+1) (v+1) with ?u = u.

[Kevin Buzzard]

Lean 3 would unify universe questions like this, but Lean 4 refuses to. The solution ?u.60462=u is not unique if u<=v, but because Lean has no infrastructure for saying u<=v it's sad that it won't just solve this anyway. The other one that comes up up is max u ? = u which has the solution ?=u which Lean 4 won't assume despite it being the right one essentially always.

[Scott Morrison]

Fixed the first error, but now pausing to watch battle bots with kids. :-)

[Scott Morrison]

@Riccardo Brasca, I fixed the rest of the file. I took the opportunity of reordering some jumbled universe variables in ConcreteCategory.

[Scott Morrison]

One of the errors was very confusing, and resolved by changing fun F => to fun {F} =>. The error looked to be all about universes, but this was misleading.

[Riccardo Brasca]

Thanks!!