# Variations on non-zero divisors in `AddMonoidAlgebra`s #

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.

source
theorem MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul {R : Type u_1} {A : Type u_2} [Semiring R] [Mul A] {f g : MonoidAlgebra R A} {a0 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.

source
instance MonoidAlgebra.instNoZeroDivisorsOfUniqueProds {R : Type u_1} {A : Type u_2} [Semiring R] [NoZeroDivisors R] [Mul A] [UniqueProds A] :
NoZeroDivisors (MonoidAlgebra R A)
source
instance MonoidAlgebra.instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R] [Mul A] [UniqueProds A] :
IsLeftCancelMulZero (MonoidAlgebra R A)
source
instance MonoidAlgebra.instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R] [Mul A] [UniqueProds A] :
IsRightCancelMulZero (MonoidAlgebra R A)
source
instance MonoidAlgebra.instIsCancelMulZeroOfIsCancelAddOfUniqueProds {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsCancelMulZero R] [Mul A] [UniqueProds A] :
IsCancelMulZero (MonoidAlgebra R A)
source
instance MonoidAlgebra.instIsDomainOfIsCancelAddOfUniqueProds {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsDomain R] [Monoid A] [UniqueProds A] :
IsDomain (MonoidAlgebra R A)
source
theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd {R : Type u_1} {A : Type u_2} [Semiring R] [Add A] {f g : AddMonoidAlgebra R A} {a0 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.

source
instance AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums {R : Type u_1} {A : Type u_2} [Semiring R] [NoZeroDivisors R] [Add A] [UniqueSums A] :
NoZeroDivisors (AddMonoidAlgebra R A)
source
instance AddMonoidAlgebra.instIsLeftCancelMulZeroOfIsCancelAddOfUniqueSums {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R] [Add A] [UniqueSums A] :
IsLeftCancelMulZero (AddMonoidAlgebra R A)
source
instance AddMonoidAlgebra.instIsRightCancelMulZeroOfIsCancelAddOfUniqueSums {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R] [Add A] [UniqueSums A] :
IsRightCancelMulZero (AddMonoidAlgebra R A)
source
instance AddMonoidAlgebra.instIsCancelMulZeroOfIsCancelAddOfUniqueSums {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsCancelMulZero R] [Add A] [UniqueSums A] :
IsCancelMulZero (AddMonoidAlgebra R A)
source
instance AddMonoidAlgebra.instIsDomainOfIsCancelAddOfUniqueSums {R : Type u_1} {A : Type u_2} [Semiring R] [IsCancelAdd R] [IsDomain R] [AddMonoid A] [UniqueSums A] :
IsDomain (AddMonoidAlgebra R A)