First isomorphism theorem for rings

Stream: Is there code for X?

[Riccardo Brasca]

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]

For rings or commutative rings?

[Riccardo Brasca]

Sorry, commutative rings

[Adam Topaz]

I think it should be there for comm_rings.

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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

[Adam Topaz]

Oh.

[Adam Topaz]

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

[Riccardo Brasca]

Sure, I will do it

[Adam Topaz]

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

[Riccardo Brasca]

We have ring_hom.lift_of_surjective, so it should be OK

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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

[Mario Carneiro]

remark: the name surjective should be in the lemma iff the lemma statement actually uses function.surjective

[Mario Carneiro]

not sure if that addresses Adam Topaz's point

[Adam Topaz]

Yeah, it does.

[Adam Topaz]

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]

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]

@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]

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

[Adam Topaz]

Feel free to use the code above if you want.

[Adam Topaz]

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]

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

[Riccardo Brasca]

#6166

[Riccardo Brasca]

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]

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]

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]

This is part of my secret plan to remove comm_ring from mathlib and to get it replaced by algebra :smiling_devil:

[Riccardo Brasca]

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]

algebra or comm_algebra?