Documentation

Counterexamples.ZeroDivisorsInAddMonoidAlgebras

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 : FF (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.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.

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
    Equations
    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
    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

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

        Equations

        A tactic to prove trivial goals by enumeration.

        Equations
        Instances For

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

          Equations
          Instances For
            @[simp]
            theorem Counterexample.F.z01 :
            0 < 1

            The AddLeftMonoes asserting monotonicity of addition hold for F.

            @[simp]

            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