feat(linear_algebra/affine_space/ordered): define slope (#4669)

* Review API of `ordered_semimodule`:
  - replace `lt_of_smul_lt_smul_of_nonneg` with `lt_of_smul_lt_smul_of_pos`;
    it's equivalent but is easier to prove;
  - add more lemmas;
  - add a constructor for the special case of an ordered semimodule over
	a linearly ordered field; in this case it suffices to verify only
	`a < b → 0 < c → c • a ≤ c • b`;
  - use the new constructor in `analysis/convex/cone`;
* Define `units.smul_perm_hom`, reroute `mul_action.to_perm` through it;
* Add a few more lemmas unfolding `affine_map.line_map` in special cases;
* Define `slope f a b = (b - a)⁻¹ • (f b -ᵥ f a)` and prove a handful
  of monotonicity properties.

src/algebra/module/ordered.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 -/
 
-import algebra.module.basic
-import algebra.ordered_group
+import linear_algebra.basic
+import algebra.ordered_field
 
 /-!
 # Ordered semimodules
@@ -39,15 +39,15 @@ An ordered semimodule is an ordered additive commutative monoid
 with a partial order in which the scalar multiplication is compatible with the order.
 -/
 @[protect_proj, ancestor semimodule]
-class ordered_semimodule (R β : Type*)
-  [ordered_semiring R] [ordered_add_comm_monoid β] extends semimodule R β :=
-(smul_lt_smul_of_pos : ∀ {a b : β}, ∀ {c : R}, a < b → 0 < c → c • a < c • b)
-(lt_of_smul_lt_smul_of_nonneg : ∀ {a b : β}, ∀ {c : R}, c • a < c • b → 0 ≤ c → a < b)
+class ordered_semimodule (R M : Type*)
+  [ordered_semiring R] [ordered_add_comm_monoid M] extends semimodule R M :=
+(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_semimodule
 
-variables {R β : Type*} [ordered_semiring R] [ordered_add_comm_monoid β] [ordered_semimodule R β]
-  {a b : β} {c : R}
+variables {R M : Type*} [ordered_semiring R] [ordered_add_comm_monoid M] [ordered_semimodule R M]
+  {a b : M} {c : R}
 
 lemma smul_lt_smul_of_pos : a < b → 0 < c → c • a < c • b := ordered_semimodule.smul_lt_smul_of_pos
 
@@ -61,40 +61,111 @@ begin
         (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_semimodule.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_semimodule
 
-section instances
+/-- If `R` is a linear ordered semifield, then it suffices to verify only the first axiom of
+`ordered_semimodule`. 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. -/
+def ordered_semimodule.mk'' {R M : Type*} [linear_ordered_semiring R] [ordered_add_comm_monoid M]
+  [semimodule 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_semimodule 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', to_semimodule := ‹_›, .. },
+  intros a b c h hc,
+  rcases (hR hc.ne') with ⟨c, rfl⟩,
+  rw [← c.inv_smul_smul a, ← c.inv_smul_smul 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_semimodule`. -/
+def ordered_semimodule.mk' {k M : Type*} [linear_ordered_field k] [ordered_add_comm_monoid M]
+  [semimodule k M] (hlt : ∀ ⦃a b : M⦄ ⦃c : k⦄, a < b → 0 < c → c • a ≤ c • b) :
+  ordered_semimodule k M :=
+ordered_semimodule.mk'' (λ c hc, is_unit.mk0 _ hc) hlt
+
+instance linear_ordered_semiring.to_ordered_semimodule  {R : Type*} [linear_ordered_semiring R] :
+  ordered_semimodule 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]
+  [ordered_semimodule k M] [ordered_add_comm_group N] [ordered_semimodule 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 :=
+by rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff, smul_le_smul_iff_of_pos (neg_pos.2 hc)]
+
+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
 
-variables {R : Type*} [linear_ordered_ring R]
+instance prod.ordered_semimodule : ordered_semimodule k (M × N) :=
+ordered_semimodule.mk' $ λ v u 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_ring.to_ordered_semimodule : ordered_semimodule R R :=
-{ smul_lt_smul_of_pos      := ordered_semiring.mul_lt_mul_of_pos_left,
-  lt_of_smul_lt_smul_of_nonneg  := λ _ _ _, lt_of_mul_lt_mul_left }
+end field
 
-end instances
 
 section order_dual
 
-variables {R β : Type*}
+variables {R M : Type*}
 
-instance [semiring R] [ordered_add_comm_monoid β] [semimodule R β] : has_scalar R (order_dual β) :=
-{ smul := @has_scalar.smul R β _ }
+instance [semiring R] [ordered_add_comm_monoid M] [semimodule R M] : has_scalar R (order_dual M) :=
+{ smul := @has_scalar.smul R M _ }
 
-instance [semiring R] [ordered_add_comm_monoid β] [semimodule R β] : mul_action R (order_dual β) :=
-{ one_smul := @mul_action.one_smul R β _ _,
-  mul_smul := @mul_action.mul_smul R β _ _ }
+instance [semiring R] [ordered_add_comm_monoid M] [semimodule 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 β] [semimodule R β] : distrib_mul_action R (order_dual β) :=
-{ smul_add := @distrib_mul_action.smul_add R β _ _ _,
-  smul_zero := @distrib_mul_action.smul_zero R β _ _ _ }
+instance [semiring R] [ordered_add_comm_monoid M] [semimodule 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 β] [semimodule R β] : semimodule R (order_dual β) :=
-{ add_smul := @semimodule.add_smul R β _ _ _,
-  zero_smul := @semimodule.zero_smul R β _ _ _ }
+instance [semiring R] [ordered_add_comm_monoid M] [semimodule R M] : semimodule R (order_dual M) :=
+{ add_smul := @semimodule.add_smul R M _ _ _,
+  zero_smul := @semimodule.zero_smul R M _ _ _ }
 
-instance [ordered_semiring R] [ordered_add_comm_monoid β] [ordered_semimodule R β] :
-  ordered_semimodule R (order_dual β) :=
-{ smul_lt_smul_of_pos := λ a b, @ordered_semimodule.smul_lt_smul_of_pos R β _ _ _ b a,
-  lt_of_smul_lt_smul_of_nonneg := λ a b, @ordered_semimodule.lt_of_smul_lt_smul_of_nonneg R β _ _ _ b a }
+instance [ordered_semiring R] [ordered_add_comm_monoid M] [ordered_semimodule R M] :
+  ordered_semimodule R (order_dual M) :=
+{ smul_lt_smul_of_pos := λ a b, @ordered_semimodule.smul_lt_smul_of_pos R M _ _ _ b a,
+  lt_of_smul_lt_smul_of_pos := λ a b, @ordered_semimodule.lt_of_smul_lt_smul_of_pos R M _ _ _ b a }
 
 end order_dual

src/analysis/convex/cone.lean

@@ -189,44 +189,20 @@ ext' $ preimage_comp.symm
 @[simp] lemma mem_comap {f : E →ₗ[ℝ] F} {S : convex_cone F} {x : E} :
   x ∈ S.comap f ↔ f x ∈ S := iff.rfl
 
+-- We use `{ to_semimodule := ‹_›, .. }` to avoid making this definition noncomputable
 /--
 Constructs an ordered semimodule given an `ordered_add_comm_group`, a cone, and a proof that
 the order relation is the one defined by the cone.
 -/
 def to_ordered_semimodule {M : Type*} [ordered_add_comm_group M] [semimodule ℝ M]
   (S : convex_cone M) (h : ∀ x y : M, x ≤ y ↔ y - x ∈ S) : ordered_semimodule ℝ M :=
-{ smul_lt_smul_of_pos :=
+{ to_semimodule := ‹_›,
+  .. (show ordered_semimodule ℝ M, from ordered_semimodule.mk'
     begin
       intros x y z xy hz,
-      refine lt_of_le_of_ne _ _,
-      { rw [h (z • x) (z • y), ←smul_sub z y x],
-        exact smul_mem S hz ((h x y).mp (le_of_lt xy)) },
-      { intro H,
-        have H' := congr_arg (λ r, (1/z) • r) H,
-        refine (ne_of_lt xy) _,
-        field_simp [smul_smul, div_self ((ne_of_lt hz).symm)] at H',
-        exact H' },
-    end,
-  lt_of_smul_lt_smul_of_nonneg :=
-    begin
-      intros x y z hxy hz,
-      refine lt_of_le_of_ne _ _,
-      { rw [h x y],
-        have hz' : 0 < z,
-        { refine lt_of_le_of_ne hz _,
-          rintro rfl,
-          rw [zero_smul, zero_smul] at hxy,
-          exact lt_irrefl 0 hxy },
-        have hz'' : 0 < 1/z := div_pos (by linarith) hz',
-        have hxy' := (h (z • x) (z • y)).mp (le_of_lt hxy),
-        rw [←smul_sub z y x] at hxy',
-        have hxy'' := smul_mem S hz'' hxy',
-        field_simp [smul_smul, div_self ((ne_of_lt hz').symm)] at hxy'',
-        exact hxy'' },
-      { rintro rfl,
-        exact lt_irrefl (z • x) hxy }
-    end,
-}
+      rw [h (z • x) (z • y), ←smul_sub z y x],
+      exact smul_mem S hz ((h x y).mp (le_of_lt xy))
+    end) }
 
 /-! ### Convex cones with extra properties -/
 

src/group_theory/group_action.lean

@@ -44,6 +44,24 @@ by rw [smul_smul, u.inv_mul, one_smul]
   (u:α) • (↑u⁻¹:α) • x = x :=
 by rw [smul_smul, u.mul_inv, one_smul]
 
+/-- If a monoid `α` acts on `β`, then each `u : units α` defines a permutation of `β`. -/
+def units.smul_perm_hom : units α →* equiv.perm β :=
+{ to_fun := λ u, ⟨λ x, (u:α) • x, λ x, (↑u⁻¹:α) • x, u.inv_smul_smul, u.smul_inv_smul⟩,
+  map_one' := equiv.ext $ one_smul α,
+  map_mul' := λ u₁ u₂, equiv.ext $ mul_smul (u₁:α) u₂ }
+
+@[simp] lemma units.smul_left_cancel (u : units α) {x y : β} :
+  (u:α) • x = (u:α) • y ↔ x = y :=
+u.smul_perm_hom.apply_eq_iff_eq
+
+lemma units.smul_eq_iff_eq_inv_smul (u : units α) {x y : β} :
+  (u:α) • x = y ↔ x = (↑u⁻¹:α) • y :=
+u.smul_perm_hom.apply_eq_iff_eq_symm_apply
+
+lemma is_unit.smul_left_cancel {a : α} (ha : is_unit a) {x y : β} :
+  a • x = a • y ↔ x = y :=
+let ⟨u, hu⟩ := ha in hu ▸ u.smul_left_cancel
+
 /-- Pullback a multiplicative action along an injective map respecting `•`. -/
 protected def function.injective.mul_action [has_scalar α γ] (f : γ → β)
   (hf : injective f) (smul : ∀ (c : α) x, f (c • x) = c • f x) :
@@ -248,17 +266,11 @@ def stabilizer (b : β) : subgroup α :=
 variable (β)
 
 /-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
-def to_perm (g : α) : equiv.perm β :=
-{ to_fun := (•) g,
-  inv_fun := (•) g⁻¹,
-  left_inv := inv_smul_smul g,
-  right_inv := smul_inv_smul g }
+def to_perm : α →* equiv.perm β :=
+units.smul_perm_hom.comp to_units.to_monoid_hom
 
 variables {α} {β}
 
-instance : is_group_hom (to_perm α β) :=
-{ map_mul := λ x y, equiv.ext (λ a, mul_action.mul_smul x y a) }
-
 protected lemma bijective (g : α) : bijective (λ b : β, g • b) :=
 (to_perm α β g).bijective
 

src/linear_algebra/affine_space/basic.lean

@@ -1360,6 +1360,21 @@ lemma coe_line_map (p₀ p₁ : P1) : (line_map p₀ p₁ : k → P1) = λ c, c
 
 lemma line_map_apply (p₀ p₁ : P1) (c : k) : line_map p₀ p₁ c = c • (p₁ -ᵥ p₀) +ᵥ p₀ := rfl
 
+lemma line_map_apply_module' (p₀ p₁ : V1) (c : k) : line_map p₀ p₁ c = c • (p₁ - p₀) + p₀ := rfl
+
+lemma line_map_apply_module (p₀ p₁ : V1) (c : k) : line_map p₀ p₁ c = (1 - c) • p₀ + c • p₁ :=
+by simp [line_map_apply_module', smul_sub, sub_smul]; abel
+
+omit V1
+
+lemma line_map_apply_ring' (a b c : k) : line_map a b c = c * (b - a) + a :=
+rfl
+
+lemma line_map_apply_ring (a b c : k) : line_map a b c = (1 - c) * a + c * b :=
+line_map_apply_module a b c
+
+include V1
+
 lemma line_map_vadd_apply (p : P1) (v : V1) (c : k) :
   line_map p (v +ᵥ p) c = c • v +ᵥ p :=
 by rw [line_map_apply, vadd_vsub]
@@ -1368,8 +1383,10 @@ by rw [line_map_apply, vadd_vsub]
   (line_map p₀ p₁ : k →ᵃ[k] P1).linear = linear_map.id.smul_right (p₁ -ᵥ p₀) :=
 add_zero _
 
+lemma line_map_same_apply (p : P1) (c : k) : line_map p p c = p := by simp [line_map_apply]
+
 @[simp] lemma line_map_same (p : P1) : line_map p p = const k k p :=
-by { ext c, simp [line_map_apply] }
+ext $ line_map_same_apply p
 
 @[simp] lemma line_map_apply_zero (p₀ p₁ : P1) : line_map p₀ p₁ (0:k) = p₀ :=
 by simp [line_map_apply]
@@ -1387,12 +1404,24 @@ by simp [line_map_apply]
   f.comp (line_map p₀ p₁) = line_map (f p₀) (f p₁) :=
 ext $ f.apply_line_map p₀ p₁
 
+@[simp] lemma fst_line_map (p₀ p₁ : P1 × P2) (c : k) :
+  (line_map p₀ p₁ c).1 = line_map p₀.1 p₁.1 c :=
+fst.apply_line_map p₀ p₁ c
+
+@[simp] lemma snd_line_map (p₀ p₁ : P1 × P2) (c : k) :
+  (line_map p₀ p₁ c).2 = line_map p₀.2 p₁.2 c :=
+snd.apply_line_map p₀ p₁ c
+
 omit V2
 
 lemma line_map_symm (p₀ p₁ : P1) :
   line_map p₀ p₁ = (line_map p₁ p₀).comp (line_map (1:k) (0:k)) :=
 by { rw [comp_line_map], simp }
 
+lemma line_map_apply_one_sub (p₀ p₁ : P1) (c : k) :
+  line_map p₀ p₁ (1 - c) = line_map p₁ p₀ c :=
+by { rw [line_map_symm p₀, comp_apply], congr, simp [line_map_apply] }
+
 /-- Decomposition of an affine map in the special case when the point space and vector space
 are the same. -/
 lemma decomp (f : V1 →ᵃ[k] V2) : (f : V1 → V2) = f.linear + (λ z, f 0) :=