# 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} [] [Mul A] {f : } {g : } {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} [] [] [Mul A] [] :
Equations
• =
theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd {R : Type u_1} {A : Type u_2} [] [Add A] {f : } {g : } {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.instNoZeroDivisorsOfUniqueSums {R : Type u_1} {A : Type u_2} [] [] [Add A] [] :
Equations
• =