Localization.Away API

Stream: mathlib4

[Kenny Lau]

what is the canonical way to express $\dfrac{a}{b^3}$ as an element of Localization.Away b?

import Mathlib

variable {R : Type*} [CommRing R] (a b : R)

-- a/b^3
example : Localization.Away b := sorry

[Yury G. Kudryashov]

My guess: (a * .invSelf b : Localization.Away b)

[Kenny Lau]

invSelf is literally never used

[Kenny Lau]

I believe we should have a new constructor for Localization.Away

[Yury G. Kudryashov]

WDYT about introducing Localization.Away.self (x : M) : Units (Localization.Away x) with val := .mk x 1 _ and inv := invSelf x?

[Yury G. Kudryashov]

Then you can write (a : Away b) /_p Away.self b.

[Kenny Lau]

import Mathlib

namespace Localization.Away

nonrec def mk {M : Type*} [CommMonoid M] {b : M} (n : ℕ) (a : M) : Away b :=
  .mk a ⟨b ^ n, n, rfl⟩

def mkₗ {R : Type*} [CommRing R] {b : R} (n : ℕ) : R →ₗ[R] Away b where
  toFun := mk n
  map_add' := by simp [mk, add_mk_self]
  map_smul' := by simp [mk, smul_mk]

end Localization.Away

-- a/b^3
example {R : Type*} [CommRing R] {a b : R} : Localization.Away b := .mkₗ 3 a

[Kenny Lau]

I think the advantage of this is that you get a bundled map

[Andrew Yang]

Probably just Islocalization.mk'or IsLocalization.Away.invSelf. Please do not add any API to Localization.Away and add it instead for IsLocalization.Away.

[Kenny Lau]

if you use IsLocalization, then you start by assuming a ring, so the minimally bundled mk would be the linear one above