## Stream: maths

### Topic: localization take 2

#### Kenny Lau (Oct 25 2019 at 06:37):

import group_theory.submonoid

universes u

variables (α : Type u) [comm_monoid α] (s : set α) [is_submonoid s]

namespace localization

instance : setoid (α × s) :=
{ r := λ x y : α × s, ∃ t : s, t.1 * x.1 * y.2.1 = t.1 * y.1 * x.2.1,
iseqv := ⟨λ x, ⟨1, rfl⟩, λ x y ⟨t, ht⟩, ⟨t, ht.symm⟩,
λ x y z ⟨t, ht⟩ ⟨u, hu⟩, ⟨t * u * y.2, calc
t.1 * u.1 * y.2.1 * x.1 * z.2.1
= u.1 * (t.1 * x.1 * y.2.1) * z.2.1 : by ac_refl
... = u.1 * (t.1 * y.1 * x.2.1) * z.2.1 : by rw ht
... = t.1 * (u.1 * y.1 * z.2.1) * x.2.1 : by ac_refl
... = t.1 * (u.1 * z.1 * y.2.1) * x.2.1 : by rw hu
... = t.1 * u.1 * y.2.1 * z.1 * x.2.1 : by ac_refl⟩⟩ }

end localization

def localization : Type u :=
quotient \$ localization.setoid α s


is this useful?

#### Kenny Lau (Oct 25 2019 at 06:37):

we can localization any commutative monoid on a submonoid

#### Johan Commelin (Oct 25 2019 at 06:51):

You should be aware that there is a massive refactor in the making by @Amelia Livingston

#### Johan Commelin (Oct 25 2019 at 06:51):

It would be best to talk to here, before diving into this

#### Kenny Lau (Oct 25 2019 at 06:53):

oh I wasn't aware

#### Kevin Buzzard (Oct 25 2019 at 07:23):

is this useful?

Yes, because it means that given a valuation from an ID into a monoid, you can extend to a valuation on the field of fractions (perhaps to a bigger monoid), and this comes up in the perfectoid project. That's why Amelia is working on it.

Last updated: May 06 2021 at 18:20 UTC