mathlib3 documentation

algebra.monoid_algebra.no_zero_divisors

Variations on non-zero divisors in add_monoid_algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file studies the interaction between typeclass assumptions on two Types R and A and whether add_monoid_algebra 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.

We formalize in this file 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. Some of these assumptions can be trivially weakened: below we mention what assumptions are sufficient for the proofs in this file.

Main results #

The conditions on A imposed in no_zero_divisors.of_left_ordered are sometimes referred to as left-ordered. The conditions on A imposed in no_zero_divisors.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 add_monoid_algebra.mul_apply_add_eq_mul_of_forall_ne {R : Type u_1} {A : Type u_2} [semiring R] [has_add A] {f g : add_monoid_algebra R A} {a0 b0 : A} (h : {a b : A}, a f.support b g.support a a0 b b0 a + b 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.

theorem add_monoid_algebra.left.exists_add_of_mem_support_single_mul {R : Type u_1} {A : Type u_2} [semiring R] [add_left_cancel_semigroup A] {g : add_monoid_algebra R A} (a x : A) (hx : x (finsupp.single a 1 * g).support) :
(b : A) (H : b g.support), a + b = x
theorem add_monoid_algebra.right.exists_add_of_mem_support_single_mul {R : Type u_1} {A : Type u_2} [semiring R] [add_right_cancel_semigroup A] {f : add_monoid_algebra R A} (b x : A) (hx : x (f * finsupp.single b 1).support) :
(a : A) (H : a f.support), a + b = x

If R is a semiring with no non-trivial zero-divisors and A is a left-ordered add right cancel semigroup, then add_monoid_algebra R A also contains no non-zero zero-divisors.

If R is a semiring with no non-trivial zero-divisors and A is a right-ordered add left cancel semigroup, then add_monoid_algebra R A also contains no non-zero zero-divisors.