feat: pointwise scalar multiplication is monotone (#11809)

Everywhere we have a `smul_mem_pointwise_smul` lemma, I've added this result.

Mathlib.lean

@@ -401,6 +401,7 @@ import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Algebra.Order.Floor
 import Mathlib.Algebra.Order.Floor.Div
 import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Algebra.Order.Group.Action
 import Mathlib.Algebra.Order.Group.Bounds
 import Mathlib.Algebra.Order.Group.Cone
 import Mathlib.Algebra.Order.Group.Defs

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

@@ -110,6 +110,9 @@ theorem smul_mem_pointwise_smul (m : R') (r : A) (S : Subalgebra R A) : r ∈ S
   (Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set A))
 #align subalgebra.smul_mem_pointwise_smul Subalgebra.smul_mem_pointwise_smul
 
+instance : CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => map_mono⟩
+
 end Pointwise
 
 end Subalgebra

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -8,6 +8,7 @@ import Mathlib.LinearAlgebra.Span
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.Algebra.Module.BigOperators
+import Mathlib.Algebra.Order.Group.Action
 
 #align_import algebra.module.submodule.pointwise from "leanprover-community/mathlib"@"48085f140e684306f9e7da907cd5932056d1aded"
 
@@ -240,6 +241,9 @@ theorem smul_mem_pointwise_smul (m : M) (a : α) (S : Submodule R M) : m ∈ S 
   (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))
 #align submodule.smul_mem_pointwise_smul Submodule.smul_mem_pointwise_smul
 
+instance : CovariantClass α (Submodule R M) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => map_mono⟩
+
 /-- See also `Submodule.smul_bot`. -/
 @[simp]
 theorem smul_bot' (a : α) : a • (⊥ : Submodule R M) = ⊥ :=
@@ -374,10 +378,14 @@ lemma set_smul_eq_of_le (p : Submodule R M)
     s • N = p :=
   le_antisymm (set_smul_le s N p closed_under_smul) le
 
-lemma set_smul_mono_right {p q : Submodule R M} (le : p ≤ q) :
+instance : CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le :=
+  ⟨fun _ _ _ le => set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := hr)
+    (mem2 := le hm)⟩
+
+-- 2024-03-31
+@[deprecated smul_mono_right] theorem set_smul_mono_right {p q : Submodule R M} (le : p ≤ q) :
     s • p ≤ s • q :=
-  set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := hr)
-    (mem2 := le hm)
+  smul_mono_right s le
 
 lemma set_smul_mono_left {s t : Set S} (le : s ≤ t) :
     s • N ≤ t • N :=
@@ -386,7 +394,7 @@ lemma set_smul_mono_left {s t : Set S} (le : s ≤ t) :
 
 lemma set_smul_le_of_le_le {s t : Set S} {p q : Submodule R M}
     (le_set : s ≤ t) (le_submodule : p ≤ q) : s • p ≤ t • q :=
-  le_trans (set_smul_mono_left _ le_set) <| set_smul_mono_right _ le_submodule
+  le_trans (set_smul_mono_left _ le_set) <| smul_mono_right _ le_submodule
 
 variable {s N} in
 /--
@@ -545,8 +553,7 @@ protected def pointwiseSetDistribMulAction [SMulCommClass R R M] :
       rw [smul_add, add_eq_sup, Submodule.mem_sup]
       exact ⟨r • a, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := ha),
         r • b, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := hb), rfl⟩)
-    (sup_le_iff.mpr ⟨set_smul_mono_right _ le_sup_left,
-      set_smul_mono_right _ le_sup_right⟩)
+    (sup_le_iff.mpr ⟨smul_mono_right _ le_sup_left, smul_mono_right _ le_sup_right⟩)
 
 scoped[Pointwise] attribute [instance] Submodule.pointwiseSetDistribMulAction
 

Mathlib/Algebra/Order/Group/Action.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Algebra.CovariantAndContravariant
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/-!
+# Results about `CovariantClass G α HSMul.hSMul LE.le`
+
+When working with group actions rather than modules, we drop the `0 < c` condition.
+
+Notably these are relevant for pointwise actions on set-like objects.
+-/
+
+variable {ι : Sort*} {M α : Type*}
+
+theorem smul_mono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le]
+    (m : M) : Monotone (HSMul.hSMul m : α → α) :=
+  fun _ _ => CovariantClass.elim _
+
+/-- A copy of `smul_mono_right` that is understood by `gcongr`. -/
+@[gcongr]
+theorem smul_le_smul_left [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le]
+    (m : M) {a b : α} (h : a ≤ b) :
+    m • a ≤ m • b :=
+  smul_mono_right _ h
+
+theorem smul_inf_le [SMul M α] [SemilatticeInf α] [CovariantClass M α HSMul.hSMul LE.le]
+    (m : M) (a₁ a₂ : α) : m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂ :=
+  (smul_mono_right _).map_inf_le _ _
+
+theorem smul_iInf_le [SMul M α] [CompleteLattice α] [CovariantClass M α HSMul.hSMul LE.le]
+    {m : M} {t : ι → α} :
+    m • iInf t ≤ ⨅ i, m • t i :=
+  le_iInf fun _ => smul_mono_right _ (iInf_le _ _)
+
+theorem smul_strictMono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LT.lt]
+    (m : M) : StrictMono (HSMul.hSMul m : α → α) :=
+  fun _ _ => CovariantClass.elim _

