Zero ring morphism implies trivial codomain

Stream: Is there code for X?

[Artie Khovanov]

theorem RingHom.subsingleton_of_ker_eq_top {R S : Type*} [Semiring R] [Semiring S]
    {f : R →+* S} (hf : RingHom.ker f = ⊤) : Subsingleton S := by
  have : f 1 = 0 := by
    rw [← RingHom.mem_ker]
    simp [hf]
  simpa [← subsingleton_iff_zero_eq_one] using this.symm

I couldn't find anything in the library.

[Damiano Testa]

This is an equivalence, right? The other direction exists, I think.

[Damiano Testa]

Now that I am at a computer, this works:

import Mathlib.RingTheory.Ideal.Maps

theorem RingHom.ker_eq_top_iff_subsingleton {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) :
    RingHom.ker f = ⊤ ↔ Subsingleton S := by
  simp only [Ideal.eq_top_iff_one, mem_ker, map_one, eq_comm, ← subsingleton_iff_zero_eq_one]

[Artie Khovanov]

Damiano Testa said:

This is an equivalence, right? The other direction exists, I think.

Yeah the other direction is already a theorem in the library

[Artie Khovanov]

Damiano Testa said:

Now that I am at a computer, this works:

import Mathlib.RingTheory.Ideal.Maps

theorem RingHom.ker_eq_top_iff_subsingleton {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) :
    RingHom.ker f = ⊤ ↔ Subsingleton S := by
  simp only [Ideal.eq_top_iff_one, mem_ker, map_one, eq_comm, ← subsingleton_iff_zero_eq_one]

Thanks, will (eventually) PR