## Stream: new members

### Topic: Ring iso induced by quotient

#### 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!

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


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

#### Adam Topaz (Feb 26 2021 at 20:04):

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

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

#### Adam Topaz (Feb 26 2021 at 20:07):

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

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

#### Riccardo Brasca (Mar 01 2021 at 18:20):

#6492 if someone is interested

Last updated: May 16 2021 at 05:21 UTC