mathlib3 documentation

mathlib-counterexamples / canonically_ordered_comm_semiring_two_mul

A canonically_ordered_comm_semiring 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 canonically_ordered_comm_semiring 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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
def counterexample.from_Bhavik.K  :
Type

Bhavik Mehta's example. There are only the initial definitions, but no proofs. The Type K is a canonically ordered commutative semiring with the property that 2 * (1/2) ≤ 2 * 1, even though it is not true that 1/2 ≤ 1, since 1/2 and 1 are not comparable.

Equations
Instances for counterexample.from_Bhavik.K
source
@[protected, instance]
def counterexample.from_Bhavik.K.comm_semiring  :
comm_semiring counterexample.from_Bhavik.K
source
@[protected, instance]
def counterexample.from_Bhavik.rat.has_coe  :
has_coe counterexample.from_Bhavik.K ℚ
Equations
source
@[protected, instance]
def counterexample.from_Bhavik.inhabited_K  :
inhabited counterexample.from_Bhavik.K
Equations
source
@[protected, instance]
def counterexample.from_Bhavik.K.preorder  :
preorder counterexample.from_Bhavik.K
Equations
source
theorem counterexample.mem_zmod_2 (a : zmod 2) :
a = 0 ∨ a = 1
source
theorem counterexample.add_self_zmod_2 (a : zmod 2) :
a + a = 0
source
@[protected, instance]
def counterexample.Nxzmod_2.preN2  :
partial_order (ℕ × zmod 2)

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
source
@[protected, instance]
def counterexample.Nxzmod_2.csrN2  :
comm_semiring (ℕ × zmod 2)
Equations
source
@[protected, instance]
def counterexample.Nxzmod_2.csrN2_1  :
add_cancel_comm_monoid (ℕ × zmod 2)
Equations
source
@[simp]
theorem counterexample.Nxzmod_2.lt_def {a b : ℕ × zmod 2} :
a < b ↔ a.fst < b.fst

A strict inequality forces the first components to be different.

source
theorem counterexample.Nxzmod_2.add_left_cancel (a b c : ℕ × zmod 2) :
a + b = a + c → b = c
source
theorem counterexample.Nxzmod_2.add_le_add_left (a b : ℕ × zmod 2) :
a ≤ b → ∀ (c : ℕ × zmod 2), c + a ≤ c + b
source
theorem counterexample.Nxzmod_2.le_of_add_le_add_left (a b c : ℕ × zmod 2) :
a + b ≤ a + c → b ≤ c
source
@[protected, instance]
def counterexample.Nxzmod_2.prod.zero_le_one_class  :
zero_le_one_class (ℕ × zmod 2)
Equations
source
theorem counterexample.Nxzmod_2.mul_lt_mul_of_pos_left (a b c : ℕ × zmod 2) :
a < b → 0 < c → c * a < c * b
source
theorem counterexample.Nxzmod_2.mul_lt_mul_of_pos_right (a b c : ℕ × zmod 2) :
a < b → 0 < c → a * c < b * c
source
@[protected, instance]
def counterexample.Nxzmod_2.socsN2  :
strict_ordered_comm_semiring (ℕ × zmod 2)
Equations
source
def counterexample.ex_L.L  :
Type

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

Equations
Instances for counterexample.ex_L.L
source
theorem counterexample.ex_L.add_L {a b : ℕ × zmod 2} (ha : a ≠ (0, 1)) (hb : b ≠ (0, 1)) :
a + b ≠ (0, 1)
source
theorem counterexample.ex_L.mul_L {a b : ℕ × zmod 2} (ha : a ≠ (0, 1)) (hb : b ≠ (0, 1)) :
a * b ≠ (0, 1)
source
def counterexample.ex_L.L_subsemiring  :
subsemiring (ℕ × zmod 2)

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

Equations
source
@[protected, instance]
def counterexample.ex_L.L.ordered_comm_semiring  :
ordered_comm_semiring counterexample.ex_L.L
Equations
source
@[protected, instance]
def counterexample.ex_L.inhabited  :
inhabited counterexample.ex_L.L
Equations
source
theorem counterexample.ex_L.bot_le (a : counterexample.ex_L.L) :
0 ≤ a
source
@[protected, instance]
def counterexample.ex_L.order_bot  :
order_bot counterexample.ex_L.L
Equations
source
theorem counterexample.ex_L.exists_add_of_le (a b : counterexample.ex_L.L) :
a ≤ b → (∃ (c : counterexample.ex_L.L), b = a + c)
source
theorem counterexample.ex_L.le_self_add (a b : counterexample.ex_L.L) :
a ≤ a + b
source
theorem counterexample.ex_L.eq_zero_or_eq_zero_of_mul_eq_zero (a b : counterexample.ex_L.L) :
a * b = 0 → a = 0 ∨ b = 0
source
@[protected, instance]
def counterexample.ex_L.can  :
canonically_ordered_comm_semiring counterexample.ex_L.L
Equations