Basis.localizationLocalizedModule

Stream: Is there code for X?

[Xavier Roblot]

I need to prove that a $\mathbb{Z}$-basis of an integral ideal of a number field is also a $\mathbb{Q}$-basis of the number field. For the case of the ring of integers, this is done using docs#Basis.localizationLocalization but it does not work in this case since it needs a CommRing. I wrote a proof that uses the fact that $\mathbb{Q}$ is the fraction field of $\mathbb{Z}$ and that any element of the field multiplied by a large enough integers lies in the ideal. However, it feels this should fit into a larger setting. I believe the following construction (with probably some adjustment to the hypothesis) would work in my case and would be a worthy addition to Mathlib.

import Mathlib.Algebra.Module.LocalizedModule

variable {ι R : Type*} [CommRing R] (M : Submonoid R) (S : Type*) [CommSemiring S] [Algebra R S]
  [IsLocalization M S] (A : Type*) [AddCommMonoid A] [Module R A] (b : Basis ι R A)

instance : Module S (LocalizedModule M A) := sorry

def Basis.localizationLocalizedModule (b : Basis ι R A) : Basis ι S (LocalizedModule M A) := sorry

theorem Basis.localizedModule_apply (i : ι) :
    b.localizationLocalizedModule M S A i = LocalizedModule.mkLinearMap M A (b i) := sorry

However, I want to make sure we don't have that in another and that it is the right way to go before working on the proof.

[Andrew Yang]

I think IsLocalizedModule should be used instead.

[Xavier Roblot]

Andrew Yang said:

I think IsLocalizedModule should be used instead.

Well, that would have been the next step after I complete the first version :sweat_smile:

[Xavier Roblot]

The file Mathlib.Algebra.Module.LocalizedModule uses Localization at many places rather than IsLocalization. Is it worth first refactoring the file to use IsLocalization instead or should I just duplicate the results?

[Xavier Roblot]

And this file should probably introduce IsLocalizedModule first with all the proper instances and then LocalizedModule as it is done for Localization. I do not mind doing the changes but I want to make sure it is the right thing to do first...

[Andrew Yang]

We should use IsLocalization instead. We should still keep the instances though, since typeclass inference cannot figure them out in general.