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