localization take 2

Stream: maths

[Kenny Lau]

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

[Kenny Lau]

is this useful?

[Kenny Lau]

we can localization any commutative monoid on a submonoid

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

oh I wasn't aware

[Kevin Buzzard]

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.