Localization preservers injective maps

Stream: maths

[Nikolas Kuhn]

Am I wrong that this lemma docs#map_injective_of_injective should hold without the assumption hM? This is in the context of rings, I'm not sure whether there are some subtleties in general.

/-- Injectivity of a map descends to the map induced on localizations. -/
lemma map_injective_of_injective
  (hg : function.injective g) [is_localization (M.map g : submonoid P) Q]
  (hM : (M.map g : submonoid P) ≤ non_zero_divisors P) :
  function.injective (map Q g M.le_comap_map : S → Q) :=
begin
  rintros x y hxy,
  obtain ⟨a, b, rfl⟩ := mk'_surjective M x,
  obtain ⟨c, d, rfl⟩ := mk'_surjective M y,
  rw [map_mk' _ a b, map_mk' _ c d, mk'_eq_iff_eq] at hxy,
  refine mk'_eq_iff_eq.2 (congr_arg (algebra_map _ _) (hg _)),
  convert is_localization.injective _ hM hxy; simp,
end

[Kevin Buzzard]

Can you prove it without hM? If so then you don't need to ask :-)

[Kevin Buzzard]

docs#map_injective_of_injective

[Kevin Buzzard]

You don't give the types of the things you're talking about and there seem to be several functions with this name so I don't know what the mathematical question you're asking is yet.

[Damiano Testa]

docs#is_localization.map_injective_of_injective?

[Kevin Buzzard]

That looks like it!

[Nikolas Kuhn]

Whoops, my bad! Yes, that's the right one.

[Nikolas Kuhn]

More precisely, I think this should be a special case of localization (for modules over rings) being exact, which doesn't need the additional assumptions.

[Kevin Buzzard]

So, if I've got it right, the maths question is: if $M$ is a multiplicative subset of the commutative ring $R$ and if $g:R\to P$ is an injective morphism of commutative rings, then is the induced map $R[1/M]\to P[1/g(M)]$ also injective?

[Kevin Buzzard]

Yeah this looks true to me. Try to prove it in Lean!

[Kevin Buzzard]

If $g(r/m)=g(r'/m')$ then $g(r)/g(m)=g(r')/g(m')$ so there's some $m''$ with $(g(r)g(m')-g(r')g(m))g(m'')=0$ but this means $g(rm'm''-r'mm'')=0$ so $rm'm''-r'mm''=0$ so $r/m=r'/m'$.

[Nikolas Kuhn]

It's less of a math question than whether I'm understanding that this is what the Lemma is trying to say... (maybe the math channel isn't the best one to ask). But I'll see whether I can do the Lean proof!

[Andrew Yang]

If there is some zero divisor in $g(M)$, wouldn't $P[1/g(M)]$ become the trivial ring?

[Kevin Buzzard]

right, it's that line of argument which makes you think that the assumption should be there and this is why I was initially hesitent. But if you have a zero divisor then localising it at doesn't give you the zero ring, it just kills components where the thing you're inverting is zero. For example localising Z/2 x Z/3 at the zero divisor (0,1) just gives you the ring Z/3.

[Kevin Buzzard]

The universal example would be something like $R=\Z[X]$, $M=\langle X\rangle$, $P=\Z[X,Y]/(XY)$. So if the map is still injective in this case then this is evidence things are OK. And localising $\Z[X,Y]/(XY)$ at $X$ doesn't give you the zero ring, it just kills $Y$ and then inverts $X$.

[Nikolas Kuhn]

Here's a proof. Golfs are welcome!

import ring_theory.localization.basic

lemma map_injective_of_injective' {R P S : Type*} {Q : Type*} [comm_ring R] [comm_ring P]
  [comm_ring S] [comm_ring Q] [algebra R S] {M : submonoid R} [is_localization M S] {g : R →+* P}
  [algebra P Q] (hg : function.injective g) [is_localization (M.map g : submonoid P) Q] :
  function.injective (is_localization.map Q g M.le_comap_map : S → Q) :=
begin
  rintros x y hxy,
  rw ←sub_eq_zero at ⊢  hxy,
  rw ← map_sub at hxy,
  set z := x-y,
  obtain ⟨a, b, hz⟩ := is_localization.mk'_surjective M z,
  rw [← hz, is_localization.map_mk', is_localization.mk'_eq_zero_iff] at hxy,
  cases hxy with m hm,
  obtain ⟨m', hm'⟩ := m,
  rw submonoid.mem_map at hm',
  obtain ⟨n, hn, hnm⟩ :=hm',
  rw [subtype.coe_mk, ← hnm, ring_hom.coe_monoid_hom, ← map_mul, ← map_zero g] at hm,
  replace hm := hg hm,
  rw [←hz, is_localization.mk'_eq_zero_iff],
  use ⟨n,hn⟩,
  rw subtype.coe_mk,
  exact hm,
end

[Kevin Buzzard]

You should make a PR to mathlib! This I'm sure would be a welcome contribution. Do you have a github account and have you done this before?

[Nikolas Kuhn]

I haven't done a PR myself before, but I'm going to give it a try!

[Kevin Buzzard]

You'll need to post your github account name here, and ask the maintainers for push access to non-master branches. You'll also need to fix any code you break with the change (which hopefully won't be much, but github will tell you what you broke when it tries to recompile mathlib after the change).

[Nikolas Kuhn]

I've worked on a PR before, so I should have the rights.

[Nikolas Kuhn]

Here it is : #15184

[Nikolas Kuhn]

This has been merged. Thanks to Eric Wieser and Kyle Miller for their reviews and contribution!