Mathlib/GroupTheory/Subgroup/Pointwise.lean

@@ -330,6 +330,9 @@ theorem smul_mem_pointwise_smul (m : G) (a : α) (S : Subgroup G) : m ∈ S →
   (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set G))
 #align subgroup.smul_mem_pointwise_smul Subgroup.smul_mem_pointwise_smul
 
+instance : CovariantClass α (Subgroup G) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => image_subset _⟩
+
 theorem mem_smul_pointwise_iff_exists (m : G) (a : α) (S : Subgroup G) :
     m ∈ a • S ↔ ∃ s : G, s ∈ S ∧ a • s = m :=
   (Set.mem_smul_set : m ∈ a • (S : Set G) ↔ _)

Mathlib/GroupTheory/Submonoid/Pointwise.lean

@@ -239,6 +239,9 @@ theorem smul_mem_pointwise_smul (m : M) (a : α) (S : Submonoid M) : m ∈ S →
   (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))
 #align submonoid.smul_mem_pointwise_smul Submonoid.smul_mem_pointwise_smul
 
+instance : CovariantClass α (Submonoid M) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => image_subset _⟩
+
 theorem mem_smul_pointwise_iff_exists (m : M) (a : α) (S : Submonoid M) :
     m ∈ a • S ↔ ∃ s : M, s ∈ S ∧ a • s = m :=
   (Set.mem_smul_set : m ∈ a • (S : Set M) ↔ _)

Mathlib/RingTheory/Filtration.lean

@@ -67,12 +67,12 @@ theorem pow_smul_le (i j : ℕ) : I ^ i • F.N j ≤ F.N (i + j) := by
   induction' i with _ ih
   · simp
   · rw [pow_succ', mul_smul, Nat.succ_eq_add_one, add_assoc, add_comm 1, ← add_assoc]
-    exact (Submodule.smul_mono_right ih).trans (F.smul_le _)
+    exact (smul_mono_right _ ih).trans (F.smul_le _)
 #align ideal.filtration.pow_smul_le Ideal.Filtration.pow_smul_le
 
 theorem pow_smul_le_pow_smul (i j k : ℕ) : I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j) := by
   rw [add_comm, pow_add, mul_smul]
-  exact Submodule.smul_mono_right (F.pow_smul_le i j)
+  exact smul_mono_right _ (F.pow_smul_le i j)
 #align ideal.filtration.pow_smul_le_pow_smul Ideal.Filtration.pow_smul_le_pow_smul
 
 protected theorem antitone : Antitone F.N :=
@@ -111,7 +111,7 @@ instance : SupSet (I.Filtration M) :=
 instance : Inf (I.Filtration M) :=
   ⟨fun F F' =>
     ⟨F.N ⊓ F'.N, fun i => inf_le_inf (F.mono i) (F'.mono i), fun i =>
