feat(algebra/ordered_monoid): linear_ordered_add_comm_monoid(_with_top) (#6520)

Separates out classes for `linear_ordered_(add_)comm_monoid`
Creates `linear_ordered_add_comm_monoid_with_top`, an additive and order-reversed version of `linear_ordered_comm_monoid_with_zero`.
Puts an instance of `linear_ordered_add_comm_monoid_with_top` on `with_top` of any `linear_ordered_add_comm_monoid` and also on `enat`



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: awainverse

src/algebra/group/type_tags.lean

@@ -65,6 +65,12 @@ end multiplicative
 instance [inhabited α] : inhabited (additive α) := ⟨additive.of_mul (default α)⟩
 instance [inhabited α] : inhabited (multiplicative α) := ⟨multiplicative.of_add (default α)⟩
 
+instance [nontrivial α] : nontrivial (additive α) :=
+additive.of_mul.injective.nontrivial
+
+instance [nontrivial α] : nontrivial (multiplicative α) :=
+multiplicative.of_add.injective.nontrivial
+
 instance additive.has_add [has_mul α] : has_add (additive α) :=
 { add := λ x y, additive.of_mul (x.to_mul * y.to_mul) }
 

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -35,6 +35,15 @@ class linear_ordered_comm_group_with_zero (α : Type*)
 variables {α : Type*}
 variables {a b c d x y z : α}
 
+instance [linear_ordered_add_comm_monoid_with_top α] :
+  linear_ordered_comm_monoid_with_zero (multiplicative (order_dual α)) :=
+{ zero := multiplicative.of_add (⊤ : α),
+  zero_mul := top_add,
+  mul_zero := add_top,
+  zero_le_one := (le_top : (0 : α) ≤ ⊤),
+  ..multiplicative.ordered_comm_monoid,
+  ..multiplicative.linear_order }
+
 section linear_ordered_comm_monoid
 
 variables [linear_ordered_comm_monoid_with_zero α]
@@ -123,6 +132,13 @@ lemma zero_lt_iff : 0 < a ↔ a ≠ 0 :=
 lemma ne_zero_of_lt (h : b < a) : a ≠ 0 :=
 λ h1, not_lt_zero' $ show b < 0, from h1 ▸ h
 
+instance : linear_ordered_add_comm_monoid_with_top (additive (order_dual α)) :=
+{ top := (0 : α),
+  top_add' := λ a, (zero_mul a : (0 : α) * a = 0),
+  le_top := λ _, zero_le',
+  ..additive.ordered_add_comm_monoid,
+  ..additive.linear_order }
+
 end linear_ordered_comm_monoid
 
 variables [linear_ordered_comm_group_with_zero α]

src/algebra/module/submodule.lean

@@ -209,6 +209,12 @@ instance to_ordered_add_comm_monoid
   ordered_add_comm_monoid S :=
 subtype.coe_injective.ordered_add_comm_monoid coe rfl (λ _ _, rfl)
 
+/-- A submodule of a `linear_ordered_add_comm_monoid` is a `linear_ordered_add_comm_monoid`. -/
+instance to_linear_ordered_add_comm_monoid
+  {M} [linear_ordered_add_comm_monoid M] [semimodule R M] (S : submodule R M) :
+  linear_ordered_add_comm_monoid S :=
+subtype.coe_injective.linear_ordered_add_comm_monoid coe rfl (λ _ _, rfl)
+
 /-- A submodule of an `ordered_cancel_add_comm_monoid` is an `ordered_cancel_add_comm_monoid`. -/
 instance to_ordered_cancel_add_comm_monoid
   {M} [ordered_cancel_add_comm_monoid M] [semimodule R M] (S : submodule R M) :

src/algebra/ordered_group.lean

@@ -942,4 +942,12 @@ instance [ordered_comm_group α] : ordered_add_comm_group (additive α) :=
 { ..additive.add_comm_group,
   ..additive.ordered_add_comm_monoid }
 
+instance [linear_ordered_add_comm_group α] : linear_ordered_comm_group (multiplicative α) :=
+{ ..multiplicative.linear_order,
+  ..multiplicative.ordered_comm_group }
+
+instance [linear_ordered_comm_group α] : linear_ordered_add_comm_group (additive α) :=
+{ ..additive.linear_order,
+  ..additive.ordered_add_comm_group }
+
 end type_tags

src/algebra/ordered_monoid.lean

@@ -49,10 +49,24 @@ class ordered_add_comm_monoid (α : Type*) extends add_comm_monoid α, partial_o
 
 attribute [to_additive] ordered_comm_monoid
 
-/-- A linearly ordered commutative monoid with a zero element. -/
-class linear_ordered_comm_monoid_with_zero (α : Type*)
-  extends linear_order α, comm_monoid_with_zero α, ordered_comm_monoid α :=
-(zero_le_one : (0:α) ≤ 1)
+/-- A linearly ordered additive commutative monoid. -/
+@[protect_proj, ancestor linear_order ordered_add_comm_monoid]
+class linear_ordered_add_comm_monoid (α : Type*)
+  extends linear_order α, ordered_add_comm_monoid α :=
+(lt_of_add_lt_add_left := λ x y z, by {
+  apply imp_of_not_imp_not,
+  intro h,
+  apply not_lt_of_le,
+  apply add_le_add_left,
+  -- type-class inference uses `a : linear_order α` which it can't unfold, unless we provide this!
+  -- `lt_iff_le_not_le` gets filled incorrectly with `autoparam` if we don't provide that field.
+  letI : linear_order α := by refine { le := le, lt := lt, lt_iff_le_not_le := _, .. }; assumption,
+  exact le_of_not_lt h })
+
+/-- A linearly ordered commutative monoid. -/
+@[protect_proj, ancestor linear_order ordered_comm_monoid, to_additive]
+class linear_ordered_comm_monoid (α : Type*)
+  extends linear_order α, ordered_comm_monoid α :=
 (lt_of_mul_lt_mul_left := λ x y z, by {
   apply imp_of_not_imp_not,
   intro h,
@@ -63,6 +77,29 @@ class linear_ordered_comm_monoid_with_zero (α : Type*)
   letI : linear_order α := by refine { le := le, lt := lt, lt_iff_le_not_le := _, .. }; assumption,
   exact le_of_not_lt h })
 
+/-- A linearly ordered commutative monoid with a zero element. -/
+class linear_ordered_comm_monoid_with_zero (α : Type*)
+  extends linear_ordered_comm_monoid α, comm_monoid_with_zero α :=
+(zero_le_one : (0 : α) ≤ 1)
+
+/-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
+  Instances should include number systems with an infinite element adjoined.` -/
+@[protect_proj, ancestor linear_ordered_add_comm_monoid order_top]
+class linear_ordered_add_comm_monoid_with_top (α : Type*)
+  extends linear_ordered_add_comm_monoid α, order_top α :=
+(top_add' : ∀ x : α, ⊤ + x = ⊤)
+
+section linear_ordered_add_comm_monoid_with_top
+variables [linear_ordered_add_comm_monoid_with_top α] {a b : α}
+
+@[simp]
+lemma top_add (a : α) : ⊤ + a = ⊤ := linear_ordered_add_comm_monoid_with_top.top_add' a
+
+@[simp]
+lemma add_top (a : α) : a + ⊤ = ⊤ :=
+by rw [add_comm, top_add]
+
+end linear_ordered_add_comm_monoid_with_top
 
 section ordered_comm_monoid
 variables [ordered_comm_monoid α] {a b c d : α}
@@ -299,6 +336,17 @@ end mono
 
 end ordered_comm_monoid
 
+/-- Pullback a `linear_ordered_comm_monoid` under an injective map. -/
+@[to_additive function.injective.linear_ordered_add_comm_monoid
+"Pullback an `ordered_add_comm_monoid` under an injective map."]
+def function.injective.linear_ordered_comm_monoid [linear_ordered_comm_monoid α] {β : Type*}
+  [has_one β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y) :
+  linear_ordered_comm_monoid β :=
+{ .. hf.ordered_comm_monoid f one mul,
+  .. linear_order.lift f hf }
+
 lemma bit0_pos [ordered_add_comm_monoid α] {a : α} (h : 0 < a) : 0 < bit0 a :=
 add_pos h h
 
@@ -552,6 +600,14 @@ instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
     end,
   ..with_top.partial_order, ..with_top.add_comm_monoid }
 
+instance [linear_ordered_add_comm_monoid α] :
+  linear_ordered_add_comm_monoid_with_top (with_top α) :=
+{ top_add' := λ x, with_top.top_add,
+  ..with_top.order_top,
+  ..with_top.linear_order,
+  ..with_top.ordered_add_comm_monoid,
+  ..option.nontrivial }
+
 /-- Coercion from `α` to `with_top α` as an `add_monoid_hom`. -/
 def coe_add_hom [add_monoid α] : α →+ with_top α :=
 ⟨coe, rfl, λ _ _, rfl⟩
@@ -1076,16 +1132,16 @@ fn_min_mul_fn_max id n m
 /-- A linearly ordered cancellative additive commutative monoid
 is an additive commutative monoid with a decidable linear order
 in which addition is cancellative and monotone. -/
-@[protect_proj, ancestor ordered_cancel_add_comm_monoid linear_order]
+@[protect_proj, ancestor ordered_cancel_add_comm_monoid linear_ordered_add_comm_monoid]
 class linear_ordered_cancel_add_comm_monoid (α : Type u)
-  extends ordered_cancel_add_comm_monoid α, linear_order α
+  extends ordered_cancel_add_comm_monoid α, linear_ordered_add_comm_monoid α
 
 /-- A linearly ordered cancellative commutative monoid
 is a commutative monoid with a linear order
 in which multiplication is cancellative and monotone. -/
-@[protect_proj, ancestor ordered_cancel_comm_monoid linear_order, to_additive]
+@[protect_proj, ancestor ordered_cancel_comm_monoid linear_ordered_comm_monoid, to_additive]
 class linear_ordered_cancel_comm_monoid (α : Type u)
-  extends ordered_cancel_comm_monoid α, linear_order α
+  extends ordered_cancel_comm_monoid α, linear_ordered_comm_monoid α
 
 section linear_ordered_cancel_comm_monoid
 
@@ -1126,7 +1182,7 @@ def function.injective.linear_ordered_cancel_comm_monoid {β : Type*}
   (f : β → α) (hf : function.injective f) (one : f 1 = 1)
   (mul : ∀ x y, f (x * y) = f x * f y) :
   linear_ordered_cancel_comm_monoid β :=
-{ ..linear_order.lift f hf,
+{ ..hf.linear_ordered_comm_monoid f one mul,
   ..hf.ordered_cancel_comm_monoid f one mul }
 
 end linear_ordered_cancel_comm_monoid
@@ -1203,4 +1259,12 @@ instance [ordered_cancel_comm_monoid α] : ordered_cancel_add_comm_monoid (addit
   ..additive.add_left_cancel_semigroup,
   ..additive.ordered_add_comm_monoid }
 
+instance [linear_ordered_add_comm_monoid α] : linear_ordered_comm_monoid (multiplicative α) :=
+{ ..multiplicative.linear_order,
+  ..multiplicative.ordered_comm_monoid }
+
+instance [linear_ordered_comm_monoid α] : linear_ordered_add_comm_monoid (additive α) :=
+{ ..additive.linear_order,
+  ..additive.ordered_add_comm_monoid }
+
 end type_tags

src/data/nat/enat.lean

@@ -493,4 +493,10 @@ lemma find_eq_top_iff : find P = ⊤ ↔ ∀ n, ¬P n :=
 
 end find
 
+noncomputable instance : linear_ordered_add_comm_monoid_with_top enat :=
+{ top_add' := top_add,
+  .. enat.linear_order,
+  .. enat.ordered_add_comm_monoid,
+  .. enat.order_top }
+
 end enat

src/group_theory/submonoid/operations.lean

@@ -332,13 +332,20 @@ an `add_comm_monoid`."]
 instance to_comm_monoid {M} [comm_monoid M] (S : submonoid M) : comm_monoid S :=
 S.coe_injective.comm_monoid coe rfl (λ _ _, rfl)
 
-/-- A submonoid of a `ordered_comm_monoid` is a `ordered_comm_monoid`. -/
+/-- A submonoid of an `ordered_comm_monoid` is an `ordered_comm_monoid`. -/
 @[to_additive "An `add_submonoid` of an `ordered_add_comm_monoid` is
 an `ordered_add_comm_monoid`."]
 instance to_ordered_comm_monoid {M} [ordered_comm_monoid M] (S : submonoid M) :
   ordered_comm_monoid S :=
 S.coe_injective.ordered_comm_monoid coe rfl (λ _ _, rfl)
 
+/-- A submonoid of a `linear_ordered_comm_monoid` is a `linear_ordered_comm_monoid`. -/
+@[to_additive "An `add_submonoid` of a `linear_ordered_add_comm_monoid` is
+a `linear_ordered_add_comm_monoid`."]
+instance to_linear_ordered_comm_monoid {M} [linear_ordered_comm_monoid M] (S : submonoid M) :
+  linear_ordered_comm_monoid S :=
+S.coe_injective.linear_ordered_comm_monoid coe rfl (λ _ _, rfl)
+
 /-- A submonoid of an `ordered_cancel_comm_monoid` is an `ordered_cancel_comm_monoid`. -/
 @[to_additive "An `add_submonoid` of an `ordered_cancel_add_comm_monoid` is
 an `ordered_cancel_add_comm_monoid`."]