Universe confusion

Stream: new members

[Jack J Garzella]

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]

Well first, M should appear somewhere in hm

[Reid Barton]

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]

Ahh, whoops. That fixed it, thanks.

[Jack J Garzella]

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]

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

[Reid Barton]

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]

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

[Jack J Garzella]

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]

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 ...