chore(algebra/order/{module, smul}): Move to the correct spot (#16131)

Make `algebra.order.module` do what it says on the tin. Namely, move everything that wasn't about `module` to `algebra.order.smul` and generalize accordingly.

As a bonus, add a shortcut instance for `ordered_smul 𝕜 (ι → 𝕜)` as this solves #16021.

src/algebra/order/module.lean

@@ -3,11 +3,7 @@ Copyright (c) 2020 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis, Yaël Dillies
 -/
-import algebra.module.pi
-import algebra.module.prod
-import algebra.order.pi
 import algebra.order.smul
-import data.set.pointwise
 
 /-!
 # Ordered module
@@ -27,14 +23,10 @@ open_locale pointwise
 
 variables {k M N : Type*}
 
-namespace order_dual
-
 instance [semiring k] [ordered_add_comm_monoid M] [module k M] : module k Mᵒᵈ :=
 { add_smul := λ r s x, order_dual.rec (add_smul _ _) x,
   zero_smul := λ m, order_dual.rec (zero_smul _) m }
 
-end order_dual
-
 section semiring
 variables [ordered_semiring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M]
   {a b : M} {c : k}
@@ -190,57 +182,10 @@ variables (M)
   right_inv := smul_inv_smul₀ hc.ne,
   map_rel_iff' := λ b₁ b₂, smul_le_smul_iff_of_neg hc }
 
-variables {M} [ordered_add_comm_group N] [module k N] [ordered_smul k N]
-
--- 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.smul_with_zero'' {ι : Type*} {M : ι → Type*} [Π i, ordered_add_comm_group (M i)]
-  [Π i, mul_action_with_zero k (M i)] :
-  smul_with_zero k (Π i : ι, M i) := by apply_instance
-
-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_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_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
 
 /-! ### Upper/lower bounds -/
 
-section ordered_semiring
-variables [ordered_semiring k] [ordered_add_comm_monoid M] [smul_with_zero k M] [ordered_smul k M]
-  {s : set M} {c : k}
-
-lemma smul_lower_bounds_subset_lower_bounds_smul (hc : 0 ≤ c) :
-  c • lower_bounds s ⊆ lower_bounds (c • s) :=
-(monotone_smul_left hc).image_lower_bounds_subset_lower_bounds_image
-
-lemma smul_upper_bounds_subset_upper_bounds_smul (hc : 0 ≤ c) :
-  c • upper_bounds s ⊆ upper_bounds (c • s) :=
-(monotone_smul_left hc).image_upper_bounds_subset_upper_bounds_image
-
-lemma bdd_below.smul_of_nonneg (hs : bdd_below s) (hc : 0 ≤ c) : bdd_below (c • s) :=
-(monotone_smul_left hc).map_bdd_below hs
-
-lemma bdd_above.smul_of_nonneg (hs : bdd_above s) (hc : 0 ≤ c) : bdd_above (c • s) :=
-(monotone_smul_left hc).map_bdd_above hs
-
-end ordered_semiring
-
 section ordered_ring
 variables [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M]
   {s : set M} {c : k}
@@ -262,27 +207,8 @@ lemma bdd_above.smul_of_nonpos (hc : c ≤ 0) (hs : bdd_above s) : bdd_below (c
 end ordered_ring
 
 section linear_ordered_field
-variables [linear_ordered_field k] [ordered_add_comm_group M]
-
-section mul_action_with_zero
-variables [mul_action_with_zero k M] [ordered_smul k M] {s t : set M} {c : k}
-
-@[simp] lemma lower_bounds_smul_of_pos (hc : 0 < c) : lower_bounds (c • s) = c • lower_bounds s :=
-(order_iso.smul_left _ hc).lower_bounds_image
-
-@[simp] lemma upper_bounds_smul_of_pos (hc : 0 < c) : upper_bounds (c • s) = c • upper_bounds s :=
-(order_iso.smul_left _ hc).upper_bounds_image
-
-@[simp] lemma bdd_below_smul_iff_of_pos (hc : 0 < c) : bdd_below (c • s) ↔ bdd_below s :=
-(order_iso.smul_left _ hc).bdd_below_image
-
-@[simp] lemma bdd_above_smul_iff_of_pos (hc : 0 < c) : bdd_above (c • s) ↔ bdd_above s :=
-(order_iso.smul_left _ hc).bdd_above_image
-
-end mul_action_with_zero
-
-section module
-variables [module k M] [ordered_smul k M] {s t : set M} {c : k}
+variables [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M]
+  {s : set M} {c : k}
 
 @[simp] lemma lower_bounds_smul_of_neg (hc : c < 0) : lower_bounds (c • s) = c • upper_bounds s :=
 (order_iso.smul_left_dual M hc).upper_bounds_image
@@ -296,5 +222,4 @@ variables [module k M] [ordered_smul k M] {s t : set M} {c : k}
 @[simp] lemma bdd_above_smul_iff_of_neg (hc : c < 0) : bdd_above (c • s) ↔ bdd_below s :=
 (order_iso.smul_left_dual M hc).bdd_below_image
 
-end module
 end linear_ordered_field

src/algebra/order/smul.lean

@@ -3,10 +3,11 @@ Copyright (c) 2020 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 -/
-
+import algebra.module.pi
+import algebra.module.prod
 import algebra.order.field
-import algebra.smul_with_zero
-import group_theory.group_action.group
+import algebra.order.pi
+import data.set.pointwise
 
 /-!
 # Ordered scalar product
@@ -35,6 +36,7 @@ In this file we define
 ordered module, ordered scalar, ordered smul, ordered action, ordered vector space
 -/
 
+open_locale pointwise
 
 /--
 The ordered scalar product property is when an ordered additive commutative monoid
@@ -46,9 +48,9 @@ class ordered_smul (R M : Type*)
 (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)
 
-namespace order_dual
+variables {ι 𝕜 R M N : Type*}
 
-variables {R M : Type*}
+namespace order_dual
 
 instance [has_zero R] [add_zero_class M] [h : smul_with_zero R M] : smul_with_zero R Mᵒᵈ :=
 { zero_smul := λ m, order_dual.rec (zero_smul _) m,
@@ -79,10 +81,8 @@ instance [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M]
 end order_dual
 
 section ordered_smul
-
-variables {R M : Type*}
-  [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M]
-  {a b : M} {c : R}
+variables [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M]
+  {s : set M} {a b : M} {c : R}
 
 lemma smul_lt_smul_of_pos : a < b → 0 < c → c • a < c • b := ordered_smul.smul_lt_smul_of_pos
 
@@ -125,46 +125,72 @@ lemma monotone_smul_left (hc : 0 ≤ c) : monotone (has_smul.smul c : M → M) :
 lemma strict_mono_smul_left (hc : 0 < c) : strict_mono (has_smul.smul c : M → M) :=
 λ a b h, smul_lt_smul_of_pos h hc
 
+lemma smul_lower_bounds_subset_lower_bounds_smul (hc : 0 ≤ c) :
+  c • lower_bounds s ⊆ lower_bounds (c • s) :=
+(monotone_smul_left hc).image_lower_bounds_subset_lower_bounds_image
+
+lemma smul_upper_bounds_subset_upper_bounds_smul (hc : 0 ≤ c) :
+  c • upper_bounds s ⊆ upper_bounds (c • s) :=
+(monotone_smul_left hc).image_upper_bounds_subset_upper_bounds_image
+
+lemma bdd_below.smul_of_nonneg (hs : bdd_below s) (hc : 0 ≤ c) : bdd_below (c • s) :=
+(monotone_smul_left hc).map_bdd_below hs
+
+lemma bdd_above.smul_of_nonneg (hs : bdd_above s) (hc : 0 ≤ c) : bdd_above (c • s) :=
+(monotone_smul_left hc).map_bdd_above hs
+
 end ordered_smul
 
-/-- If `R` is a linear ordered semifield, then it suffices to verify only the first axiom of
-`ordered_smul`. 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_smul.mk'' {R M : Type*} [linear_ordered_semiring R] [ordered_add_comm_monoid M]
-  [mul_action_with_zero 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_smul R M :=
+instance linear_ordered_semiring.to_ordered_smul {R : Type*} [linear_ordered_semiring R] :
+  ordered_smul 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 }
+
+section linear_ordered_semifield
+variables [linear_ordered_semifield 𝕜]
+
+section ordered_add_comm_monoid
+variables [ordered_add_comm_monoid M] [ordered_add_comm_monoid N] [mul_action_with_zero 𝕜 M]
+  [mul_action_with_zero 𝕜 N]
+
+/-- To prove that a vector space over a linear ordered field is ordered, it suffices to verify only
+the first axiom of `ordered_smul`. -/
+lemma ordered_smul.mk' (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) :
+  ordered_smul 𝕜 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],
+  have hlt' : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a < c • b,
+  { refine λ a b c hab hc, (h hab hc).lt_of_ne _,
+    rw [ne.def, hc.ne'.is_unit.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⟩,
+  intros a b c hab hc,
+  obtain ⟨c, rfl⟩ := hc.ne'.is_unit,
   rw [← inv_smul_smul c a, ← inv_smul_smul c b],
-  refine hlt' h (pos_of_mul_pos_right _ hc.le),
+  refine hlt' hab (pos_of_mul_pos_right _ 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_smul`. -/
-lemma ordered_smul.mk' {k M : Type*} [linear_ordered_field k] [ordered_add_comm_monoid M]
-  [mul_action_with_zero k M] (hlt : ∀ ⦃a b : M⦄ ⦃c : k⦄, a < b → 0 < c → c • a ≤ c • b) :
-  ordered_smul k M :=
-ordered_smul.mk'' (λ c hc, is_unit.mk0 _ hc) hlt
+instance [ordered_smul 𝕜 M] [ordered_smul 𝕜 N] : ordered_smul 𝕜 (M × N) :=
+ordered_smul.mk' $ λ a b c h hc,
+  ⟨smul_le_smul_of_nonneg h.1.1 hc.le, smul_le_smul_of_nonneg h.1.2 hc.le⟩
 
-instance linear_ordered_semiring.to_ordered_smul {R : Type*} [linear_ordered_semiring R] :
-  ordered_smul 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 }
+instance pi.ordered_smul {M : ι → Type*} [Π i, ordered_add_comm_monoid (M i)]
+  [Π i, mul_action_with_zero 𝕜 (M i)] [∀ i, ordered_smul 𝕜 (M i)] :
+  ordered_smul 𝕜 (Π i, M i) :=
+ordered_smul.mk' $ λ v u c h hc i, smul_le_smul_of_nonneg (h.le i) hc.le
+
+/- Sometimes Lean fails to apply the dependent version to non-dependent functions, so we define
+another instance. -/
+instance pi.ordered_smul' [ordered_smul 𝕜 M] : ordered_smul 𝕜 (ι → M) := pi.ordered_smul
 
-section field
+/- Sometimes Lean fails to unify the module with the scalars, so we define another instance. -/
+instance pi.ordered_smul'' : ordered_smul 𝕜 (ι → 𝕜) := @pi.ordered_smul' ι 𝕜 𝕜 _ _ _ _
 
-variables {k M : Type*} [linear_ordered_field k]
-  [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M]
-  {a b : M} {c : k}
+end ordered_add_comm_monoid
+
+section ordered_add_comm_group
+variables [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {s : set M}
+  {a b : M} {c : 𝕜}
 
 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 ▸
@@ -190,11 +216,26 @@ calc a ≤ c • b ↔ c • c⁻¹ • a ≤ c • b : by rw [smul_inv_smul₀
 variables (M)
 
 /-- Left scalar multiplication as an order isomorphism. -/
-@[simps] def order_iso.smul_left {c : k} (hc : 0 < c) : M ≃o M :=
+@[simps] def order_iso.smul_left (hc : 0 < c) : M ≃o M :=
 { to_fun := λ b, c • b,
   inv_fun := λ b, c⁻¹ • b,
   left_inv := inv_smul_smul₀ hc.ne',
   right_inv := smul_inv_smul₀ hc.ne',
   map_rel_iff' := λ b₁ b₂, smul_le_smul_iff_of_pos hc }
 
-end field
+variables {M}
+
+@[simp] lemma lower_bounds_smul_of_pos (hc : 0 < c) : lower_bounds (c • s) = c • lower_bounds s :=
+(order_iso.smul_left _ hc).lower_bounds_image
+
+@[simp] lemma upper_bounds_smul_of_pos (hc : 0 < c) : upper_bounds (c • s) = c • upper_bounds s :=
+(order_iso.smul_left _ hc).upper_bounds_image
+
+@[simp] lemma bdd_below_smul_iff_of_pos (hc : 0 < c) : bdd_below (c • s) ↔ bdd_below s :=
+(order_iso.smul_left _ hc).bdd_below_image
+
+@[simp] lemma bdd_above_smul_iff_of_pos (hc : 0 < c) : bdd_above (c • s) ↔ bdd_above s :=
+(order_iso.smul_left _ hc).bdd_above_image
+
+end ordered_add_comm_group
+end linear_ordered_semifield