Refactor of `Localization`

Stream: mathlib4

[Kevin Buzzard]

I was looking for a project for a student and I was wondering if there was one in our set-up of localization. I'm trying to understand it. Currently there's a TODO in Algebra.Module.LocalizedModule saying "Redefine docs#Localization for monoids and rings to coincide with docs#LocalizedModule ". Is this still something which we want to do? Pinging @Jujian Zhang @Eric Wieser @Andrew Yang who I know have discussed this in the past.

[Jujian Zhang]

Perhaps a relevant Lean3 PR was: https://github.com/leanprover-community/mathlib3/pull/15584

But since ring localization was changed to Ore localization, I don’t know if the claim that ring localization and module localization could be made defer is still valid.

[Kevin Buzzard]

So is this the situation: docs#LocalizedModule is mathematically a special case of docs#OreLocalization. Apparently we wanted docs#Localization to be defeq to OreLocalization so the way to do that would be to redefine LocalizedModule to be some abbrev for OreLocalization.

[Kevin Buzzard]

import Mathlib

def LocalizedModule' {R : Type*} [CommSemiring R] (S : Submonoid R) (M : Type*) [AddCommMonoid M]
    [Module R M] := OreLocalization S M

example : @LocalizedModule = @LocalizedModule' := rfl -- no

[Kevin Buzzard]

Oh yikes,

import Mathlib

def LocalizedModule' {R : Type*} [CommSemiring R] (S : Submonoid R) (M : Type*) [AddCommMonoid M]
    [Module R M] := OreLocalization S M

example : @LocalizedModule = @LocalizedModule' := rfl -- no

variable {M : Type*} [CommMonoid M] (S : Submonoid M) in
example : Localization S = OreLocalization S M := rfl -- yes

-- yikes
variable {M : Type*} [CommMonoid M] (S : Submonoid M) in
example : Localization S = LocalizedModule' S M := rfl -- doesn't typecheck because M isn't a ring!

variable {A : Type*} [CommRing A] (S : Submonoid A) in
example : Localization S = LocalizedModule' S A := rfl -- works

docs#LocalizedModule is kind of stupid now. It's just OreLocalization but with redundant extra typeclass assumptions.

[Kevin Buzzard]

I should explain the reason I got interested in this question: I only discovered docs#LocalizedModule the other day. My PRs #16746 and #16650 (not ready for merging) were written when I needed that the localization of an R-algebra at an R-submonoid S was an R[1/S]-algebra, and we didn't have this so I tried to make it and I used Ore Localization because I thought that was what I was supposed to do, but it was silly because all my rings were commutative and I only needed a theory in the commutative case, so all my hypotheses in the theorems in those PRs have commutative rings in. And then I discovered LocalizedModule and thought "oh crap I could have just used that and then I probably wouldn't have got into that mess with smul" and then I saw the TODO and here we are.

[Kevin Buzzard]

All of this has come from me trying to understand Frobenius elements by the way!

[Christian Merten]

@Andrew Yang has been refactoring localizations with the goal to redefine docs#LocalizedModule in terms of docs#OreLocalization and the relevant PR is #13156. It seems to me that this PR contains (some of) the instances you are (were?) interested in?

[Kevin Buzzard]

import Mathlib

variable {M : Type*} [CommMonoid M] (S : Submonoid M) in
example : Localization S = M[S⁻¹] := rfl -- yes

variable {A : Type*} [CommRing A] (S : Submonoid A) in
example : Localization S = A[S⁻¹] := rfl -- works

variable {R : Type*} [CommSemiring R] (S : Submonoid R) (M : Type*) [AddCommMonoid M]
    [Module R M]

namespace OreLocalization

-- in #16650 but this is probably the right name
unseal OreLocalization.smul in
theorem oreDiv_smul_oreDiv_comm {R : Type*} [CommMonoid R] {S : Submonoid R} {A : Type*}
    [MulAction R A] {r : R} {a : A} {s₁ s₂ : S} :
    (r /ₒ s₁) • (a /ₒ s₂) = r • a /ₒ (s₂ * s₁) := rfl

-- this one works for OreSets in the non-comm case. Most of the rest doesn't.
def of : M →ₗ[R] M[S⁻¹] where
  toFun m :=  m /ₒ 1
  map_add' _m _n := add_oreDiv.symm
  map_smul' r m := (smul_oreDiv_one r m).symm

variable {S M} in
def smul_left (t : R[S⁻¹]) :
    M[S⁻¹] →ₗ[R] M[S⁻¹] where
toFun := (t • ·)
map_add' := smul_add t
map_smul' := smul_comm t

lemma smul_left_apply (t : R[S⁻¹]) (q : M[S⁻¹]) :
    smul_left t q = t • q := rfl

lemma smul_oreDiv' (r : R) (s : S) (m : M) : r • (m /ₒ s) = (r • m) /ₒ s := by
  rw [← oreDiv_one_smul r]
  simp only [oreDiv_smul_oreDiv]
  change r • m /ₒ (s * 1) = r • m /ₒ s
  simp only [mul_one]

noncomputable def ofLocalizedModule.toFun : LocalizedModule S M →ₗ[R] M[S⁻¹] :=
  LocalizedModule.lift _ (OreLocalization.of S M) <| by
  intro s
  refine ⟨⟨smul_left (s /ₒ 1), smul_left (1 /ₒ s),
      by
    ext
    simp [smul_left_apply, ← @smul_assoc], by
    ext
    simp [smul_left_apply, ← smul_assoc, smul_oreDiv']⟩,
      by
    ext r
    exact oreDiv_one_smul (↑s) r
  ⟩

noncomputable def ofLocalizedModule.invFun : M[S⁻¹] →ₗ[R] LocalizedModule S M :=
  -- oh yikes, is the universal property not there for OreLocalization?
  sorry

[Junyan Xu]

the localization of an R-algebra at an R-submonoid S was an R[1/S]-algebra

Note that there is docs#localizationAlgebra but there you localize at the image of S under the algebraMap.