Universe trouble when using ```Module.Injective```

Stream: maths

[Sophie Morel]

I've succesfully using projective modules before, but today was my first time tying to use injective modules in Lean4, and I immediately run into trouble with universes. Here is a MWE:

import Mathlib.Tactic
import Mathlib.Algebra.Module.Injective


universe u v w
variable (R : Type u) (M : Type v) (N : Type w) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

example [Module.Injective R M] (f : M →ₗ[R] N) : True := sorry

The error message (on the last line) says:

stuck at solving universe constraint
  max u ?u.2942 =?= v
while trying to unify
  TypeMax.{?u.2942, u} : Type ((max ?u.2942 u) + 1)
with
  Type v : Type (v + 1)

I've trying ULifting various objects but without success so far, and I'm also worried that this would cause trouble later.

[Sophie Morel]

For some reason, Module.Injective R M requires M to be TypeMax u v (R is type u, v is just other universe floating around). I'm sure there's very good reasons behind that decision even though I don't know what they were. I'm just not sure how to use the Module.Injective structure now. Is the only solution to re-introduce a new module that is explicitely TypeMax ? But then what will happen when I try to apply my new lemmas to an already existing module ?

[Sophie Morel]

Ah well, I wouldn't be able to use the new lemmas anyway because there does not seem to be Module.Injective instance on vector spaces, which is what I was hoping to use. So I'll do things another way. But if somebody know how to use Module.Injective, I would still be interested.

[Eric Wieser]

This works:

import Mathlib.Tactic
import Mathlib.Algebra.Module.Injective


universe u v w
variable (R : Type u) (M : TypeMax.{v,u}) (N : Type w) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

example [Module.Injective R M] (f : M →ₗ[R] N) : True := sorry

[Kevin Buzzard]

My instinct when universes start causing problems is to start assuming that some of them are equal. Lean has universes so whenever possible one should be as universe polymorphic as possible, but the moment mathematical issues start appearing there will be no mathematical harm in toning them down. Here the mathematical issue is that if the ring is in a bigger universe than the module then nonzero free modules for the ring don't live in the same universe as the module so a bunch of homological algebra gets messed up. In practice mathematicians don't see this phenomenon because of course the module is in the same universe as the ring in all cases in practice

[Sophie Morel]

Eric Wieser said:

This works:

import Mathlib.Tactic
import Mathlib.Algebra.Module.Injective


universe u v w
variable (R : Type u) (M : TypeMax.{v,u}) (N : Type w) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

example [Module.Injective R M] (f : M →ₗ[R] N) : True := sorry

Thanks !
Suppose that I sometimes want M to be injective and sometimes N, then I have to make sure that both of them are TypeMax.{v,u}. But if this shows up in the middle of a big complicated file (which is not theoretical but exactly what happened to me), then I need to go back to the start and change all my universe declarations. I'm a bit uncomfortable with that because who knows whether it will mess up something else.

I solved the problem by going back to basics: I wanted the modules to be injective/projective so some linear maps would have sections or retractions. So I just used the existence of the sections or retractions as hypotheses.

[Sophie Morel]

Kevin Buzzard said:

My instinct when universes start causing problems is to start assuming that some of them are equal. Lean has universes so whenever possible one should be as universe polymorphic as possible, but the moment mathematical issues start appearing there will be no mathematical harm in toning them down. Here the mathematical issue is that if the ring is in a bigger universe than the module then nonzero free modules for the ring don't live in the same universe as the module so a bunch of homological algebra gets messed up. In practice mathematicians don't see this phenomenon because of course the module is in the same universe as the ring in all cases in practice

Aha, thanks for explaining the universe convention in the definition. So there was a real mathematical problem !

I tend to tell Lean that everything is Type* (which as far as I understand creates as many different universes as there are declared objects), but here we see how that doesn't always work.

[Kevin Buzzard]

yeah, and when it doesn't work I just make an explicit universe u and start letting different things be in the same universe (because fighting with universes doesn't really appeal to me). The one drawback I've seen from my approach is that if you put all your rings and modules into Type u then when you want to use the reals or integers, either all the modules have to be in Type, or we persuade someone to make copies of the reals and the integers which live in Type u and still have all the usual bells and whistles which people expect from these types (e.g. that a whole bunch of tactics still work on them).

[Eric Wieser]

(we have those copies, they're ULift ℕ etc; but indeed various whistles are missing)

[Adam Topaz]

Does anyone understand why TypeMax is actually needed for this definition? Ping @Matthew Ballard who ported the file and @Jujian Zhang who wrote it originally.

[Adam Topaz]

Can't we just dualize the definition of projective modules replacing free modules with "cofree" modules?

[Kevin Buzzard]

Isn't the issue that if the universe of the module is smaller than the universe of the ring then there may well be no free modules at all other than the zero module (because the ring itself is too big for the module's universe). So the entire theory is basically totally messed up without this assumption.

[Adam Topaz]

But that doesn’t matter… if you can’t prove some module is injective then you can’t use the fact that it’s injective…

[Adam Topaz]

Take a look at docs#Module.Projective I’m just suggestion that we dualize that.

[Adam Topaz]

I.e define injectivity as “a direct summand of the cofree module generated by the underlying set of the module” or something like that

[Adam Topaz]

Does anyone know where we have the fact that a divisible abelian group is injective?

[Kevin Buzzard]

@Jujian Zhang you know your way around this part of the library very well :-)

[Joël Riou]

There are various candidates for a predicate Module.Injective with general universe parameters (e.g. the module become injective in the category ModuleCat.{max u v}), but in order to get all the equivalences and practical lemmas we want, we may need more general API developments about injective objects (in particular, a module is injective iff it satisfies a lifting property with respect to inclusions of ideals). Anyway, at least, mathlib shall soon know that ModuleCat has enough injectives #7392

[Junyan Xu]

Adam Topaz said:

Does anyone know where we have the fact that a divisible abelian group is injective?

docs#AddCommGroupCat.injective_of_divisible

[Junyan Xu]

I guess one option is to promote docs#Module.Baer to the official definition, as it quantifies ideals of the ring rather than all modules in a universe.