When the fraction ring is a field

Stream: maths

[Snir Broshi]

What can we say about a ring R whose fraction ring is a field?
The other direction is known: If R is an integral domain, then its fraction ring is a field:

import Mathlib

variable {R : Type*} [CommRing R] [IsDomain R]
variable {K : Type*} [CommRing K]
variable [Algebra R K] [IsFractionRing R K]

noncomputable def field_k : Field K := IsFractionRing.toField R

But if we know that the fraction ring is a field, is it true that R must be an integral domain?

import Mathlib

variable {R : Type*} [CommRing R]
variable {K : Type*} [Field K]
variable [Algebra R K] [IsFractionRing R K]

instance : IsDomain R := sorry

If not, what if I add [IsIntegrallyClosed R] as a hypothesis?
Or can we say something weaker on R maybe?
Basically, what does the property "the ring of fractions is a field" imply?

[Yakov Pechersky]

import Mathlib

variable (R : Type*) [CommRing R]

lemma IsFractionRing.subsingleton_of (S : Type*) [Subsingleton R] [CommRing S] [Algebra R S]
    [hf : IsFractionRing R S] :
    Subsingleton S := by
  apply IsLocalization.subsingleton (M := nonZeroDivisors R)
  simp only [mem_nonZeroDivisors_iff, zero_mul, forall_const, mul_zero, and_self]
  intro
  exact Subsingleton.elim _ _

-- can't be an instance because `K` can't be inferred
lemma IsFractionRing.isDomain_left (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K] :
    IsDomain R := by
  rw [isDomain_iff_noZeroDivisors_and_nontrivial R, noZeroDivisors_iff_left_eq_zero_of_mul]
  constructor
  · intro x hx y hy
    rw [← (IsFractionRing.injective R K).eq_iff] at hy
    simpa [hx] using hy
  · have : Nontrivial K := inferInstance
    rw [← not_subsingleton_iff_nontrivial] at this ⊢
    contrapose! this
    exact IsFractionRing.subsingleton_of R K

[Kenny Lau]

import Mathlib

-- can't be an instance because `R` can't be inferred
lemma Subsingleton.of_algebra (R : Type*) [CommSemiring R] [Subsingleton R]
    (S : Type*) [Semiring S] [Algebra R S] :
    Subsingleton S :=
  (algebraMap R S).codomain_trivial

-- can't be an instance because `K` can't be inferred
lemma IsFractionRing.isDomain_left (R : Type*) [CommRing R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K] :
    IsDomain R :=
  (FaithfulSMul.algebraMap_injective _ K).isDomain _

[Yakov Pechersky]

Even better.