# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: First isomorphism theorem for rings

#### Riccardo Brasca (Feb 10 2021 at 19:50):

I am not finding the first isomorphism theorem for rings... is it somewhere? I am asking because I would be surprised if it weren't there, but in that case I can prove it without problems.

#### Adam Topaz (Feb 10 2021 at 19:54):

For rings or commutative rings?

#### Riccardo Brasca (Feb 10 2021 at 19:54):

Sorry, commutative rings

#### Adam Topaz (Feb 10 2021 at 19:54):

I think it should be there for `comm_rings`

.

#### Riccardo Brasca (Feb 10 2021 at 19:57):

I am not finding it in `ring_theory/ideal/basic`

nor in `ring_theory/ideal/operations`

. If you think it can be somewhere else I can look for it

#### Adam Topaz (Feb 10 2021 at 19:57):

We have this: docs#ideal.quotient.mkₐ_ker

#### Riccardo Brasca (Feb 10 2021 at 19:58):

I wrote it :grinning: But that is the point, I want a generic surjective map, not the natural map to the quotient

#### Adam Topaz (Feb 10 2021 at 19:58):

Oh.

#### Adam Topaz (Feb 10 2021 at 19:58):

Well, it should be easy enough to patch together what's already there, but yeah I don't see the precise statement.

#### Riccardo Brasca (Feb 10 2021 at 20:00):

Sure, I will do it

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

Hmm.... looks like we don't have the lemma that modding out by the kernel gives an injective morphism.

#### Riccardo Brasca (Feb 10 2021 at 20:12):

We have `ring_hom.lift_of_surjective`

, so it should be OK

#### Adam Topaz (Feb 10 2021 at 20:14):

Here's the quick sketch I came up with:

```
import ring_theory.ideal.operations
variables {A B : Type*} [comm_ring A] [comm_ring B] (f : A →+* B)
noncomputable def foo (cond : function.surjective f) : f.ker.quotient ≃+* B :=
ring_equiv.of_bijective (ideal.quotient.lift f.ker f $ λ x hx, f.mem_ker.mp hx) $
{ left := begin
rw ring_hom.injective_iff,
intros a ha,
rcases ideal.quotient.mk_surjective a with ⟨b,rfl⟩,
simp only [ideal.quotient.lift_mk] at ha,
rw ← ring_hom.mem_ker at ha,
rwa ideal.quotient.eq_zero_iff_mem,
end,
right := begin
intros x,
rcases cond x with ⟨y,rfl⟩,
refine ⟨ideal.quotient.mk _ y, rfl⟩,
end }
```

#### Adam Topaz (Feb 10 2021 at 20:15):

The first proof there is injectivity, and I think it should probably be a separate lemma, analogous to docs#quotient_group.ker_lift_injective

#### Riccardo Brasca (Feb 10 2021 at 20:17):

Ah yes, following what is done for groups is probably the best idea

#### Adam Topaz (Feb 10 2021 at 20:19):

This `mk_surjective`

name seems to conflict with things like docs#quotient.exists_rep

#### Mario Carneiro (Feb 10 2021 at 20:21):

remark: the name `surjective`

should be in the lemma iff the lemma statement actually uses `function.surjective`

#### Mario Carneiro (Feb 10 2021 at 20:21):

not sure if that addresses Adam Topaz's point

#### Adam Topaz (Feb 10 2021 at 20:21):

Yeah, it does.

#### Adam Topaz (Feb 10 2021 at 20:22):

But since I'm used to `quotient.exists_rep`

, I tried using `ideal.quotient.exists_rep`

which doesn't exist, and had to go searching for something else.

#### Mario Carneiro (Feb 10 2021 at 20:23):

That might be useful as a lemma as well, but the lemma name is more about how the theorem is concretely presented and not so much about what it abstractly means

#### Riccardo Brasca (Feb 10 2021 at 20:24):

@Adam Topaz Are you doing it? If not don't worry, I can do it... if yes it would also be useful (to me...) to have the version for algebras.

#### Adam Topaz (Feb 10 2021 at 20:27):

@Riccardo Brasca please go ahead, I don't have much time for cleaning up this code and/or any PR today.

#### Adam Topaz (Feb 10 2021 at 20:27):

Feel free to use the code above if you want.

#### Adam Topaz (Feb 10 2021 at 20:55):

Here's a version of this in the noncommutative case.

```
import algebra.ring_quot
variables {A B : Type*} [ring A] [ring B] (f : A →+* B)
noncomputable def foo (cond : function.surjective f) :
ring_quot (λ (a b : A), f (a - b) = 0) ≃+* B :=
ring_equiv.of_bijective (ring_quot.lift ⟨f, λ a b h, eq_of_sub_eq_zero $ by {rwa ← f.map_sub}⟩)
{ left := begin
intros x y,
rcases ring_quot.mk_ring_hom_surjective _ x with ⟨x,rfl⟩,
rcases ring_quot.mk_ring_hom_surjective _ y with ⟨y,rfl⟩,
intro h,
simp only [ring_quot.lift_mk_ring_hom_apply] at h,
replace h := sub_eq_zero_of_eq h,
rw ← f.map_sub at h,
dsimp only [ring_quot.mk_ring_hom],
exact quot.sound (ring_quot.rel.of h)
end,
right := begin
intros x,
rcases cond x with ⟨a,rfl⟩,
exact ⟨ring_quot.mk_ring_hom _ a, by simp⟩,
end }
```

#### Adam Topaz (Feb 10 2021 at 20:56):

But for this it probably makes sense to wait until we have two-sided ideals.

#### Riccardo Brasca (Feb 10 2021 at 23:32):

#### Riccardo Brasca (Feb 10 2021 at 23:46):

Working with algebras I noticed that if `f : A →ₐ[R] B`

then we cannot write `f.ker`

, but we have to use `f.to_ring_hom.ker`

. I do not see any reason to avoid `f.ker`

for algebra morphisms, defined as `f.to_ring_hom.ker`

: if everybody agrees I can do this modification.

#### Eric Wieser (Feb 11 2021 at 00:08):

If you add `alg_hom.ker`

, then you will probably also need to either:

- Add a simp lemma converting
`x.ker`

to`x.to_ring_hom.ker`

- Copy across every single lemma about
`ring_hom.ker`

to`alg_hom`

(thankfully the proofs can just be`:= the_ring_hom_lemma`

)

#### Riccardo Brasca (Feb 11 2021 at 00:21):

Mmh, you're right, rewriting all the lemmas is a little annoying... especially since a quick `grep`

gives just three occurrences for `to_ring_hom.ker`

(and probably all written by myself...)

#### Riccardo Brasca (Feb 11 2021 at 00:25):

This is part of my secret plan to remove `comm_ring`

from mathlib and to get it replaced by `algebra`

:smiling_devil:

#### Riccardo Brasca (Feb 11 2021 at 00:26):

Just joking of course, even if I really think one should try to work with algebras rather than rings if possible, but this is just my algebraic geometry oriented opinion.

#### Julian Külshammer (Feb 11 2021 at 06:48):

`algebra`

or `comm_algebra`

?

Last updated: May 19 2021 at 00:40 UTC