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.covariantClass_lt_left and its analogue Finsupp.Lex.covariantClass_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 : 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 CovariantClasses asserting monotonicity of addition hold for F.

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