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].
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.
Instances For
Equations
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
1 is not really needed, but it is nice to use the notation.
Equations
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
F would be a CommSemiring, using min as multiplication. Again, we do not need this.
Equations
- One or more equations did not get rendered due to their size.
The AddLeftMonoes asserting monotonicity of addition hold for F.
A few simp-lemmas to take care of trivialities in the proof of the example below.