Zulip Chat Archive

Stream: Is there code for X?

Topic: First isomorphism theorem for rings


view this post on Zulip 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.

view this post on Zulip Adam Topaz (Feb 10 2021 at 19:54):

For rings or commutative rings?

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 19:54):

Sorry, commutative rings

view this post on Zulip Adam Topaz (Feb 10 2021 at 19:54):

I think it should be there for comm_rings.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 10 2021 at 19:57):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 10 2021 at 19:58):

Oh.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 20:00):

Sure, I will do it

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 20:12):

We have ring_hom.lift_of_surjective, so it should be OK

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 20:17):

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

view this post on Zulip Adam Topaz (Feb 10 2021 at 20:19):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:21):

not sure if that addresses Adam Topaz's point

view this post on Zulip Adam Topaz (Feb 10 2021 at 20:21):

Yeah, it does.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Feb 10 2021 at 20:27):

Feel free to use the code above if you want.

view this post on Zulip 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 }

view this post on Zulip Adam Topaz (Feb 10 2021 at 20:56):

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

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 23:32):

#6166

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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...)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Julian Külshammer (Feb 11 2021 at 06:48):

algebra or comm_algebra?


Last updated: May 19 2021 at 00:40 UTC