Zulip Chat Archive

Stream: new members

Topic: Ring iso induced by quotient


view this post on Zulip Riccardo Brasca (Feb 26 2021 at 18:47):

What is the best way of proving that if f : R ≃+* S is an isomorphism of rings and I : ideal R then I get an iso I.quotient ≃+* (map (f : R →+* S) I).quotient? As in the following

import ring_theory.ideal.operations

variables {R S : Type*} [comm_ring R] [comm_ring S]

open ideal

def quotient_equiv (I : ideal R) (f : R ≃+* S) :
  I.quotient ≃+* (map (f : R →+* S) I).quotient := sorry

The map in one direction if given immediately by quotient_map (map ↑f I) ↑f (@le_comap_map _ S _ _ _ _), but going in the other direction requires (I : ideal R) (f : R ≃+* S) : I.map (f : R →+* S) ≤ I.comap f.symm that, even if not difficult, is annoying. The fact that I am doing this by hand make me suspicious that I didn't understand the API correctly, in particular ideal.rel_iso_of_bijective seems relevant, but I don't know how to use it. Thank you!

view this post on Zulip Adam Topaz (Feb 26 2021 at 19:57):

Here's a proof I came up with that's WAY too long:

import ring_theory.ideal.operations

variables {R S : Type*} [comm_ring R] [comm_ring S]

open ideal

lemma helper (I : ideal R) (f : R ≃+* S) :
  (I.map (f : R →+* S) : set S) = f '' I :=
begin
  ext,
  split,
  { intros hx,
    apply submodule.span_induction hx,
    { tauto },
    { refine 0, I.zero_mem, by simp },
    { rintros x y x,hx,rfl y,hy,rfl⟩,
      refine x+y,I.add_mem hx hy, by simp },
    { rintros a x x,hx,rfl⟩,
      refine f.symm a * x,_,_⟩,
      refine I.mul_mem_left _ hx,
      simp } },
  { rintros y,hy,rfl⟩,
    exact mem_map_of_mem hy }
end

def quotient_equiv (I : ideal R) (f : R ≃+* S) :
  I.quotient ≃+* (map (f : R →+* S) I).quotient :=
let J := map (f : R →+* S) I,
    π : R →+* I.quotient := ideal.quotient.mk _,
    π' : S →+* J.quotient := ideal.quotient.mk _
in
ring_equiv.of_hom_inv
(ideal.quotient.lift _ (π'.comp f.to_ring_hom)
begin
  intros a ha,
  erw quotient.eq_zero_iff_mem,
  exact mem_map_of_mem ha
end) (ideal.quotient.lift _ (π.comp f.symm.to_ring_hom)
begin
  intros s hs,
  erw quotient.eq_zero_iff_mem,
  change _  (_ : set _) at hs,
  rw helper at hs,
  rcases hs with r,hr,rfl⟩,
  change ((f.symm  f) r)  _,
  simpa,
end)
begin
  ext,
  rcases quotient.mk_surjective x with x,rfl⟩,
  tidy,
end
begin
  ext,
  rcases quotient.mk_surjective x with x,rfl⟩,
  tidy,
end

view this post on Zulip Riccardo Brasca (Feb 26 2021 at 20:04):

It is surprisingly annoying, isn't it? If this is not my fault no problem, I will prove the relevant lemmas to improve the API. For example I am a little surprised that ext doesn't work for ideals...

view this post on Zulip Adam Topaz (Feb 26 2021 at 20:04):

It looks like there should certainly be some more api around this map function.

view this post on Zulip Riccardo Brasca (Feb 26 2021 at 20:05):

For example your helper should be an immediate consequence of ideal.mem_image_of_mem_map_of_surjective

view this post on Zulip Adam Topaz (Feb 26 2021 at 20:07):

Oh yeah, I didn't know about that lemma.

view this post on Zulip Riccardo Brasca (Feb 26 2021 at 20:08):

Ah sure, because you wrote (I.map (f : R →+* S) : set S), but I mean, this should be true without going to set S

view this post on Zulip Riccardo Brasca (Mar 01 2021 at 18:20):

#6492 if someone is interested


Last updated: May 16 2021 at 05:21 UTC