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

• 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 <.

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 < & nontriviality
  • OrderedSemiring & + respects < & * respects < & nontriviality
• OrderedCommSemiring
  • OrderedSemiring & commutativity of multiplication
  • CommSemiring & partial order structure & + respects ≤ & * respects <
• StrictOrderedCommSemiring
  • StrictOrderedSemiring & commutativity of multiplication
  • OrderedCommSemiring & + respects < & * respects < & nontriviality
• OrderedRing
  • OrderedSemiring & additive inverses
  • OrderedAddCommGroup & multiplication & * respects <
  • Ring & partial order structure & + respects ≤ & * respects <
• StrictOrderedRing
  • StrictOrderedSemiring & additive inverses
  • OrderedSemiring & + respects < & * respects < & nontriviality
• OrderedCommRing
  • OrderedRing & commutativity of multiplication
  • OrderedCommSemiring & additive inverses
  • CommRing & partial order structure & + respects ≤ & * respects <
• StrictOrderedCommRing
  • StrictOrderedCommSemiring & additive inverses
  • StrictOrderedRing & commutativity of multiplication
  • OrderedCommRing & + respects < & * respects < & nontriviality
• LinearOrderedSemiring
  • StrictOrderedSemiring & totality of the order
  • LinearOrderedAddCommMonoid & multiplication & nontriviality & * respects <
• LinearOrderedCommSemiring
  • StrictOrderedCommSemiring & totality of the order
  • LinearOrderedSemiring & commutativity of multiplication
• LinearOrderedRing
  • StrictOrderedRing & totality of the order
  • LinearOrderedSemiring & additive inverses
  • LinearOrderedAddCommGroup & multiplication & * respects <
  • Ring & IsDomain & linear order structure
• LinearOrderedCommRing
  • StrictOrderedCommRing & totality of the order
  • LinearOrderedRing & commutativity of multiplication
  • LinearOrderedCommSemiring & additive inverses
  • CommRing & 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), c + a ≤ c + b
• add_le_add_right (a b : R) : a ≤ b → ∀ (c : R), a + c ≤ b + c
• 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), c + a ≤ c + b
• add_le_add_right (a b : R) : a ≤ b → ∀ (c : R), a + c ≤ b + c
• 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)

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