# Zulip Chat Archive

## Stream: new members

### Topic: Universe confusion

#### Jack J Garzella (Jul 19 2022 at 18:58):

Hello, I'm a relatively inexperienced Lean user, and I'm a bit confused about how one is supposed to handle universes when dealing with rings and modules. For example, I'm trying to assume the following statement: Let $M$ is an $R$-module and $\mathfrak{p}$ be a prime ideal, then $M_{\mathfrak{p}}$ is a free $R_{\mathfrak{p}}$-module. Here's the #mwe:

```
import algebra.module.localized_module
import ring_theory.localization.at_prime
import linear_algebra.free_module.basic
universes u v
variables (R : Type u) [comm_ring R]
variables (M : Type v) [add_comm_group M] [module R M]
variables (P : ideal R) [hp : P.is_prime]
#check localized_module P.prime_compl
variable (hm : @module.free
(localization.at_prime P) (localized_module P.prime_compl))
```

And here's the error Lean gives me:

```
type mismatch at application
module.free (localization.at_prime P) (localized_module P.prime_compl)
term
localized_module P.prime_compl
has type
Π (M : Type ?) [_inst_2 : add_comm_monoid M] [_inst_3 : module R M], Type (max u ?) : Type (max
(?+1)
?
((max u ?)+1))
but is expected to have type
Type ? : Type (?+1)
```

It seems like my universe `v`

has been replaced by a question mark in the error, but as far as I can tell it's mad that `localized_module`

has a universe which is the max of `u`

and `v`

(possibly adding one), rather than being in universe `v`

.

Does anyone know what's going on here? What is the best practice for dealing with such issues?

#### Reid Barton (Jul 19 2022 at 19:11):

Well first, `M`

should appear somewhere in `hm`

#### Reid Barton (Jul 19 2022 at 19:12):

You can read the error message as: `localized_module P.prime_compl`

was supposed to be a type, but actually it's a function that still needs another type (clearly `M`

) and some type classes and stuff, and then after providing that see whether things get better

#### Jack J Garzella (Jul 19 2022 at 19:34):

Ahh, whoops. That fixed it, thanks.

#### Jack J Garzella (Jul 19 2022 at 19:37):

Based on the documentation in localized_module.lean, I was expecting to put `localized_module M P.prime_compl`

instead of `localized_module P.prime_compl M`

. The same swap occurs in the localization.lean file for rings. Is there a reason these are flipped? If not, I can possibly make a quick docs PR?

#### Jack J Garzella (Jul 19 2022 at 19:37):

btw I'm looking at https://github.com/leanprover-community/mathlib/blob/master/src/algebra/module/localized_module.lean, line 20

#### Reid Barton (Jul 19 2022 at 19:51):

It looks like the comments are out of date (there are further occurrences with the arguments swapped in later comments in the file).

#### Junyan Xu (Jul 19 2022 at 20:56):

You can prove the same thing for any submonoid, not just prime_compl, right? The result will be strictly more general.

#### Jack J Garzella (Jul 20 2022 at 02:33):

You mean to say that $M$ free over $R$ implies $S^{-1}M$ is free over $S^{-1}R$ for any submonoid $S$? If so, yes, and it follows quickly from the fact that localization is a tensor product/base change. However, this isn't what I'm trying to prove--I'm going for (the algebraic version of) Hartshorne II.5.7, in which you don't know that $M$ is free over $R$.

#### Junyan Xu (Jul 20 2022 at 02:43):

Oh sorry, I misread your original question: you are assuming that M_p is free over R_p for all p, which is a weaker assumption than assuming it for all submonoids. Indeed, I erroneously thought you want to show that if M is free over R then M_p is free over R_p. However,

it follows quickly from the fact that localization is a tensor product/base change.

I think we don't have this yet in mathlib, but maybe it's in some open PR ...

Last updated: Dec 20 2023 at 11:08 UTC