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

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

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.

#6166

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