feat(algebra/module/ordered): redefine ordered_module as `ordered_s…

…mul` (#8930)

One would like to talk about `ordered_monoid R (with_top R)`, but the `module` constraint is too strict to allow this.

The definition of `ordered_monoid` works if it is loosened to `has_scalar R M`. Most of the proofs that are part of its API need at most `smul_with_zero`. So it has been loosened to `smul_with_zero`, since a lawless `ordered_monoid` wouldn't do much.

In the `ordered_field` portion, `module` has been loosened to `mul_action_with_zero`.

`order_dual` instances of `smul` instances have also been generalized to better transmit. There are more generalizations possible, but seem out of scope for a single PR.

Unfortunately, these generalizations exposed a gnarly misalignment between `prod.has_lt` and `prod.has_le`, which have incompatible definitions, when inferred through separate paths. In particular, the `lt` definition of generated by `prod.preorder` is different than the core `prod.has_lt`. Due to this, the `prod.ordered_monoid` instance has not been generalized.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/algebra/algebra/ordered.lean

@@ -21,7 +21,7 @@ i.e. `A ≤ B` iff `B - A = star R * R` for some `R`.
 ## Implementation
 
 Because the axioms for an ordered algebra are exactly the same as those for the underlying
-module being ordered, we don't actually introduce a new class, but just use the `ordered_module`
+module being ordered, we don't actually introduce a new class, but just use the `ordered_smul`
 mixin.
 
 ## Tags
@@ -33,7 +33,7 @@ section ordered_algebra
 
 variables {R A : Type*} {a b : A} {r : R}
 
-variables [ordered_comm_ring R] [ordered_ring A] [algebra R A] [ordered_module R A]
+variables [ordered_comm_ring R] [ordered_ring A] [algebra R A] [ordered_smul R A]
 
 lemma algebra_map_monotone : monotone (algebra_map R A) :=
 λ a b h,
@@ -50,7 +50,7 @@ section instances
 
 variables {R : Type*} [linear_ordered_comm_ring R]
 
-instance linear_ordered_comm_ring.to_ordered_module : ordered_module R R :=
+instance linear_ordered_comm_ring.to_ordered_smul : ordered_smul R R :=
 { smul_lt_smul_of_pos       := ordered_semiring.mul_lt_mul_of_pos_left,
   lt_of_smul_lt_smul_of_pos := λ a b c w₁ w₂, (mul_lt_mul_left w₂).mp w₁ }
 

src/algebra/module/ordered.lean

@@ -5,194 +5,65 @@ Authors: Frédéric Dupuis
 -/
 
 import algebra.module.pi
-import algebra.ordered_pi
+import algebra.ordered_smul
 import algebra.module.prod
 import algebra.ordered_field
 
 /-!
-# Ordered modules
+# Ordered module
 
-In this file we define
-
-* `ordered_module R M` : an ordered additive commutative monoid `M` is an `ordered_module`
-  over an `ordered_semiring` `R` if the scalar product respects the order relation on the
-  monoid and on the ring. There is a correspondence between this structure and convex cones,
-  which is proven in `analysis/convex/cone.lean`.
-
-## Implementation notes
-
-* We choose to define `ordered_module` as a `Prop`-valued mixin, so that it can be
-  used for both modules and algebras
-  (the axioms for an "ordered algebra" are exactly that the algebra is ordered as a module).
-* To get ordered modules and ordered vector spaces, it suffices to replace the
-  `order_add_comm_monoid` and the `ordered_semiring` as desired.
+In this file we provide lemmas about `ordered_smul` that hold once a module structure is present.
 
 ## References
 
 * https://en.wikipedia.org/wiki/Ordered_module
 
 ## Tags
 
-ordered module, ordered module, ordered vector space
--/
-
-
-/--
-An ordered module is an ordered additive commutative monoid
-with a partial order in which the scalar multiplication is compatible with the order.
+ordered module, ordered scalar, ordered smul, ordered action, ordered vector space
 -/
-@[protect_proj]
-class ordered_module (R M : Type*)
-  [ordered_semiring R] [ordered_add_comm_monoid M] [module R M] : Prop :=
-(smul_lt_smul_of_pos : ∀ {a b : M}, ∀ {c : R}, a < b → 0 < c → c • a < c • b)
-(lt_of_smul_lt_smul_of_pos : ∀ {a b : M}, ∀ {c : R}, c • a < c • b → 0 < c → a < b)
-
-section ordered_module
-
-variables {R M : Type*}
-  [ordered_semiring R] [ordered_add_comm_monoid M] [module R M] [ordered_module R M]
-  {a b : M} {c : R}
-
-lemma smul_lt_smul_of_pos : a < b → 0 < c → c • a < c • b := ordered_module.smul_lt_smul_of_pos
-
-lemma smul_le_smul_of_nonneg (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c • a ≤ c • b :=
-begin
-  by_cases H₁ : c = 0,
-  { simp [H₁, zero_smul] },
-  { by_cases H₂ : a = b,
-    { rw H₂ },
-    { exact le_of_lt
-        (smul_lt_smul_of_pos (lt_of_le_of_ne h₁ H₂) (lt_of_le_of_ne h₂ (ne.symm H₁))), } }
-end
-
-lemma eq_of_smul_eq_smul_of_pos_of_le (h₁ : c • a = c • b) (hc : 0 < c) (hle : a ≤ b) :
-  a = b :=
-hle.lt_or_eq.resolve_left $ λ hlt, (smul_lt_smul_of_pos hlt hc).ne h₁
-
-lemma lt_of_smul_lt_smul_of_nonneg (h : c • a < c • b) (hc : 0 ≤ c) : a < b :=
-hc.eq_or_lt.elim (λ hc, false.elim $ lt_irrefl (0:M) $ by rwa [← hc, zero_smul, zero_smul] at h)
-  (ordered_module.lt_of_smul_lt_smul_of_pos h)
-
-lemma smul_lt_smul_iff_of_pos (hc : 0 < c) : c • a < c • b ↔ a < b :=
-⟨λ h, lt_of_smul_lt_smul_of_nonneg h hc.le, λ h, smul_lt_smul_of_pos h hc⟩
-
-lemma smul_pos_iff_of_pos (hc : 0 < c) : 0 < c • a ↔ 0 < a :=
-calc 0 < c • a ↔ c • 0 < c • a : by rw smul_zero
-           ... ↔ 0 < a         : smul_lt_smul_iff_of_pos hc
 
-end ordered_module
-
-/-- If `R` is a linear ordered semifield, then it suffices to verify only the first axiom of
-`ordered_module`. Moreover, it suffices to verify that `a < b` and `0 < c` imply
-`c • a ≤ c • b`. We have no semifields in `mathlib`, so we use the assumption `∀ c ≠ 0, is_unit c`
-instead. -/
-lemma ordered_module.mk'' {R M : Type*} [linear_ordered_semiring R] [ordered_add_comm_monoid M]
-  [module R M] (hR : ∀ {c : R}, c ≠ 0 → is_unit c)
-  (hlt : ∀ ⦃a b : M⦄ ⦃c : R⦄, a < b → 0 < c → c • a ≤ c • b) :
-  ordered_module R M :=
-begin
-  have hlt' : ∀ ⦃a b : M⦄ ⦃c : R⦄, a < b → 0 < c → c • a < c • b,
-  { refine λ a b c hab hc, (hlt hab hc).lt_of_ne _,
-    rw [ne.def, (hR hc.ne').smul_left_cancel],
-    exact hab.ne },
-  refine { smul_lt_smul_of_pos := hlt', .. },
-  intros a b c h hc,
-  rcases (hR hc.ne') with ⟨c, rfl⟩,
-  rw [← inv_smul_smul c a, ← inv_smul_smul c b],
-  refine hlt' h (pos_of_mul_pos_left _ hc.le),
-  simp only [c.mul_inv, zero_lt_one]
-end
-
-/-- If `R` is a linear ordered field, then it suffices to verify only the first axiom of
-`ordered_module`. -/
-lemma ordered_module.mk' {k M : Type*} [linear_ordered_field k] [ordered_add_comm_monoid M]
-  [module k M] (hlt : ∀ ⦃a b : M⦄ ⦃c : k⦄, a < b → 0 < c → c • a ≤ c • b) :
-  ordered_module k M :=
-ordered_module.mk'' (λ c hc, is_unit.mk0 _ hc) hlt
-
-instance linear_ordered_semiring.to_ordered_module  {R : Type*} [linear_ordered_semiring R] :
-  ordered_module R R :=
-{ smul_lt_smul_of_pos        := ordered_semiring.mul_lt_mul_of_pos_left,
-  lt_of_smul_lt_smul_of_pos  := λ _ _ _ h hc, lt_of_mul_lt_mul_left h hc.le }
+variables {k M N : Type*}
 
 section field
 
-variables {k M N : Type*} [linear_ordered_field k]
-  [ordered_add_comm_group M] [module k M] [ordered_module k M]
-  [ordered_add_comm_group N] [module k N] [ordered_module k N]
-  {a b : M} {c : k}
-
-lemma smul_le_smul_iff_of_pos (hc : 0 < c) : c • a ≤ c • b ↔ a ≤ b :=
-⟨λ h, inv_smul_smul' hc.ne' a ▸ inv_smul_smul' hc.ne' b ▸
-  smul_le_smul_of_nonneg h (inv_nonneg.2 hc.le),
-  λ h, smul_le_smul_of_nonneg h hc.le⟩
+variables [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M]
+  [ordered_add_comm_group N] [module k N] [ordered_smul k N]
 
-lemma smul_le_smul_iff_of_neg (hc : c < 0) : c • a ≤ c • b ↔ b ≤ a :=
+lemma smul_le_smul_iff_of_neg
+  {a b : M} {c : k} (hc : c < 0) : c • a ≤ c • b ↔ b ≤ a :=
 begin
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff, smul_le_smul_iff_of_pos (neg_pos.2 hc)],
   apply_instance,
 end
 
-lemma smul_lt_iff_of_pos (hc : 0 < c) : c • a < b ↔ a < c⁻¹ • b :=
-calc c • a < b ↔ c • a < c • c⁻¹ • b : by rw [smul_inv_smul' hc.ne']
-... ↔ a < c⁻¹ • b : smul_lt_smul_iff_of_pos hc
-
-lemma smul_le_iff_of_pos (hc : 0 < c) : c • a ≤ b ↔ a ≤ c⁻¹ • b :=
-calc c • a ≤ b ↔ c • a ≤ c • c⁻¹ • b : by rw [smul_inv_smul' hc.ne']
-... ↔ a ≤ c⁻¹ • b : smul_le_smul_iff_of_pos hc
-
-lemma le_smul_iff_of_pos (hc : 0 < c) : a ≤ c • b ↔ c⁻¹ • a ≤ b :=
-calc a ≤ c • b ↔ c • c⁻¹ • a ≤ c • b : by rw [smul_inv_smul' hc.ne']
-... ↔ c⁻¹ • a ≤ b : smul_le_smul_iff_of_pos hc
-
-instance prod.ordered_module : ordered_module k (M × N) :=
-ordered_module.mk' $ λ v u c h hc,
+-- TODO: solve `prod.has_lt` and `prod.has_le` misalignment issue
+instance prod.ordered_smul : ordered_smul k (M × N) :=
+ordered_smul.mk' $ λ (v u : M × N) (c : k) h hc,
   ⟨smul_le_smul_of_nonneg h.1.1 hc.le, smul_le_smul_of_nonneg h.1.2 hc.le⟩
 
-instance pi.ordered_module {ι : Type*} {M : ι → Type*} [Π i, ordered_add_comm_group (M i)]
-  [Π i, module k (M i)] [∀ i, ordered_module k (M i)] :
-  ordered_module k (Π i : ι, M i) :=
+instance pi.ordered_smul {ι : Type*} {M : ι → Type*} [Π i, ordered_add_comm_group (M i)]
+  [Π i, mul_action_with_zero k (M i)] [∀ i, ordered_smul k (M i)] :
+  ordered_smul k (Π i : ι, M i) :=
 begin
-  refine (ordered_module.mk' $ λ v u c h hc i, _),
+  refine (ordered_smul.mk' $ λ v u c h hc i, _),
   change c • v i ≤ c • u i,
   exact smul_le_smul_of_nonneg (h.le i) hc.le,
 end
 
 -- Sometimes Lean fails to apply the dependent version to non-dependent functions,
 -- so we define another instance
-instance pi.ordered_module' {ι : Type*} {M : Type*} [ordered_add_comm_group M]
-  [module k M] [ordered_module k M] :
-  ordered_module k (ι → M) :=
-pi.ordered_module
+instance pi.ordered_smul' {ι : Type*} {M : Type*} [ordered_add_comm_group M]
+  [mul_action_with_zero k M] [ordered_smul k M] :
+  ordered_smul k (ι → M) :=
+pi.ordered_smul
 
 end field
 
+namespace order_dual
 
-section order_dual
-
-variables {R M : Type*}
-
-instance [semiring R] [ordered_add_comm_monoid M] [module R M] : has_scalar R (order_dual M) :=
-{ smul := @has_scalar.smul R M _ }
-
-instance [semiring R] [ordered_add_comm_monoid M] [module R M] : mul_action R (order_dual M) :=
-{ one_smul := @mul_action.one_smul R M _ _,
-  mul_smul := @mul_action.mul_smul R M _ _ }
-
-instance [semiring R] [ordered_add_comm_monoid M] [module R M] :
-  distrib_mul_action R (order_dual M) :=
-{ smul_add := @distrib_mul_action.smul_add R M _ _ _,
-  smul_zero := @distrib_mul_action.smul_zero R M _ _ _ }
-
-instance [semiring R] [ordered_add_comm_monoid M] [module R M] : module R (order_dual M) :=
-{ add_smul := @module.add_smul R M _ _ _,
-  zero_smul := @module.zero_smul R M _ _ _ }
-
-instance [ordered_semiring R] [ordered_add_comm_monoid M] [module R M]
-  [ordered_module R M] :
-  ordered_module R (order_dual M) :=
-{ smul_lt_smul_of_pos := λ a b, @ordered_module.smul_lt_smul_of_pos R M _ _ _ _ b a,
-  lt_of_smul_lt_smul_of_pos := λ a b,
-    @ordered_module.lt_of_smul_lt_smul_of_pos R M _ _ _ _ b a }
+instance [semiring k] [ordered_add_comm_monoid M] [module k M] : module k (order_dual M) :=
+{ add_smul := λ r s x, order_dual.rec (add_smul _ _) x,
+  zero_smul := λ m, order_dual.rec (zero_smul _) m }
 
 end order_dual