[Merged by Bors] - feat(algebra/module/ordered): redefine ordered_module as ordered_smul

src/algebra/module/ordered.lean

@@ -43,14 +43,14 @@ with a partial order in which the scalar multiplication is compatible with the o
 -/
 @[protect_proj]
 class ordered_module (R M : Type*)
-  [ordered_semiring R] [ordered_add_comm_monoid M] [module R M] : Prop :=
+  [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero 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]
+  [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero 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
@@ -77,7 +77,7 @@ 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
+calc 0 < c • a ↔ c • 0 < c • a : by rw smul_zero'
            ... ↔ 0 < a         : smul_lt_smul_iff_of_pos hc
 
 end ordered_module
@@ -87,7 +87,7 @@ end ordered_module
 `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)
+  [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_module R M :=
 begin
@@ -106,28 +106,30 @@ 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) :
+  [mul_action_with_zero 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] :
+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 }
 
 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]
+  [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_module k M]
+  [ordered_add_comm_group N] [smul_with_zero 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⟩
 
-lemma smul_le_smul_iff_of_neg (hc : c < 0) : c • a ≤ c • b ↔ b ≤ a :=
+lemma smul_le_smul_iff_of_neg {k M : Type*} [linear_ordered_field k]
+  [ordered_add_comm_group M] [module k M] [ordered_module k M]
+  {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,
@@ -145,12 +147,16 @@ 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_module {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] :
+  ordered_module k (M × N) :=
+ordered_module.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)] :
+  [Π i, mul_action_with_zero k (M i)] [∀ i, ordered_module k (M i)] :
   ordered_module k (Π i : ι, M i) :=
 begin
   refine (ordered_module.mk' $ λ v u c h hc i, _),
@@ -161,34 +167,45 @@ 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] :
+  [mul_action_with_zero k M] [ordered_module k M] :
   ordered_module k (ι → M) :=
 pi.ordered_module
 
 end field
 
 
-section order_dual
+namespace 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 [has_scalar R M] : has_scalar R (order_dual M) :=
+{ smul := λ k x, order_dual.rec (λ x', (k • x' : M)) x }
+
+instance [semiring R] [ordered_add_comm_monoid M] [h : smul_with_zero R M] :
+  smul_with_zero R (order_dual M) :=
+{ zero_smul := λ m, order_dual.rec (zero_smul _) m,
+  smul_zero := λ r, order_dual.rec (smul_zero' _) r,
+  ..order_dual.has_scalar }
+
+instance [semiring R] [mul_action R M] : mul_action R (order_dual M) :=
+{ one_smul := λ m, order_dual.rec (one_smul _) m,
+  mul_smul := λ r, order_dual.rec mul_smul r,
+  ..order_dual.has_scalar }
 
-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] [mul_action_with_zero R M] :
+  mul_action_with_zero R (order_dual M) :=
+{ ..order_dual.mul_action, ..order_dual.smul_with_zero }
 
-instance [semiring R] [ordered_add_comm_monoid M] [module R M] :
+instance [semiring R] [ordered_add_comm_monoid M] [distrib_mul_action 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 _ _ _ }
+{ smul_add := λ k a, order_dual.rec (λ a' b, order_dual.rec (smul_add _ _) b) a,
+  smul_zero := λ r, order_dual.rec smul_zero r }
 
 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 _ _ _ }
+{ add_smul := λ r s x, order_dual.rec (add_smul _ _) x,
+  zero_smul := λ m, order_dual.rec (zero_smul _) m }
 
-instance [ordered_semiring R] [ordered_add_comm_monoid M] [module R M]
+instance [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero 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,

src/linear_algebra/affine_space/ordered.lean

@@ -275,11 +275,16 @@ local notation `c` := line_map a b r
 segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f a b`. -/
 lemma map_le_line_map_iff_slope_le_slope_left (h : 0 < r * (b - a)) :
   f c ≤ line_map (f a) (f b) r ↔ slope f a c ≤ slope f a b :=
-by simp_rw [line_map_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul, add_sub_cancel, smul_sub,
-  sub_le_iff_le_add, mul_inv_rev', mul_smul, ← smul_sub, ← smul_add, smul_smul, ← mul_inv_rev',
-  smul_le_iff_of_pos (inv_pos.2 h), inv_inv', smul_smul,
+begin
+  rw [line_map_apply, line_map_apply, slope, slope,
+  vsub_eq_sub, vsub_eq_sub, vsub_eq_sub, vadd_eq_add, vadd_eq_add,
+  smul_eq_mul, add_sub_cancel, smul_sub, smul_sub, smul_sub,
+  sub_le_iff_le_add, mul_inv_rev', mul_smul, mul_smul, ←smul_sub, ←smul_sub, ←smul_add, smul_smul,
+  ← mul_inv_rev', smul_le_iff_of_pos (inv_pos.2 h), inv_inv', smul_smul,
   mul_inv_cancel_right' (right_ne_zero_of_mul h.ne'), smul_add,
-  smul_inv_smul' (left_ne_zero_of_mul h.ne')]
+  smul_inv_smul' (left_ne_zero_of_mul h.ne')],
+  apply_instance
+end
 
 /-- Given `c = line_map a b r`, `a < c`, the point `(c, f c)` is non-strictly above the
 segment `[(a, f a), (b, f b)]` if and only if `slope f a b ≤ slope f a c`. -/