Documentation

Counterexamples.CanonicallyOrderedCommSemiringTwoMul

A canonically ordered commutative 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 commutative 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

theorem Counterexample.mem_zmod_2 (a : ZMod 2) :

a = 0 ∨ a = 1

theorem Counterexample.add_self_zmod_2 (a : ZMod 2) :

a + a = 0

instance Counterexample.Nxzmod2.preN2 :

PartialOrder (ℕ × 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

One or more equations did not get rendered due to their size.

instance Counterexample.Nxzmod2.csrN2 :

CommSemiring (ℕ × ZMod 2)

Equations

Counterexample.Nxzmod2.csrN2 = inferInstance

instance Counterexample.Nxzmod2.csrN21 :

AddCancelCommMonoid (ℕ × ZMod 2)

Equations

Counterexample.Nxzmod2.csrN21 = { toAddCommMonoid := NonUnitalNonAssocSemiring.toAddCommMonoid, add_left_cancel := Counterexample.Nxzmod2.csrN21._proof_5 }

@[simp]

theorem Counterexample.Nxzmod2.lt_def {a 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 b c : ℕ × ZMod 2) :

a + b = a + c → b = c

theorem Counterexample.Nxzmod2.add_le_add_left (a b : ℕ × ZMod 2) :

a ≤ b → ∀ (c : ℕ × ZMod 2), c + a ≤ c + b

theorem Counterexample.Nxzmod2.le_of_add_le_add_left (a b c : ℕ × ZMod 2) :

a + b ≤ a + c → b ≤ c

instance Counterexample.Nxzmod2.instZeroLEOneClassProdNatZModOfNat_counterexamples :

ZeroLEOneClass (ℕ × ZMod 2)

theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_left (a b c : ℕ × ZMod 2) :

a < b → 0 < c → c * a < c * b

theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_right (a b c : ℕ × ZMod 2) :

a < b → 0 < c → a * c < b * c

instance Counterexample.Nxzmod2.isorN2 :

IsStrictOrderedRing (ℕ × ZMod 2)

def Counterexample.ExL.L :

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

Equations

Counterexample.ExL.L = { l : ℕ × ZMod 2 // l ≠ (0, 1) }

Instances For

theorem Counterexample.ExL.add_L {a b : ℕ × ZMod 2} (ha : a ≠ (0, 1)) (hb : b ≠ (0, 1)) :

a + b ≠ (0, 1)

theorem Counterexample.ExL.mul_L {a b : ℕ × ZMod 2} (ha : a ≠ (0, 1)) (hb : b ≠ (0, 1)) :

a * b ≠ (0, 1)

def Counterexample.ExL.lSubsemiring :

Subsemiring (ℕ × ZMod 2)

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

instance Counterexample.ExL.instCommSemiringL :

Equations

Counterexample.ExL.instCommSemiringL = Counterexample.ExL.lSubsemiring.toCommSemiring

instance Counterexample.ExL.instPartialOrderL :

Equations

Counterexample.ExL.instPartialOrderL = Subtype.partialOrder fun (l : ℕ × ZMod 2) => l ≠ (0, 1)

instance Counterexample.ExL.instIsOrderedRingL :

IsOrderedRing L

instance Counterexample.ExL.inhabited :

Equations

Counterexample.ExL.inhabited = { default := 1 }

theorem Counterexample.ExL.bot_le (a : L) :

0 ≤ a

instance Counterexample.ExL.orderBot :

Equations

Counterexample.ExL.orderBot = { bot := 0, bot_le := Counterexample.ExL.bot_le }

theorem Counterexample.ExL.exists_add_of_le (a b : L) :

a ≤ b → ∃ (c : L), b = a + c

theorem Counterexample.ExL.le_self_add (a b : L) :

a ≤ a + b

theorem Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zero (a b : L) :

a * b = 0 → a = 0 ∨ b = 0

instance Counterexample.ExL.instCommSemiringL_1 :

Equations

Counterexample.ExL.instCommSemiringL_1 = inferInstance

instance Counterexample.ExL.instPartialOrderL_1 :

Equations

Counterexample.ExL.instPartialOrderL_1 = inferInstance

instance Counterexample.ExL.instIsOrderedRingL_1 :

IsOrderedRing L

instance Counterexample.ExL.instCanonicallyOrderedAddL :

CanonicallyOrderedAdd L

instance Counterexample.ExL.instNoZeroDivisorsL :

NoZeroDivisors L