mathlib3 documentation

mathlib-counterexamples / zero_divisors_in_add_monoid_algebras

Examples of 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 contains an easy source of zero-divisors in an add_monoid_algebra. If k is a field and G is an additive group containing a non-zero torsion element, then add_monoid_algebra k G contains non-zero zero-divisors: this is lemma zero_divisors_of_torsion.

There is also a version for periodic elements of an additive monoid: zero_divisors_of_periodic.

The converse of this statement is Kaplansky's zero divisor conjecture.

The formalized example generalizes in trivial ways the assumptions: the field k can be any nontrivial ring R and the additive group G with a torsion element can be any additive monoid A with a non-zero periodic element.

Besides this example, we also address a comment in data.finsupp.lex to the effect that the proof that addition is monotone on α →₀ N uses that it is strictly monotone on N.

The specific statement is about finsupp.lex.covariant_class_le_left and its analogue finsupp.lex.covariant_class_le_right. We do not need two separate counterexamples, since the operation is commutative.

The example is very simple. Let F = {0, 1} with order determined by 0 < 1 and absorbing addition (which is the same as max in this case). We denote a function f : F → F (which is automatically finitely supported!) by [f 0, f 1], listing its values. Recall that the order on finitely supported function is lexicographic, matching the list notation. The inequality [0, 1] ≤ [1, 0] holds. However, adding [1, 0] to both sides yields the reversed inequality [1, 1] > [1, 0].

source
theorem counterexample.zero_divisors_of_periodic {R : Type u_1} {A : Type u_2} [nontrivial R] [ring R] [add_monoid A] {n : ℕ} (a : A) (n2 : 2 ≤ n) (na : n • a = a) (na1 : (n - 1) • a ≠ 0) :
∃ (f g : add_monoid_algebra R A), f ≠ 0 ∧ g ≠ 0 ∧ f * g = 0

This is a simple example showing that if R is a non-trivial ring and A is an additive monoid with an element a satisfying n • a = a and (n - 1) • a ≠ a, for some 2 ≤ n, then add_monoid_algebra R A contains non-zero zero-divisors. The elements are easy to write down: [a] and [a] ^ (n - 1) - 1 are non-zero elements of add_monoid_algebra R A whose product is zero.

Observe that such an element a cannot be invertible. In particular, this lemma never applies if A is a group.

source
theorem counterexample.single_zero_one {R : Type u_1} {A : Type u_2} [semiring R] [has_zero A] :
finsupp.single 0 1 = 1
source
theorem counterexample.zero_divisors_of_torsion {R : Type u_1} {A : Type u_2} [nontrivial R] [ring R] [add_monoid A] (a : A) (o2 : 2 ≤ add_order_of a) :
∃ (f g : add_monoid_algebra R A), f ≠ 0 ∧ g ≠ 0 ∧ f * g = 0

This is a simple example showing that if R is a non-trivial ring and A is an additive monoid with a non-zero element a of finite order oa, then add_monoid_algebra R A contains non-zero zero-divisors. The elements are easy to write down: ∑ i in finset.range oa, [a] ^ i and [a] - 1 are non-zero elements of add_monoid_algebra R A whose product is zero.

In particular, this applies whenever the additive monoid A is an additive group with a non-zero torsion element.

source
@[protected, instance]
def counterexample.F.inhabited  :
inhabited counterexample.F
source
@[protected, instance]
def counterexample.F.decidable_eq  :
decidable_eq counterexample.F
source
inductive counterexample.F  :
Type

F is the type with two elements zero and one. We define the "obvious" linear order and absorbing addition on it to generate our counterexample.

Instances for counterexample.F
source
def counterexample.list.drop_until {α : Type u_1} [decidable_eq α] :
list α → list α → list α

The same as list.get_rest, except that we take the "rest" from the first match, rather than from the beginning, returning [] if there is no match. For instance,

#eval [1,2].drop_until [3,1,2,4,1,2]  -- [4, 1, 2]
Equations
source
meta def counterexample.guard_decl_in_file (na : name) (loc : list string) :
tactic unit

guard_decl_in_file na loc makes sure that the declaration with name na is in the file with relative path "src/" ++ "/".intercalate loc ++ ".lean".

#eval guard_decl_in_file `nat.nontrivial ["data", "nat", "basic"]  -- does nothing

#eval guard_decl_in_file `nat.nontrivial ["not", "in", "here"]
-- fails giving the location 'data/nat/basic.lean'

This test makes sure that the comment referring to this example is in the file claimed in the doc-module to this counterexample.

source
@[protected, instance]
def counterexample.F.has_zero  :
has_zero counterexample.F
Equations
source
@[protected, instance]
def counterexample.F.has_one  :
has_one counterexample.F

1 is not really needed, but it is nice to use the notation.

Equations
source
meta def counterexample.F.boom  :
tactic unit

A tactic to prove trivial goals by enumeration.

source
def counterexample.F.val  :
counterexample.F → ℕ

val maps 0 1 : F to their counterparts in ℕ. We use it to lift the linear order on ℕ.

Equations
source
@[protected, instance]
def counterexample.F.linear_order  :
linear_order counterexample.F
Equations
source
@[simp]
theorem counterexample.F.z01  :
0 < 1
source
@[protected, instance]
def counterexample.F.add_comm_monoid  :
add_comm_monoid counterexample.F

F would be a comm_semiring, using min as multiplication. Again, we do not need this.

Equations
source
@[protected, instance]
def counterexample.F.covariant_class_add_le  :
covariant_class counterexample.F counterexample.F has_add.add has_le.le

The covariant_classes asserting monotonicity of addition hold for F.

source
@[simp]
theorem counterexample.F.f1 (a : counterexample.F) :
1 + a = 1

A few simp-lemmas to take care of trivialities in the proof of the example below.

source
@[simp]
theorem counterexample.F.f011  :
⇑(⇑of_lex (finsupp.single 0 1)) 1 = 0
source
@[simp]
theorem counterexample.F.f010  :
⇑(⇑of_lex (finsupp.single 0 1)) 0 = 1
source
@[simp]
theorem counterexample.F.f111  :
⇑(⇑of_lex (finsupp.single 1 1)) 1 = 1
source
@[simp]
theorem counterexample.F.f110  :
⇑(⇑of_lex (finsupp.single 1 1)) 0 = 0