Ring iso induced by quotient

Stream: new members

[Riccardo Brasca]

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!

[Adam Topaz]

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

[Riccardo Brasca]

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...

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

#6492 if someone is interested