Variations on non-zero divisors in AddMonoidAlgebras

This file studies the interaction between typeclass assumptions on two Types R and A and whether R[A] has non-zero zero-divisors. For some background on related questions, see Kaplansky's Conjectures, especially the zero divisor conjecture.

Conjecture. Let K be a field, and G a torsion-free group. The group ring K[G] does not contain nontrivial zero divisors, that is, it is a domain.

In this file we show that if R satisfies NoZeroDivisors and A is a grading type satisfying UniqueProds A (resp. UniqueSums A), then MonoidAlgebra R A (resp. R[A]) also satisfies NoZeroDivisors.

Because of the instances to UniqueProds/Sums, we obtain a formalization of the well-known result that if R is a field and A is a left-ordered group, then R[A] contains no non-zero zero-divisors. The actual assumptions on R are weaker.

Main results

• MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul and AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd general sufficient results stating that certain monomials in a product have as coefficient a product of coefficients of the factors.
• The instance showing that Semiring R, NoZeroDivisors R, Mul A, UniqueProds A imply NoZeroDivisors (MonoidAlgebra R A).
• The instance showing that Semiring R, NoZeroDivisors R, Add A, UniqueSums A imply NoZeroDivisors R[A].

TODO: move the rest of the docs to UniqueProds? NoZeroDivisors.of_left_ordered shows that if R is a semiring with no non-zero zero-divisors, A is a linearly ordered, add right cancel semigroup with strictly monotone left addition, then R[A] has no non-zero zero-divisors.

• NoZeroDivisors.of_right_ordered shows that if R is a semiring with no non-zero zero-divisors, A is a linearly ordered, add left cancel semigroup with strictly monotone right addition, then R[A] has no non-zero zero-divisors.

The conditions on A imposed in NoZeroDivisors.of_left_ordered are sometimes referred to as left-ordered. The conditions on A imposed in NoZeroDivisors.of_right_ordered are sometimes referred to as right-ordered.

These conditions are sufficient, but not necessary. As mentioned above, Kaplansky's Conjecture asserts that A being torsion-free may be enough.

theorem MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul {R : Type u_1} {A : Type u_2} [Semiring R] [Mul A] {f : MonoidAlgebra R A} {g : MonoidAlgebra R A} {a0 : A} {b0 : A} (h : UniqueMul f.support g.support a0 b0) : (f * g) (a0 * b0) = f a0 * g b0

The coefficient of a monomial in a product f * g that can be reached in at most one way as a product of monomials in the supports of f and g is a product.

instance MonoidAlgebra.instNoZeroDivisorsOfUniqueProds {R : Type u_1} {A : Type u_2} [Semiring R] [NoZeroDivisors R] [Mul A] [UniqueProds A] : NoZeroDivisors (MonoidAlgebra R A)

Equations

• (_ : NoZeroDivisors (MonoidAlgebra R A)) = (_ : NoZeroDivisors (MonoidAlgebra R A))

theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd {R : Type u_1} {A : Type u_2} [Semiring R] [Add A] {f : AddMonoidAlgebra R A} {g : AddMonoidAlgebra R A} {a0 : A} {b0 : A} (h : UniqueAdd f.support g.support a0 b0) : (f * g) (a0 + b0) = f a0 * g b0

The coefficient of a monomial in a product f * g that can be reached in at most one way as a product of monomials in the supports of f and g is a product.

instance AddMonoidAlgebra.instNoZeroDivisorsAddMonoidAlgebraHasMulToZeroToMulZeroClassNonUnitalNonAssocSemiring {R : Type u_1} {A : Type u_2} [Semiring R] [NoZeroDivisors R] [Add A] [UniqueSums A] : NoZeroDivisors (AddMonoidAlgebra R A)

Equations

• (_ : NoZeroDivisors (AddMonoidAlgebra R A)) = (_ : NoZeroDivisors (MonoidAlgebra R (Multiplicative A)))