Basic facts for ordered rings and semirings #
This file develops the basics of ordered (semi)rings in an unbundled fashion for later use with
the bundled classes from Algebra.Order.Ring.Defs
.
The set of typeclass variables here comprises
- an algebraic class (
Semiring
,CommSemiring
,Ring
,CommRing
) - an order class (
PartialOrder
,LinearOrder
) - assumptions on how both interact ((strict) monotonicity, canonicity)
For short,
- "
+
respects≤
" means "monotonicity of addition" - "
+
respects<
" means "strict monotonicity of addition" - "
*
respects≤
" means "monotonicity of multiplication by a nonnegative number". - "
*
respects<
" means "strict monotonicity of multiplication by a positive number".
Typeclasses found in Algebra.Order.Ring.Defs
#
OrderedSemiring
: Semiring with a partial order such that+
and*
respect≤
.StrictOrderedSemiring
: Nontrivial semiring with a partial order such that+
and*
respects<
.OrderedCommSemiring
: Commutative semiring with a partial order such that+
and*
respect≤
.StrictOrderedCommSemiring
: Nontrivial commutative semiring with a partial order such that+
and*
respect<
.OrderedRing
: Ring with a partial order such that+
respects≤
and*
respects<
.OrderedCommRing
: Commutative ring with a partial order such that+
respects≤
and*
respects<
.LinearOrderedSemiring
: Nontrivial semiring with a linear order such that+
respects≤
and*
respects<
.LinearOrderedCommSemiring
: Nontrivial commutative semiring with a linear order such that+
respects≤
and*
respects<
.LinearOrderedRing
: Nontrivial ring with a linear order such that+
respects≤
and*
respects<
.LinearOrderedCommRing
: Nontrivial commutative ring with a linear order such that+
respects≤
and*
respects<
.CanonicallyOrderedCommSemiring
: Commutative semiring with a partial order such that+
respects≤
,*
respects<
, anda ≤ b ↔ ∃ c, b = a + c
.
Hierarchy #
The hardest part of proving order lemmas might be to figure out the correct generality and its corresponding typeclass. Here's an attempt at demystifying it. For each typeclass, we list its immediate predecessors and what conditions are added to each of them.
OrderedSemiring
OrderedAddCommMonoid
& multiplication &*
respects≤
Semiring
& partial order structure &+
respects≤
&*
respects≤
StrictOrderedSemiring
OrderedCancelAddCommMonoid
& multiplication &*
respects<
& nontrivialityOrderedSemiring
&+
respects<
&*
respects<
& nontriviality
OrderedCommSemiring
OrderedSemiring
& commutativity of multiplicationCommSemiring
& partial order structure &+
respects≤
&*
respects<
StrictOrderedCommSemiring
StrictOrderedSemiring
& commutativity of multiplicationOrderedCommSemiring
&+
respects<
&*
respects<
& nontriviality
OrderedRing
OrderedSemiring
& additive inversesOrderedAddCommGroup
& multiplication &*
respects<
Ring
& partial order structure &+
respects≤
&*
respects<
StrictOrderedRing
StrictOrderedSemiring
& additive inversesOrderedSemiring
&+
respects<
&*
respects<
& nontriviality
OrderedCommRing
OrderedRing
& commutativity of multiplicationOrderedCommSemiring
& additive inversesCommRing
& partial order structure &+
respects≤
&*
respects<
StrictOrderedCommRing
StrictOrderedCommSemiring
& additive inversesStrictOrderedRing
& commutativity of multiplicationOrderedCommRing
&+
respects<
&*
respects<
& nontriviality
LinearOrderedSemiring
StrictOrderedSemiring
& totality of the orderLinearOrderedAddCommMonoid
& multiplication & nontriviality &*
respects<
LinearOrderedCommSemiring
StrictOrderedCommSemiring
& totality of the orderLinearOrderedSemiring
& commutativity of multiplication
LinearOrderedRing
LinearOrderedCommRing
Generality #
Each section is labelled with a corresponding bundled ordered ring typeclass in mind. Mixin's for relating the order structures and ring structures are added as needed.
TODO: the mixin assumptiosn can be relaxed in most cases
Note that OrderDual
does not satisfy any of the ordered ring typeclasses due to the
zero_le_one
field.
Variant of mul_le_of_le_one_left
for b
non-positive instead of non-negative.
Variant of le_mul_of_one_le_left
for b
non-positive instead of non-negative.
Variant of mul_le_of_le_one_right
for a
non-positive instead of non-negative.
Variant of le_mul_of_one_le_right
for a
non-positive instead of non-negative.
Variant of mul_lt_of_lt_one_left
for b
negative instead of positive.
Variant of lt_mul_of_one_lt_left
for b
negative instead of positive.
Variant of mul_lt_of_lt_one_right
for a
negative instead of positive.
Variant of lt_mul_of_lt_one_right
for a
negative instead of positive.
Binary rearrangement inequality.
Binary rearrangement inequality.
Binary strict rearrangement inequality.
Binary rearrangement inequality.
Out of three elements of a LinearOrderedRing
, two must have the same sign.
Alias of sq_nonneg
.
The sum of two squares is zero iff both elements are zero.
Binary arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.
Alias of two_mul_le_add_sq
.
Binary arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.