Local properties of modules

Stream: mathlib4

[Yongle Hu]

Hi! I am trying to define local properties of modules analogous to the local properties of rings (such as OfLocalizationMaximal). However, I am encountering the problem that for an R-module M, after localizing M at a prime ideal 𝔭 of R, the universe of Mₚ differs from the universe of M. As a result, in order to state this property, I am only able to express it by lifting the universe of M to match the universe of Mₚ.

import Mathlib.Algebra.Module.LocalizedModule
import Mathlib.RingTheory.Localization.AtPrime

universe u v

variable (P : ∀ (R : Type u) [CommRing R] (M : Type max u v) [AddCommGroup M] [Module R M], Prop)
def OfLocalizedModuleMaximal : Prop :=
  ∀ {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M],
    (∀ (J : Ideal R) (_ : J.IsMaximal), P (Localization.AtPrime J) (LocalizedModule J.primeCompl M)) →
    P R (ULift.{u} M)

But this makes the definition difficult to use. Is there any way to resolve this problem?

Thanks!

[Andrew Yang]

An option is to change M : Type v to M : Type max u v but this might cause problems later on.

[Andrew Yang]

Another is to take two properties P and Q such that Q R M <-> P R (ULift M) for all M.

[Andrew Yang]

Or just stick with ULift. Do you have examples on how bad this is?

[Yongle Hu]

For example, if I have proven that flatness is a local property according to this definition, then when I use it, I still need to manually find theorems Module.Flat.of_linearEquiv and ULift.moduleEquiv, and then combine these theorems to derive the conclusion.

import Mathlib

universe u v

variable (P : ∀ (R : Type u) (M : Type max u v) [CommRing R] [AddCommGroup M] [Module R M], Prop)

def OfLocalizedModuleMaximal : Prop :=
  ∀ {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M],
    (∀ (J : Ideal R) (_ : J.IsMaximal), P (Localization.AtPrime J) (LocalizedModule J.primeCompl M)) →
    P R (ULift.{u} M)

theorem flat_of_localization : OfLocalizedModuleMaximal @Module.Flat := sorry

example {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (h : ∀ (J : Ideal R) (_ : J.IsMaximal), Module.Flat (Localization.AtPrime J) (LocalizedModule J.primeCompl M)) : Module.Flat R M :=
  haveI := flat_of_localization M h
  Module.Flat.of_linearEquiv R (ULift.{u} M) M ULift.moduleEquiv.symm

[Andrew Yang]

Yes you will need to restate the statement anyways.
The OfLocalizedModuleMaximal defs are there to deal with meta-properties of properties of modules and not to be applied directly. If you aren't planning on the former then I'd argue you can drop OfLocalizedModuleMaximal altogether.

[Yongle Hu]

OK, I see. Thank you!

[Kevin Buzzard]

Of course another option is just to make the ring and module live in the same universe, but this hack should only be used if the ulift tricks become painful.