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 MM is an RR-module and p\mathfrak{p} be a prime ideal, then MpM_{\mathfrak{p}} is a free RpR_{\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)
  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
        ((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 MM free over RR implies S1MS^{-1}M is free over S1RS^{-1}R for any submonoid SS? 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 MM is free over RR.

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