Localization at units

Stream: Is there code for X?

[Justus Springer]

I would like to have an isomorphism between a ring $R$ and its localization at one $R_1$. More generally, the localization of a ring $R$ at a submonoid consisting only of units, should be isomorphic to $R$, because the identity is a localization map. Is there something approximating that in the library?

[Johan Commelin]

You should be able to create a localization_map between R and R, that exhibits the identity map as a localization at {1}.

[Kevin Buzzard]

@Justus Springer the lowdown on localisation is that given R and S there is "the explicit localisation R[1/S]" in Lean (i.e. a model for the localisation) and there is also "the predicate that an R-algebra A is isomorphic to R[1/S]". So you can get what you want by first proving that the R-algebra R satisfies the predicate for S={1}, and then using the fact that everything which satisfies the predicate is isomorphic to the explicit localisation, if that is what your question is. If you formalised the question in Lean rather than just making a mathematical statement, it would be easier to see what you were after.

[Kevin Buzzard]

PS if it's not in the library already that R satisfies the localisation predicate for S=1 or more generally $S\subseteq R^\times$ then it probably should be!

[Justus Springer]

Yeah that's exactly what I meant. Just wanted to make sure I'm not missing something obvious before I spend too much time working on the general problem. It's not in the library as far as I can see.

[Justus Springer]

Here's a toy version I got to work:

import ring_theory.localization
import algebra.category.CommRing.basic

noncomputable theory

variables (R : Type*) [comm_ring R] (M : submonoid R) (hM : ∀ x ∈ M, is_unit x)
include hM

def localization_at_units_iso : localization M ≃+* R :=
localization.ring_equiv_of_quotient $
begin
  apply (𝟙 (CommRing.of R) : _ →+* _).to_localization_map (λ y, hM _ y.2),
  { intro y, refine ⟨⟨y, 1⟩, by simp⟩,},
  { intros x y,
    simp,
    refine ⟨λ h, ⟨1, by simp [h]⟩, (λ h, _)⟩,
    rcases h with ⟨c, hc⟩,
    rcases is_unit_iff_exists_inv.mp (hM _ c.2) with ⟨b, hb⟩,
    simp at hb,
    convert congr_arg (λ z, z * b) hc ;
    simp [mul_assoc, hb], }
end

[Kevin Buzzard]

import ring_theory.localization

variables (R : Type*) [comm_ring R] (M : submonoid R)

noncomputable def localization_at_units_iso (hM : ∀ x ∈ M, is_unit x) : localization M ≃+* R :=
localization.ring_equiv_of_quotient
{ map_units' := λ y, hM y.1 y.2,
  surj' := λ z, ⟨⟨z, 1⟩, mul_one z⟩,
  eq_iff_exists' := λ x y, ⟨λ h, ⟨1, by simpa using h⟩,
    λ ⟨⟨c, hc⟩, h⟩, (is_unit.mul_left_inj (hM c hc)).mp h⟩,
  ..ring_hom.id R }

[Kevin Buzzard]

It's just the same proof, but I never need to go into tactic mode (or use category theory)

[Justus Springer]

Thanks!

[Justus Springer]

Let's see if I can put something together here.

[Justus Springer]

This doesn't actually need the additive structure of rings, so it might as well go into group_theory/monoid_localization I assume...

[Patrick Massot]

Why do we assume M is a submonoid here?

[Justus Springer]

Localization is defined only at submonoids isn't it?
If I can divide by f and by g I can also divide by fg.

[Patrick Massot]

I can see it is defined only at submonoids in Lean, but it isn't in the real world.

[Patrick Massot]

Of course localizing at a random subset will be the same thing as localizing at the submonoid generated by this subset.

[Patrick Massot]

But for formalization purposes I'm surprised we imposed that useless assumption.

[Patrick Massot]

If you define a localization by the obvious universal property then the submonoid condition is completely useless.

[Justus Springer]

I'm not sure. I guess the map $M\times R\to R_M$ sending $(r,s)$ to $r/s$ wouldn't be surjective if $M$ wasn't a submonoid?

[Justus Springer]

