Aₚ ≃ₗ[Aₚ] Aₚ (Localization vs LocalizedModule)

Stream: Is there code for X?

[Jz Pan]

Suppose p is a prime ideal of A, do we have LocalizedModule p.primeCompl A ≃ₗ[Localization p.primeCompl] Localization p.primeCompl? i.e. Aₚ ≃ₗ[Aₚ] Aₚ but the first Aₚ is LocalizedModule while the second is Localization.

It could be constructed by LocalizedModule.equivTensorProduct p.primeCompl A ≪≫ₗ TensorProduct.AlgebraTensorModule.rid _ _ _. But it's better if it is in mathlib and has more properties.

For example, I need Aₚ / pAₚ ≃ₗ[Aₚ] Aₚ / pAₚ where the first pAₚ is Submodule.localized p.primeCompl p while the second is IsLocalRing.maximalIdeal (Localization p.primeCompl) (or something else equal to this). To do this I need to use the above isomorphism together with docs#Submodule.Quotient.equiv. Then I need to check some trivial but tedious things.

This is happen in https://github.com/acmepjz/lean-iwasawa/blob/dca0cd3a332776e7b2aa232764b26d3cc4426d6a/Iwasawalib/RingTheory/CharacteristicIdeal/Basic.lean#L399 and subsequent lines.

Does anyone have better solution for this?

[Andrew Yang]

I really wanted to make the two defeq but I gave up. If you need to you could try to redo #13156 (or I could try again if I have some time).

[Jz Pan]

From the current design they cannot be defeq since Localization is more general (it works for non-rings?).

I think maybe one solution is add an IsLocalizedModule property to Localization, then one can use docs#IsLocalizedModule.mapEquiv to construct this Aₚ-linear isomorphism (docs#IsLocalizedModule.iso and docs#IsLocalizedModule.linearEquiv are similar but they are only A-linear).

[Andrew Yang]

The current Localization (or docs#OreLocalization) allows you to localize a set with a monoid acting on it and both localization of rings and modules are a specific instance of this.

[Andrew Yang]

But currently the right way might be

import Mathlib

noncomputable section

variable {A : Type} [CommRing A] (S : Submonoid A)

example : LocalizedModule S A ≃ₗ[Localization S] Localization S :=
  IsLocalizedModule.linearEquiv S (LocalizedModule.mkLinearMap S A) (Algebra.linearMap A _)
    |>.extendScalarsOfIsLocalization S _

[Jz Pan]

Or maybe one can use this

noncomputable example {A : Type*} [CommRing A] (S : Submonoid A) :
    LocalizedModule S A ≃ₗ[Localization S] Localization S :=
  IsLocalizedModule.mapEquiv S (LocalizedModule.mkLinearMap S A) (Algebra.linearMap A _)
    (Localization S) (LinearEquiv.refl A A)

Does it have better apply lemmas?

[Jz Pan]

Give up. Seems that my original approach has slightly shorter code.