Basic Lemma on Localization

Stream: Is there code for X?

[Xavier Xarles]

I think this is not in mathlib4 and could be useful. Also, if someone can help me to simplify the proof...

import Mathlib.GroupTheory.MonoidLocalization

variable {M : Type*} [CommMonoid M] {S : Submonoid M}
    {N : Type*} [CommMonoid N]

theorem  Submonoid.LocalizationMap.map_units₂ (f : Submonoid.LocalizationMap S N)
    (y : M) (hy: ∃ r, r * y ∈ S) : IsUnit (f.toMap y) := by
  let ⟨r, hr⟩ := hy
  have : IsUnit (f.toMap (r * y)) := by
        have : ∃ a : S, ↑a = r * y := CanLift.prf (r * y) hr
        let ⟨a, ha⟩ := this
        rw [←ha]
        exact f.map_units a
  rw [MonoidHom.map_mul (f.toMap) r y] at this
  exact isUnit_of_mul_isUnit_right this

[Ruben Van de Velde]

A little:

import Mathlib.GroupTheory.MonoidLocalization

variable {M : Type*} [CommMonoid M] {S : Submonoid M}
    {N : Type*} [CommMonoid N]

theorem  Submonoid.LocalizationMap.map_units₂ (f : Submonoid.LocalizationMap S N) (y : M) (hy: ∃ r, r * y ∈ S) :
    IsUnit (f.toMap y) := by
  let ⟨r, hr⟩ := hy
  have := f.map_units ⟨_, hr⟩
  rw [MonoidHom.map_mul] at this
  exact isUnit_of_mul_isUnit_right this

[Xavier Xarles]

I really don't understand how to get an element a : S from and element b : M such that b ∈ S.

[Ruben Van de Velde]

That's ⟨_, hr⟩

[Ruben Van de Velde]

S treated as a type is "just" a subtype, which is a pair of an element and a proof that the element is in S

[Xavier Xarles]

And how can extract what I call hr without a letor obtain? I am sure this can be written more succinctly

[Ruben Van de Velde]

You could do have := f.map_units ⟨_, hy.choose_spec⟩ but I would keep the let. Maybe you could take another look at the places you use this lemma, though, and see if there's a better way to phrase it

[Junyan Xu]

Note it's generally preferable to split (hy: ∃ r, r * y ∈ S) into two arguments r and hry : r * y ∈ S

[Xavier Xarles]

I am not sure what you mean. In the theorem, who is r is irrelevant (only its existence matters).

[Junyan Xu]

That's true but it's easier to supply arguments like r hry than ⟨r, hry⟩, so splitting makes the theorem easier to use. So don't be surprised if reviewers ask you to split it when you PR it.

[Junyan Xu]

But if your condition is something hy : y ∈ S.saturation then there's no point splitting it.
(where y ∈ S.saturation is defeq to ∃ r, r * y ∈ S)

[Xavier Xarles]

Yes, that was what I was thinking on doing.