quotient of a ring by the zero ideal

Stream: Is there code for X?

[Junyan Xu]

I'm surprised we don't have this; just want to make sure there isn't an easier way to construct it:

import Mathlib

def quotientBotEquiv {R} [CommRing R] : R ⧸ (⊥ : Ideal R) ≃+* R :=
  .trans (Ideal.quotEquivOfEq (RingHom.ker_coe_equiv <| .refl R).symm) <|
    RingHom.quotientKerEquivOfRightInverse (f := .id R) (g := id) fun _ ↦ rfl

[Eric Wieser]

Can we prove it more generally for [Semiring R] and ⊥ : RingCon R?

[Junyan Xu]

Presumably you can, but docs#Ideal.instHasQuotientIdealToSemiringToCommSemiring is defined in terms of Submodule.hasQuotient, so R ⧸ (⊥ : Ideal R) is not defeq to (⊥ : RingCon R).Quotient, but it is defeq to (Ideal.Quotient.ringCon ⊥ : RingCon R).Quotient.

[Antoine Chambert-Loir]

Junyan Xu said:

I'm surprised we don't have this; just want to make sure there isn't an easier way to construct it:

import Mathlib

def quotientBotEquiv {R} [CommRing R] : R ⧸ (⊥ : Ideal R) ≃+* R :=
  .trans (Ideal.quotEquivOfEq (RingHom.ker_coe_equiv <| .refl R).symm) <|
    RingHom.quotientKerEquivOfRightInverse (f := .id R) (g := id) fun _ ↦ rfl

It should be a bit easier in the other direction (that of Quotient.mk).