NoZeroDivisors iff IsDomain or Subsingleton

Stream: Is there code for X?

[Xavier Xarles]

I need this elementary lemma (I have a proof, but surely too long).

import Mathlib.Algebra.Ring.Basic

lemma NoZeroDivisors_iff_IsDomain_or_Subsingleton (L : Type*) [Ring L]:
    NoZeroDivisors L ↔ (IsDomain L ∨ Subsingleton L) := by sorry

[Eric Rodriguez]

lemma NoZeroDivisors_iff_IsDomain_or_Subsingleton (L : Type*) [Ring L]: NoZeroDivisors L ↔ (IsDomain L ∨ Subsingleton L) := by
  refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ sorry)⟩
  rw [or_iff_not_imp_right, not_subsingleton_iff_nontrivial]
  exact fun _ ↦ t.to_isDomain

where the sorry is that Subsingleton rings are NZDs, I couldn't seem to find that quickly oddly

[Xavier Xarles]

That was the same place I was stuck. Of course one can prove it, but it seems it should be more elementary...

[Eric Rodriguez]

doesn't seem to exist oddly

[Antoine Chambert-Loir]

Can be golfed, but everything is more or less there

import Mathlib.Tactic
import Mathlib.Algebra.Ring.Defs
import Mathlib.Algebra.GroupWithZero.Defs

lemma NoZeroDivisors_iff_IsDomain_or_Subsingleton (L : Type*) [Ring L]:
    NoZeroDivisors L ↔ (IsDomain L ∨ Subsingleton L) := by
  constructor
  · intro nzd
    by_cases nt : Nontrivial L
    · left
      exact IsDomain.mk
    · simp only [not_nontrivial_iff_subsingleton] at nt
      exact Or.inr nt
  · intro h
    cases' h with isd ss
    · exact IsDomain.to_noZeroDivisors L
    · apply NoZeroDivisors.mk
      intro a _ _
      left
      exact Subsingleton.eq_zero a

[Antoine Chambert-Loir]

lemma NoZeroDivisors_iff_IsDomain_or_Subsingleton (L : Type*) [Ring L]: NoZeroDivisors L ↔ (IsDomain L ∨ Subsingleton L) := by
  refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ NoZeroDivisors.mk (fun _ => Or.inl (Subsingleton.eq_zero _)))⟩
  rw [or_iff_not_imp_right, not_subsingleton_iff_nontrivial]
  exact fun _ ↦ t.to_isDomain

[Eric Wieser]

This lemma might help:

lemma isDomain_iff_noZeroDivisors_and_nontrivial (L : Type*) [Ring L]:
    IsDomain L ↔ (NoZeroDivisors L ∧ Nontrivial L) :=
  ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => {}⟩

[Antoine Chambert-Loir]

What seems to be missing is the instance that a trivial ring has no zero divisors

instance (L : Type*) [Ring L] [Subsingleton L] : NoZeroDivisors L :=
  NoZeroDivisors.mk (fun _ => Or.inl (Subsingleton.eq_zero _))

[Antoine Chambert-Loir]

Funnily, trying to apply lazily your lemma led me to

example (L : Type*) [Ring L]:
    NoZeroDivisors L ↔ (IsDomain L ∨ Subsingleton L) := by
    classical
    rw [isDomain_iff_noZeroDivisors_and_nontrivial, ← not_nontrivial_iff_subsingleton]
    generalize NoZeroDivisors L = p
    generalize Nontrivial L = q
    sorry -- p ↔ (p ∧ q) ∨ ¬q  does not hold

[Eric Wieser]

That instance looks like a performance issue to me, but maybe I'm wrong

[Eric Wieser]

It should certainly be a lemma if nothing else

[Antoine Chambert-Loir]

There's probably very little chance that this lemma has to be found automatically by the TypeClass inference system.

[Xavier Xarles]

Do you think it is a good idea to do a PR with some of these?

[Xavier Xarles]

Done #9407
But there is a problem with the cache.

[Yaël Dillies]

For the cache, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work

[Antoine Chambert-Loir]

While we're at it, it would probably be a good thing to give the proofs for all properties of rings (modules, spaces…) which are introduced in mathlib when they hold for the trivial ring (module, space…).

[Yaël Dillies]

Not necessarily, since that would create diamonds. NoZeroDivisors is alright because it's Prop-valued.

[Antoine Chambert-Loir]

(For example, docs#isNoetherian_of_subsingleton exists, but not isArtinian_of_subsingleton, nor the fact that the zero module is noetherian…)

[Antoine Chambert-Loir]

Not necessarily as instances. Just the theorems when they hold.

[Junyan Xu]

We already have docs#isArtinian_of_finite though