Ordered rings and semirings

This file develops the basics of ordered (semi)rings.

Each typeclass 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

• IsOrderedRing: Semiring with a partial order such that addition and multiplication by a nonnegative number are both monotone.
• IsStrictOrderedRing: Nontrivial semiring with a partial order such that addition and multiplication by a positive number are both strictly monotone.

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.

• PartialOrder + Semiring + IsOrderedRing
  • IsOrderedAddMonoid & multiplication & * respects ≤
• PartialOrder + Semiring + IsStrictOrderedRing
  • IsOrderedCancelAddMonoid & multiplication & * respects < & nontriviality
• LinearOrder + Ring + IsOrderedRing
  • IsStrictOrderedRing & totality of the order
  • IsDomain & linear order structure

class IsOrderedRing (R : Type u_1) [Semiring R] [PartialOrder R] extends IsOrderedAddMonoid R, ZeroLEOneClass R, PosMulMono R, MulPosMono R : Prop

An ordered semiring is a semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), a + c ≤ b + c
• add_le_add_right (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• zero_le_one : 0 ≤ 1
• mul_le_mul_of_nonneg_left ⦃a : R⦄ (ha : 0 ≤ a) ⦃b c : R⦄ (hbc : b ≤ c) : a * b ≤ a * c
• mul_le_mul_of_nonneg_right ⦃c : R⦄ (hc : 0 ≤ c) ⦃a b : R⦄ (hab : a ≤ b) : a * c ≤ b * c

class IsStrictOrderedRing (R : Type u_1) [Semiring R] [PartialOrder R] extends IsOrderedCancelAddMonoid R, ZeroLEOneClass R, Nontrivial R, PosMulStrictMono R, MulPosStrictMono R : Prop

A strict ordered semiring is a nontrivial semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), a + c ≤ b + c
• add_le_add_right (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• le_of_add_le_add_left (a b c : R) : a + b ≤ a + c → b ≤ c
• le_of_add_le_add_right (a b c : R) : b + a ≤ c + a → b ≤ c
• zero_le_one : 0 ≤ 1
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• mul_lt_mul_of_pos_left ⦃a : R⦄ (ha : 0 < a) ⦃b c : R⦄ (hbc : b < c) : a * b < a * c
• mul_lt_mul_of_pos_right ⦃c : R⦄ (hc : 0 < c) ⦃a b : R⦄ (hab : a < b) : a * c < b * c

instance instOrderedRingOfIsStrictOrderedRing {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Lean.Grind.OrderedRing R

theorem IsOrderedRing.of_mul_nonneg {R : Type u} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] (mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b) : IsOrderedRing R

theorem IsStrictOrderedRing.of_mul_pos {R : Type u} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] [Nontrivial R] (mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b) : IsStrictOrderedRing R

@[instance 50]

instance IsOrderedRing.toIsStrictOrderedRing (R : Type u_1) [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Nontrivial R] : IsStrictOrderedRing R

Turn an ordered domain into a strict ordered ring.

@[instance 100]

instance IsStrictOrderedRing.toIsOrderedRing {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : IsOrderedRing R

theorem AddMonoidWithOne.toCharZero {R : Type u_1} [AddMonoidWithOne R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] : CharZero R

This is not an instance, as it would loop with NeZero.charZero_one.

@[instance 100]

instance IsStrictOrderedRing.toCharZero {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : CharZero R

@[instance 100]

instance IsStrictOrderedRing.toNoMaxOrder {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : NoMaxOrder R

@[instance 100]

instance IsStrictOrderedRing.noZeroDivisors {R : Type u} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] : NoZeroDivisors R

@[instance 100]

instance IsStrictOrderedRing.isDomain {R : Type u} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] : IsDomain R

Note that OrderDual does not satisfy any of the ordered ring typeclasses due to the zero_le_one field.

theorem one_add_le_one_sub_mul_one_add {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c)

theorem one_add_le_one_add_mul_one_sub {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c)

theorem one_sub_le_one_sub_mul_one_add {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : b + b * c ≤ a + c) : 1 - a ≤ (1 - b) * (1 + c)

theorem one_sub_le_one_add_mul_one_sub {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c)

theorem IsOrderedRing.toCharZero {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] : CharZero R

A nontrivial ordered ring is of characteristic zero. This is not made a global instance for performance reasons.

instance instNoMaxOrderOfNontrivial {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] : NoMaxOrder R

instance instNoMinOrderOfNontrivial {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] : NoMinOrder R