Documentation

Counterexamples.CanonicallyOrderedCommSemiringTwoMul

A CanonicallyOrderedCommSemiring with two different elements a and b such that a ≠ b and 2 * a = 2 * b. Thus, multiplication by a fixed non-zero element of a canonically ordered semiring need not be injective. In particular, multiplying by a strictly positive element need not be strictly monotone.

Recall that a CanonicallyOrderedCommSemiring is a commutative semiring with a partial ordering that is "canonical" in the sense that the inequality a ≤ b holds if and only if there is a c such that a + c = b. There are several compatibility conditions among addition/multiplication and the order relation. The point of the counterexample is to show that monotonicity of multiplication cannot be strengthened to strict monotonicity.

Reference: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology

theorem Counterexample.mem_zmod_2 (a : ZMod 2) :
a = 0 a = 1

The preorder relation on ℕ × ℤ/2ℤ where we only compare the first coordinate, except that we leave incomparable each pair of elements with the same first component. For instance, ∀ α, β ∈ ℤ/2ℤ, the inequality (1,α) ≤ (2,β) holds, whereas, ∀ n ∈ ℤ, the elements (n,0) and (n,1) are incomparable.

Equations
@[simp]
theorem Counterexample.Nxzmod2.lt_def {a : × ZMod 2} {b : × ZMod 2} :
a < b a.1 < b.1

A strict inequality forces the first components to be different.

theorem Counterexample.Nxzmod2.add_left_cancel (a : × ZMod 2) (b : × ZMod 2) (c : × ZMod 2) :
a + b = a + cb = c
theorem Counterexample.Nxzmod2.add_le_add_left (a : × ZMod 2) (b : × ZMod 2) :
a b∀ (c : × ZMod 2), c + a c + b
theorem Counterexample.Nxzmod2.le_of_add_le_add_left (a : × ZMod 2) (b : × ZMod 2) (c : × ZMod 2) :
a + b a + cb c
theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_left (a : × ZMod 2) (b : × ZMod 2) (c : × ZMod 2) :
a < b0 < cc * a < c * b
theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_right (a : × ZMod 2) (b : × ZMod 2) (c : × ZMod 2) :
a < b0 < ca * c < b * c

Initially, L was defined as the subsemiring closure of (1,0).

Equations
Instances For
    theorem Counterexample.ExL.add_L {a : × ZMod 2} {b : × ZMod 2} (ha : a (0, 1)) (hb : b (0, 1)) :
    a + b (0, 1)
    theorem Counterexample.ExL.mul_L {a : × ZMod 2} {b : × ZMod 2} (ha : a (0, 1)) (hb : b (0, 1)) :
    a * b (0, 1)

    The subsemiring corresponding to the elements of L, used to transfer instances.

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