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
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.
Instances For
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.
Initially, L
was defined as the subsemiring closure of (1,0)
.
Instances For
The subsemiring corresponding to the elements of L
, used to transfer instances.