Zulip Chat Archive

Stream: maths

Topic: localization take 2


view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 25 2019 at 06:37):

is this useful?

view this post on Zulip Kenny Lau (Oct 25 2019 at 06:37):

we can localization any commutative monoid on a submonoid

view this post on Zulip Johan Commelin (Oct 25 2019 at 06:51):

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

view this post on Zulip Johan Commelin (Oct 25 2019 at 06:51):

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

view this post on Zulip Kenny Lau (Oct 25 2019 at 06:53):

oh I wasn't aware

view this post on Zulip 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