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.

source
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.

source
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
source
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
source
theorem add_monoid_algebra.no_zero_divisors.of_left_ordered {R : Type u_1} {A : Type u_2} [semiring R] [no_zero_divisors R] [add_right_cancel_semigroup A] [linear_order A] [covariant_class A A has_add.add has_lt.lt] :
no_zero_divisors (add_monoid_algebra R A)

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.

source
theorem add_monoid_algebra.no_zero_divisors.of_right_ordered {R : Type u_1} {A : Type u_2} [semiring R] [no_zero_divisors R] [add_left_cancel_semigroup A] [linear_order A] [covariant_class A A (function.swap has_add.add) has_lt.lt] :
no_zero_divisors (add_monoid_algebra R A)

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.