Canonically ordered monoids

class CanonicallyOrderedAdd (α : Type u_1) [Add α] [LE α] extends ExistsAddOfLE α : Prop

An ordered additive monoid is CanonicallyOrderedAdd if the ordering coincides with the subtractibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other nontrivial OrderedAddCommGroups.

We have a ≤ b + a and a ≤ a + b as separate fields. In the commutative case the second field is redundant, but in the noncommutative case (satisfied most relevantly by the ordinals), this extra field allows us to prove more things without the extra commutativity assumption.

• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
• le_add_self (a b : α) : a ≤ b + a

  For any a and b, a ≤ a + b

• le_self_add (a b : α) : a ≤ a + b

class CanonicallyOrderedMul (α : Type u_1) [Mul α] [LE α] extends ExistsMulOfLE α : Prop

An ordered monoid is CanonicallyOrderedMul if the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a * c. Examples seem rare; it seems more likely that the OrderDual of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

• exists_mul_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a * c
• le_mul_self (a b : α) : a ≤ b * a

  For any a and b, a ≤ a * b

• le_self_mul (a b : α) : a ≤ a * b

theorem le_mul_self {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] {a b : α} : a ≤ b * a

theorem le_add_self {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b + a

theorem le_self_mul {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] {a b : α} : a ≤ a * b

theorem le_self_add {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ a + b

@[simp]

theorem self_le_mul_left {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] (a b : α) : a ≤ b * a

@[simp]

theorem self_le_add_left {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] (a b : α) : a ≤ b + a

@[simp]

theorem self_le_mul_right {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] (a b : α) : a ≤ a * b

@[simp]

theorem self_le_add_right {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] (a b : α) : a ≤ a + b

theorem le_iff_exists_mul {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = a * c

theorem le_iff_exists_add {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = a + c

theorem le_of_mul_le_left {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a * b ≤ c → a ≤ c

theorem le_of_add_le_left {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a + b ≤ c → a ≤ c

theorem le_mul_of_le_left {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ b → a ≤ b * c

theorem le_add_of_le_left {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ b → a ≤ b + c

theorem le_of_mul_le_right {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a * b ≤ c → b ≤ c

theorem le_of_add_le_right {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a + b ≤ c → b ≤ c

theorem le_mul_of_le_right {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ c → a ≤ b * c

theorem le_add_of_le_right {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ c → a ≤ b + c

theorem le_mul_left {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ c → a ≤ b * c

Alias of le_mul_of_le_right.

theorem le_add_left {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ c → a ≤ b + c

theorem le_mul_right {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ b → a ≤ b * c

Alias of le_mul_of_le_left.

theorem le_add_right {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ b → a ≤ b + c

theorem le_iff_exists_mul' {α : Type u} [CommMagma α] [Preorder α] [CanonicallyOrderedMul α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = c * a

theorem le_iff_exists_add' {α : Type u} [AddCommMagma α] [Preorder α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = c + a

instance instIsBotOneClass {α : Type u} [MulOneClass α] [LE α] [CanonicallyOrderedMul α] : IsBotOneClass α

instance instIsBotZeroClass {α : Type u} [AddZeroClass α] [LE α] [CanonicallyOrderedAdd α] : IsBotZeroClass α

theorem exists_one_lt_mul_of_lt {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a b : α} (h : a < b) : ∃ (c : α), ∃ (x : 1 < c), a * c = b

theorem exists_pos_add_of_lt {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} (h : a < b) : ∃ (c : α), ∃ (x : 0 < c), a + c = b

theorem lt_iff_exists_mul {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a b : α} [MulLeftStrictMono α] : a < b ↔ ∃ (c : α), c > 1 ∧ b = a * c

theorem lt_iff_exists_add {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} [AddLeftStrictMono α] : a < b ↔ ∃ (c : α), c > 0 ∧ b = a + c

@[instance 10]

instance CanonicallyOrderedMul.toMulLeftMono {α : Type u} [Semigroup α] [LE α] [CanonicallyOrderedMul α] : MulLeftMono α

@[instance 10]

instance CanonicallyOrderedAdd.toAddLeftMono {α : Type u} [AddSemigroup α] [LE α] [CanonicallyOrderedAdd α] : AddLeftMono α

theorem CanonicallyOrderedMul.toIsOrderedMonoid {α : Type u} [CommMonoid α] [Preorder α] [CanonicallyOrderedMul α] : IsOrderedMonoid α

theorem CanonicallyOrderedAdd.toIsOrderedAddMonoid {α : Type u} [AddCommMonoid α] [Preorder α] [CanonicallyOrderedAdd α] : IsOrderedAddMonoid α

@[implicit_reducible]

instance CanonicallyOrderedCommMonoid.toUniqueUnits {α : Type u} [Monoid α] [PartialOrder α] [CanonicallyOrderedMul α] : Unique αˣ

Equations

• CanonicallyOrderedCommMonoid.toUniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

@[implicit_reducible]

instance CanonicallyOrderedCommMonoid.toUniqueAddUnits {α : Type u} [AddMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] : Unique (AddUnits α)

Equations

• CanonicallyOrderedCommMonoid.toUniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }

@[simp]

theorem one_lt_mul_iff {α : Type u} [CommMonoid α] [PartialOrder α] [CanonicallyOrderedMul α] {a b : α} : 1 < a * b ↔ 1 < a ∨ 1 < b

@[simp]

theorem add_pos_iff {α : Type u} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} : 0 < a + b ↔ 0 < a ∨ 0 < b

theorem min_mul_distrib {α : Type u} [Monoid α] [LinearOrder α] [CanonicallyOrderedMul α] (a b c : α) : min a (b * c) = min a (min a b * min a c)

theorem min_add_distrib {α : Type u} [AddMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (a b c : α) : min a (b + c) = min a (min a b + min a c)

theorem min_mul_distrib' {α : Type u} [Monoid α] [LinearOrder α] [CanonicallyOrderedMul α] (a b c : α) : min (a * b) c = min (min a c * min b c) c

theorem min_add_distrib' {α : Type u} [AddMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (a b c : α) : min (a + b) c = min (min a c + min b c) c

@[simp]

theorem bot_eq_one' {α : Type u} [Monoid α] [LinearOrder α] [CanonicallyOrderedMul α] [OrderBot α] : ⊥ = 1

In a linearly ordered monoid, we are happy for bot_eq_one to be a @[simp] lemma.

@[simp]

theorem bot_eq_zero' {α : Type u} [AddMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [OrderBot α] : ⊥ = 0

In a linearly ordered monoid, we are happy for bot_eq_zero to be a @[simp] lemma