-      (Submodule.smul_inf_le _ _ _).trans <| inf_le_inf (F.smul_le i) (F'.smul_le i)⟩⟩
+      (smul_inf_le _ _ _).trans <| inf_le_inf (F.smul_le i) (F'.smul_le i)⟩⟩
 
 /-- The `sInf` of a family of `I.Filtration`s is an `I.Filtration`. -/
 instance : InfSet (I.Filtration M) :=
@@ -123,7 +123,7 @@ instance : InfSet (I.Filtration M) :=
         exact ⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono i⟩
       smul_le := fun i => by
         rw [sInf_eq_iInf', iInf_apply, iInf_apply]
-        refine' Submodule.smul_iInf_le.trans _
+        refine' smul_iInf_le.trans _
         apply iInf_mono _
         rintro ⟨_, F, hF, rfl⟩
         exact F.smul_le i }⟩
@@ -245,7 +245,7 @@ theorem Stable.exists_forall_le (h : F.Stable) (e : F.N 0 ≤ F'.N 0) :
   induction' n with n hn
   · refine' (F.antitone _).trans e; simp
   · rw [Nat.succ_eq_one_add, add_assoc, add_comm, add_comm 1 n, ← hF]
-    exact (Submodule.smul_mono_right hn).trans (F'.smul_le _)
+    exact (smul_mono_right _ hn).trans (F'.smul_le _)
     simp
 #align ideal.filtration.stable.exists_forall_le Ideal.Filtration.Stable.exists_forall_le
 

Mathlib/RingTheory/Ideal/Operations.lean

@@ -13,6 +13,7 @@ import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.LinearAlgebra.Basis
 import Mathlib.LinearAlgebra.Quotient
+import Mathlib.Algebra.Order.Group.Action
 
 #align_import ring_theory.ideal.operations from "leanprover-community/mathlib"@"e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74"
 
@@ -187,8 +188,12 @@ theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
   map₂_le_map₂_left h
 #align submodule.smul_mono_left Submodule.smul_mono_left
 
-theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
-  map₂_le_map₂_right h
+instance : CovariantClass (Ideal R) (Submodule R M) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => map₂_le_map₂_right⟩
+
+@[deprecated smul_mono_right] -- 2024-03-31
+protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
+  _root_.smul_mono_right I h
 #align submodule.smul_mono_right Submodule.smul_mono_right
 
 theorem map_le_smul_top (I : Ideal R) (f : R →ₗ[R] M) :
@@ -250,17 +255,19 @@ protected theorem smul_assoc : (I • J) • N = I • J • N :=
         show r • s • n ∈ (I • J) • N from mul_smul r s n ▸ smul_mem_smul (smul_mem_smul hr hs) hn)
 #align submodule.smul_assoc Submodule.smul_assoc
 
-theorem smul_inf_le (M₁ M₂ : Submodule R M) : I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ :=
-  le_inf (Submodule.smul_mono_right inf_le_left) (Submodule.smul_mono_right inf_le_right)
+@[deprecated smul_inf_le] -- 2024-03-31
+protected theorem smul_inf_le (M₁ M₂ : Submodule R M) :
+    I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _
 #align submodule.smul_inf_le Submodule.smul_inf_le
 
 theorem smul_iSup {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : I • iSup t = ⨆ i, I • t i :=
   map₂_iSup_right _ _ _
 #align submodule.smul_supr Submodule.smul_iSup
 
-theorem smul_iInf_le {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} :
+@[deprecated smul_iInf_le] -- 2024-03-31
+protected theorem smul_iInf_le {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} :
     I • iInf t ≤ ⨅ i, I • t i :=
-  le_iInf fun _ => smul_mono_right (iInf_le _ _)
+  smul_iInf_le
 #align submodule.smul_infi_le Submodule.smul_iInf_le
 
 variable (S : Set R) (T : Set M)
@@ -820,7 +827,7 @@ theorem mul_mono_left (h : I ≤ J) : I * K ≤ J * K :=
 #align ideal.mul_mono_left Ideal.mul_mono_left
 
 theorem mul_mono_right (h : J ≤ K) : I * J ≤ I * K :=
-  Submodule.smul_mono_right h
+  smul_mono_right _ h
 #align ideal.mul_mono_right Ideal.mul_mono_right
 
 variable (I J K)

Mathlib/RingTheory/Subring/Pointwise.lean

@@ -75,6 +75,9 @@ theorem smul_mem_pointwise_smul (m : M) (r : R) (S : Subring R) : r ∈ S → m
   (Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set R))
 #align subring.smul_mem_pointwise_smul Subring.smul_mem_pointwise_smul
 
+instance : CovariantClass M (Subring R) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => image_subset _⟩
+
 theorem mem_smul_pointwise_iff_exists (m : M) (r : R) (S : Subring R) :
     r ∈ m • S ↔ ∃ s : R, s ∈ S ∧ m • s = r :=
   (Set.mem_smul_set : r ∈ m • (S : Set R) ↔ _)

Mathlib/RingTheory/Subsemiring/Pointwise.lean

@@ -69,6 +69,9 @@ theorem smul_mem_pointwise_smul (m : M) (r : R) (S : Subsemiring R) : r ∈ S 
   (Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set R))
 #align subsemiring.smul_mem_pointwise_smul Subsemiring.smul_mem_pointwise_smul
 
+instance : CovariantClass M (Subsemiring R) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => image_subset _⟩
+
 theorem mem_smul_pointwise_iff_exists (m : M) (r : R) (S : Subsemiring R) :
     r ∈ m • S ↔ ∃ s : R, s ∈ S ∧ m • s = r :=
   (Set.mem_smul_set : r ∈ m • (S : Set R) ↔ _)
@@ -174,4 +177,3 @@ theorem le_pointwise_smul_iff₀ {a : M} (ha : a ≠ 0) {S T : Subsemiring R} :
 end GroupWithZero
 
 end Subsemiring
-

Mathlib/RingTheory/Valuation/ValuationSubring.lean

@@ -841,6 +841,9 @@ theorem smul_mem_pointwise_smul (g : G) (x : K) (S : ValuationSubring K) : x ∈
   (Set.smul_mem_smul_set : _ → _ ∈ g • (S : Set K))
 #align valuation_subring.smul_mem_pointwise_smul ValuationSubring.smul_mem_pointwise_smul
 
+instance : CovariantClass G (ValuationSubring K) HSMul.hSMul LE.le :=
+  ⟨fun _ _ _ => Set.image_subset _⟩
+
 theorem mem_smul_pointwise_iff_exists (g : G) (x : K) (S : ValuationSubring K) :
     x ∈ g • S ↔ ∃ s : K, s ∈ S ∧ g • s = x :=
   (Set.mem_smul_set : x ∈ g • (S : Set K) ↔ _)