Issue: nonZeroDivisors, regular elements, and localization

Stream: mathlib4

[Junyan Xu]

I opened issue #22997 and am now copying the content here for discussion.

Non-zero-divisors

We currently have the following defeqs:

import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
variable (M : Type*) [MonoidWithZero M]
example : nonZeroDivisorsLeft M = nonZeroDivisors M := rfl
example : nonZeroDivisorsRight M = nonZeroSMulDivisors M M := rfl

Notice also that nonZeroDivisorsLeft coincides with non-left zero divisors according to Wikipedia, while nonZeroDivisorsRight coincides with non-right zero divisors. My suggestions are:

• Switch the names nonZeroDivisorsLeft and nonZeroDivisorsRight (possibly rename to nonLeft/RightZeroDivisors)

• Make nonZeroDivisors an abbreviation of nonZeroDivisorsLeft

• (?) Define nonZeroDivisorsLeft using nonZeroSMulDivisors

Regular elements

• Define the submonoids leftRegulars, rightRegulars and smulRegulars in terms of IsLeftRegular, IsRightRegular and IsSMulRegular (and additivize)

• Show that they agree with non(SMul)ZeroDivisorsLeft/Right in a ring (≤holds in general)

• Redefine Is(Left,Right)CancelMul and IsCancelSMul in terms of Is(Left,Right)Regular and IsSMulRegular

Localization (of commutative monoids/semirings)

• Replace nonZeroDivisors by regulars in localization API, especially in IsFractionRing, FractionRing, and IsLocalizedModule.rank_eq: IsLocalization.injective continue to hold, and it's also true that the localization map f in IsLocalizedModule is injective iff the submonoid S is contained in smulRegulars R M.

[Damiano Testa]

I often find the left/right naming conventions confusing.

[Damiano Testa]

In this case, my initial instinct would be to define a "left zero-divisor" with the same convention that your Wikipedia link uses: a is a lzd if there is some non-zero x such that ax = 0.

[Damiano Testa]

So, assuming I did not get confused again about left and right, I am happy with your proposed changes!

[Junyan Xu]

I started fixing the left/right at #27224

[Eric Wieser]

I'll note that #25887 might be tangentially related

[Junyan Xu]

Yeah, maybe I should add analogues of isLeftRegular_op etc. for nonZeroDivisors ...

[Junyan Xu]

#27791 redefines Is(Left/Right)CancelMul(Zero) in terms of Is(Left/Right)Regular. I requested a review from @Damiano Testa who added IsRegular into mathlib.

#27877 connects IsRegular/IsCancelMul to nonZeroDivisors/NoZeroDivisors, which is also a part of this issue.

#27842 and #27862 clean up some Localization API in preparation for materials about the Grothendieck group of a monoid, previously discussed at #maths > Linear independence over semirings @ 💬 and #Is there code for X? > ℕ is Noetherian ℕ-module but ℕ × ℕ is not @ 💬.

[Junyan Xu]

I found some to_additive mistranslations at https://loogle.lean-lang.org/?q=%22IsAddCancel%22 and https://loogle.lean-lang.org/?q=%22isaddleftcancel%22 due to the first six lines of fixAbbreviation. I'm fixing this in #27940.

[Junyan Xu]

Thanks for the reviews! I think I addressed all review comments on #27877.
Note that #27842 isn't blocked by any other PR, and it reduces the number of lines, but #27862 does depend on these two PRs.

My latest PR is #27936 which additivizes Dvd and Prime; it will be used to generalize #27886 to MonoidAlgebras. Because the structure Units is used to define IsUnit, the defeq breaks and I have to introduce the following lemmas; I wonder whether there's a way to auto-generate them.

section Monoid

variable [Monoid M] {x : M} {y : Additive M}

lemma isAddUnit_ofMul_iff : IsAddUnit (Additive.ofMul x) ↔ IsUnit x := by
  rw [isAddUnit_iff_exists, isUnit_iff_exists]; rfl

lemma isUnit_toMul_iff : IsUnit y.toMul ↔ IsAddUnit y := isAddUnit_ofMul_iff.symm

lemma addIrreducible_ofMul_iff : AddIrreducible (Additive.ofMul x) ↔ Irreducible x := by
  simp_rw [addIrreducible_iff, isAddUnit_ofMul_iff, ← isUnit_toMul_iff, irreducible_iff]; rfl

lemma irreducible_toMul_iff : Irreducible y.toMul ↔ AddIrreducible y :=
  addIrreducible_ofMul_iff.symm

end Monoid

section AddMonoid

variable [AddMonoid M] {x : M} {y : Multiplicative M}

lemma isUnit_ofAdd_iff : IsUnit (Multiplicative.ofAdd x) ↔ IsAddUnit x := isUnit_toMul_iff

lemma isAddUnit_toAdd_iff : IsAddUnit y.toAdd ↔ IsUnit y := isAddUnit_ofMul_iff

lemma irreducible_ofAdd_iff : Irreducible (Multiplicative.ofAdd x) ↔ AddIrreducible x :=
  irreducible_toMul_iff

lemma addIrreducible_toAdd_iff : AddIrreducible y.toAdd ↔ Irreducible y := addIrreducible_ofMul_iff

end AddMonoid

[Junyan Xu]

There are also a lot of mistranslation of dvd to addDvd in decl names in #27936 which are currently manually fixed. Could we prevent to_additive from replacing "dvd" by "addDvd" if the type of the additivized decl doesn't mention AddDvd.dvd?

[Ruben Van de Velde]

Some simplified proofs:

import Mathlib

section Monoid

variable [Monoid M] {x : M} {y : Additive M}

lemma isAddUnit_ofMul_iff : IsAddUnit (Additive.ofMul x) ↔ IsUnit x := by
  simp [isAddUnit_iff_exists, isUnit_iff_exists, ← ofMul_mul]

lemma isUnit_toMul_iff : IsUnit y.toMul ↔ IsAddUnit y := isAddUnit_ofMul_iff.symm

lemma addIrreducible_ofMul_iff : AddIrreducible (Additive.ofMul x) ↔ Irreducible x := by
  simp [addIrreducible_iff, ← isUnit_toMul_iff, irreducible_iff, ← ofMul_mul]