And this surjectivity is one of the defining properties of localization maps, as it's defined in Lean.

[Justus Springer]

It's not defined by the universal property I think.

[Adam Topaz]

Maybe we need to change the definition of localization_map?

[Kevin Buzzard]

This was done by Kenny in 2017 as one of the very first projects that either he or I had been involved in, that's why we localise at submonoids -- we were copying out of Atiyah--Macdonald and had no idea about Lean; indeed this project taught us a lot about it.

[Johan Commelin]

I think localization_map should be refactored to be a predicate on ring homomorphisms, or maybe a mixin on top of algebra. But this is quite a massive refactor, and I haven't found time or energy to do it.

[Johan Commelin]

Currently we need to resort to some ugly hacks to make the codomain of a localization_map into an algebra.

[Johan Commelin]

Also f.to_map isn't very nice to read.

[Adam Topaz]

I acctually really like @David Wärn 's definition of is_free_group. We could do something like this:

import algebra

universes u

class localization_map {A B : Type u} [semiring A] [semiring B] (f : A →+* B) (S : set A) :=
(maps_to_unit (s) : s ∈ S → is_unit (f s))
(lift : ∀ {C : Type u} [semiring C] (g : A →+* C), (∀ (s), s ∈ S → is_unit (g s)) → (B →+* C))
(lift_comp {C : Type u} [semiring C] (g : A →+* C) (cond : ∀ (s), s ∈ S → is_unit (g s)) :
  (lift g cond).comp f = g )
(lift_unique {C : Type u} [semiring C] (g : A →+* C) (cond : ∀ (s), s ∈ S → is_unit (g s))
  (h : B →+* C) : h.comp f = g → h = lift g cond)

[Patrick Massot]

Justus Springer said:

I'm not sure. I guess the map $M\times R\to R_M$ sending $(r,s)$ to $r/s$ wouldn't be surjective if $M$ wasn't a submonoid?

Of course you can't use this formula. You need to replace $M$ by the generated submonoid.

[Patrick Massot]

This allow you do to thing like localizing at $\{f\}$ without introducing a special case notation for instance.

[Adam Topaz]

(queue the complaints about semirings in 3...2...1...)

[Johan Commelin]

We'll want eliminators for other universes as well, I guess.

[Adam Topaz]

Yeah I'm not sure what to do about universes...

[Johan Commelin]

And maybe a constructor for the current defn

[Adam Topaz]

Do we ever want a localization of a (semi)ring which is not in the same universe?

[Adam Topaz]

Every time you "construct" a localization, it ends up in the same universe

[Johan Commelin]

I can think of various ways of ending up with "$\mathbb{Q}$" in arbitrary universes.

[Johan Commelin]

If you have the rational functions on some proper variety or something.

[Adam Topaz]

Like the prime subfield of a field K : Type LARGE?

[Johan Commelin]

I guess the solution is to have is_function_field_of X rat and is_prime_subfield_of K rat, etc...

[Adam Topaz]

Yeah good point, in this case we would want that the canonical map int \to K is a localization to the prime subfield

[Johan Commelin]

Damiano was also toying with the idea of having prelocalization_maps. So that int -> real was an example. Half of the theory works for that notion.

[Adam Topaz]

Okay, here's a fix:

import algebra

universes u v

class localization_map {A : Type u} {B : Type v} [semiring A] [semiring B]
  (f : A →+* B) (S : set A) :=
(maps_to_unit (s) : s ∈ S → is_unit (f s))
(unique_lift : ∀ {C : Type (max u v)} [semiring C] (g : A →+* C)
  (cond : ∀ (s), s ∈ S → is_unit (g s)), ∃! (h : B →+* C), h.comp f = g)

[Adam Topaz]

Or perhaps we need C : Type v?

[Johan Commelin]

The easiest would be to have a defn that doesn't mention universes...

[Patrick Massot]

I don't understand, I thought Kevin was always saying Neil's predicate did exactly that.

[Adam Topaz]

Yeah, we could just use Neil's predicate with the submonoid generated by the set (in the commutative ring case!)

[Adam Topaz]

But that's okay because all semirings are commutative rings