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!