Examples of zero-divisors in AddMonoidAlgebra
s #
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]
.
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.
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.
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
Instances For
Equations
- Counterexample.instDecidableEqF x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Counterexample.instInhabitedF = { default := Counterexample.F.zero }
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)
Instances For
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.
Instances For
Equations
- Counterexample.F.instZero = { zero := Counterexample.F.zero }
1
is not really needed, but it is nice to use the notation.
Equations
- Counterexample.F.instOne = { one := Counterexample.F.one }
A tactic to prove trivial goals by enumeration.
Equations
- Counterexample.F.tacticBoom = Lean.ParserDescr.node `Counterexample.F.tacticBoom 1024 (Lean.ParserDescr.nonReservedSymbol "boom" false)
Instances For
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
Instances For
Equations
- Counterexample.F.instAdd = { add := max }
F
would be a CommSemiring
, using min
as multiplication. Again, we do not need this.
The AddLeftMono
es asserting monotonicity of addition hold for F
.
A few simp
-lemmas to take care of trivialities in the proof of the example below.