Examples of zero-divisors in AddMonoidAlgebras

This file contains an easy source of zero-divisors in an AddMonoidAlgebra. If k is a field and G is an additive group containing a non-zero torsion element, then 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.addLeftStrictMono and its analogue Finsupp.Lex.addRightStrictMono. 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].

theorem Counterexample.zero_divisors_of_periodic {R : Type u_1} {A : Type u_2} [Nontrivial R] [Ring R] [AddMonoid A] {n : ℕ} (a : A) (n2 : 2 ≤ n) (na : n • a = a) (na1 : (n - 1) • a ≠ 0) : ∃ (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra 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 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 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.

theorem Counterexample.single_zero_one {R : Type u_1} {A : Type u_2} [Semiring R] [Zero A] : AddMonoidAlgebra.single 0 1 = 1

theorem Counterexample.zero_divisors_of_torsion {R : Type u_1} {A : Type u_2} [Nontrivial R] [Ring R] [AddMonoid A] (a : A) (o2 : 2 ≤ addOrderOf a) : ∃ (f : AddMonoidAlgebra R A) (g : AddMonoidAlgebra 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 R[A] contains non-zero zero-divisors. The elements are easy to write down: ∑ i ∈ Finset.range oa, [a] ^ i and [a] - 1 are non-zero elements of 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.

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.

• zero : Counterexample.F
• one : Counterexample.F

instance Counterexample.instDecidableEqF : DecidableEq Counterexample.F

Equations

• Counterexample.instDecidableEqF x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Counterexample.instInhabitedF : Inhabited Counterexample.F

Equations

• Counterexample.instInhabitedF = { default := Counterexample.F.zero }

def Counterexample.List.dropUntil {α : Type u_1} [DecidableEq α] : List α → List α → List α

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

#eval dropUntil [1,2] [3,1,2,4,1,2]  -- [4, 1, 2]

Equations

• Counterexample.List.dropUntil x✝ [] = []
• Counterexample.List.dropUntil x✝ (a :: as) = ((a :: as).getRest x✝).getD (Counterexample.List.dropUntil x✝ as)

def Counterexample.commandGuard_decl__ : Lean.ParserDescr

guard_decl na mod makes sure that the declaration with name na is in the module mod.

guard_decl Nat.nontrivial Mathlib.Algebra.Ring.Nat -- does nothing

guard_decl Nat.nontrivial Not.In.Here
-- the module Not.In.Here is not imported!

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

Equations

• One or more equations did not get rendered due to their size.

instance Counterexample.F.instZero : Zero Counterexample.F

Equations

• Counterexample.F.instZero = { zero := Counterexample.F.zero }

instance Counterexample.F.instOne : One Counterexample.F

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

Equations

• Counterexample.F.instOne = { one := Counterexample.F.one }

def Counterexample.F.tacticBoom : Lean.ParserDescr

A tactic to prove trivial goals by enumeration.

Equations

• Counterexample.F.tacticBoom = Lean.ParserDescr.node `Counterexample.F.tacticBoom 1024 (Lean.ParserDescr.nonReservedSymbol "boom" false)

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

• Counterexample.F.zero.val = 0
• Counterexample.F.one.val = 1

instance Counterexample.F.instLinearOrder : LinearOrder Counterexample.F

Equations

• Counterexample.F.instLinearOrder = LinearOrder.lift' Counterexample.F.val Counterexample.F.instLinearOrder.proof_1

@[simp]

theorem Counterexample.F.z01 : 0 < 1

instance Counterexample.F.instAdd : Add Counterexample.F

Equations

• Counterexample.F.instAdd = { add := max }

instance Counterexample.F.instAddCommMonoid : AddCommMonoid Counterexample.F

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

Equations

• Counterexample.F.instAddCommMonoid = AddCommMonoid.mk Counterexample.F.instAddCommMonoid.proof_6

instance Counterexample.F.addLeftMono : AddLeftMono Counterexample.F

The AddLeftMonoes asserting monotonicity of addition hold for F.

@[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.

@[simp]

theorem Counterexample.F.f011 : (ofLex (Finsupp.single 0 1)) 1 = 0

@[simp]

theorem Counterexample.F.f010 : (ofLex (Finsupp.single 0 1)) 0 = 1

@[simp]

theorem Counterexample.F.f111 : (ofLex (Finsupp.single 1 1)) 1 = 1

@[simp]

theorem Counterexample.F.f110 : (ofLex (Finsupp.single 1 1)) 0 = 0