nonZeroDivisors, regular elements, and localization

Zulip: #mathlib4 > Issue: nonZeroDivisors, regular elements, and localization

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) : #27224

• Redefine nonZeroDivisors the infimum of nonZeroDivisorsLeft and nonZeroDivisorsRight for symmetry with IsRegular) : #27224

Regular elements

• Define the submonoids leftRegulars, rightRegulars, regulars and smulRegulars in terms of IsLeftRegular, IsRightRegular, IsRegular and IsSMulRegular (and additivize). Show they are contained in nonZeroDivisorsLeft/Right etc. respectively (assuming only MulZeroClass).

• Show that they agree with non(SMul)ZeroDivisorsLeft/Right in a ring (≤holds in general): done for unbundled Is(Left/Right)Regular in #27791

• Redefine Is(Left,Right)CancelMul, Is(Left,Right)CancelMulZero in terms of Is(Left,Right)Regular and IsSMulRegular : #27791

• (?) Use IsSMulRegular in the definition of IsCancelSMul (133 → 151 imports)

• In a (non-unital non-associative) ring, IsLeftCancelMulZero, IsRightCancelMulZero, IsCancelMulZero and NoZeroDivisors are all equivalent (note that IsDomain = Nontrivial + IsCancelMulZero) : #27791

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.

MvPolynomial

MonomialOrder.degree_mul_of_isRegular_left / MvPolynomial.totalDegree_mul_of_isDomain should only require nonZeroDivisors / NoZeroDivisors.

Start with Mathlib/Algebra/Regular/Basic, Mathlib/Algebra/Regular/SMul, and Mathlib/Algebra/GroupWithZero/NonZeroDivisors to review the regular-element definitions. Then inspect the localization APIs in Mathlib/RingTheory/Localization/FractionRing, Mathlib/Algebra/Module/LocalizedModule/Basic, and Mathlib/LinearAlgebra/Dimension/Localization. Done means addressing the unchecked regular-submonoid, localization, and IsCancelSMul items while preserving the stated injectivity and MvPolynomial requirements.