IsCancelMulZero and NoZeroDivisors for semirings

Stream: maths

[Bolton Bailey]

When R is a ring, IsCancelMulZero R is equivalent toNoZeroDivisors R (isCancelMulZero_iff_noZeroDivisors). But when R is only a semiring, NoZeroDivisors R is implied by IsCancelMulZero R
(although I guess this is not typeclass inferrable, see docs#IsLeftCancelMulZero.to_noZeroDivisors).

But I'm not aware of a proof that IsCancelMulZero R is implied by NoZeroDivisors R when R is just a semiring, or a counterexample that shows this is not true in general - does anyone know of a proof either way?

[Aaron Liu]

here's a counterexample:
Ring with three elements $0, 1, 2$, addition is $\min(a+b,2)$ and multiplication is $\min(ab,2)$, this is a semiring with no zero divisors but does not have cancellative multiplication by nonzero elements.

[Junyan Xu]

Here's an example with cancellative addition: ℕ × ℕ with componentwise addition, and multiplication defined by (a,b)(c,d)=(ac+bd,ad+bc). You can think of this as a subsemiring of ℤ[X]⧸⟨X²-1⟩. ac+bd=ad+bc=0 only has solutions with a=b=0 or c=d=0 in ℕ, so this semiring has no zero divisors, but (1,1)(1,0)=(1,1)(0,1)=(1,1).

[Bolton Bailey]

Junyan Xu said:

ac+bd=ad+bc=0 has only the solution a=b=c=d=0 in ℕ

Surely it has the solution a=1, b=c=d=0?

[Aaron Liu]

well of course that doesn't give you anything

[Aaron Liu]

surely instead what we wanted is ac+bd=ad+bc=0 has only the two classes of solutions a=b=0 and c=d=0 in ℕ

[Junyan Xu]

Thanks, corrected. The easiest way to prove this is by noticing (a+b)(c+d)=(ac+bd)+(ad+bc).