# Zulip Chat Archive

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