refactor: generalize SMul (Ideal R) (Submodule R M) to SMul (Submodule R A) (Submodule R M) (#18419)

alreadydone · alreadydone · commit a38db992d088 · 2024-12-04T12:33:11.000Z
and redefine `Mul (Submodule R A) (Submodule R A)` using the latter.
diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
@@ -93,87 +93,193 @@ theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P
   -- Porting note: simpa no longer closes refl goals, so added `SetLike.mem_coe`
   simp only [one_eq_span, span_le, Set.singleton_subset_iff, SetLike.mem_coe]
 
+variable {M : Type*} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
+
+instance : SMul (Submodule R A) (Submodule R M) where
+  smul A' M' :=
+  { __ := A'.toAddSubmonoid • M'.toAddSubmonoid
+    smul_mem' := fun r m hm ↦ AddSubmonoid.smul_induction_on hm
+      (fun a ha m hm ↦ by rw [← smul_assoc]; exact AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm)
+      fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (A'.1 • M'.1).add_mem h₁ h₂ }
+
+section
+
+variable {I J : Submodule R A} {N P : Submodule R M}
+
+theorem smul_toAddSubmonoid : (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid := rfl
+
+theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N :=
+  AddSubmonoid.smul_mem_smul hr hn
+
+theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P :=
+  AddSubmonoid.smul_le
+
+@[simp, norm_cast]
+lemma coe_set_smul : (I : Set A) • N = I • N :=
+  set_smul_eq_of_le _ _ _
+    (fun _ _ hr hx ↦ smul_mem_smul hr hx)
+    (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx)
+
+@[elab_as_elim]
+theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n))
+    (add : ∀ x y, p x → p y → p (x + y)) : p x :=
+  AddSubmonoid.smul_induction_on H smul add
+
+/-- Dependent version of `Submodule.smul_induction_on`. -/
+@[elab_as_elim]
+theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop}
+    (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn))
+    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx := by
+  refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
+  exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
+    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩
+
+theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P :=
+  AddSubmonoid.smul_le_smul hij hnp
+
+theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
+  smul_mono h le_rfl
+
+instance : CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le :=
+  ⟨fun _ _ => smul_mono le_rfl⟩
+
+@[deprecated smul_mono_right (since := "2024-03-31")]
+protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
+  _root_.smul_mono_right I h
+
+variable (I J N P)
+
+@[simp]
+theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ :=
+  toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _
+
+@[simp]
+theorem bot_smul : (⊥ : Submodule R A) • N = ⊥ :=
+  le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _
+
+theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
+  toAddSubmonoid_injective <| by
+    simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]
+
+theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
+  le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by
+    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
+    rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp)
+    (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right)
+
+protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module B M]
+    [IsScalarTower R A B] [IsScalarTower R B M] [IsScalarTower A B M]
+    (I : Submodule R A) (J : Submodule R B) (N : Submodule R M) :
+    (I • J) • N = I • J • N :=
+  le_antisymm
+    (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij
+      (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn))
+      fun x y ↦ (add_smul x y t).symm ▸ add_mem)
+    (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn
+      (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
+      fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)
+
+@[deprecated smul_inf_le (since := "2024-03-31")]
+protected theorem smul_inf_le (M₁ M₂ : Submodule R M) :
+    I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _
+
+theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
+    I • (⨆ i, t i)= ⨆ i, I • t i :=
+  toAddSubmonoid_injective <| by
+    simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]
+
+theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} :
+    (⨆ i, t i) • N = ⨆ i, t i • N :=
+  le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (· • s ∈ _)) ht
+    (fun i t ht ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
+    (by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem)
+    (iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i)
+
+@[deprecated smul_iInf_le (since := "2024-03-31")]
+protected theorem smul_iInf_le {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
+    I • iInf t ≤ ⨅ i, I • t i :=
+  smul_iInf_le
+
+protected theorem one_smul : (1 : Submodule R A) • N = N := by
+  refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
+  · obtain ⟨r, rfl⟩ := hr
+    rw [LinearMap.toSpanSingleton_apply, smul_one_smul]; exact N.smul_mem r hm
+  · rw [← one_smul A m]; exact smul_mem_smul (one_le.mp le_rfl) hm
+
+theorem smul_subset_smul : (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M) :=
+  AddSubmonoid.smul_subset_smul
+
+end
+
 variable [IsScalarTower R A A]
 
 /-- Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N`
 consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`. -/
 instance mul : Mul (Submodule R A) where
-  mul M N :=
-  { __ := M.toAddSubmonoid * N.toAddSubmonoid
-    smul_mem' := fun r a ha ↦ AddSubmonoid.mul_induction_on ha
-      (fun m h n h' ↦ by rw [← smul_mul_assoc]; exact AddSubmonoid.mul_mem_mul (M.smul_mem r h) h')
-      fun a₁ a₂ h₁ h₂ ↦ by rw [smul_add]; apply (M.1 * N.1).add_mem h₁ h₂ }
+  mul := (· • ·)
 
 variable (S T : Set A) {M N P Q : Submodule R A} {m n : A}
 
 theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N :=
-  AddSubmonoid.mul_mem_mul hm hn
+  smul_mem_smul hm hn
 
 theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P :=
-  AddSubmonoid.mul_le
+  smul_le
 
 theorem mul_toAddSubmonoid (M N : Submodule R A) :
     (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := rfl
 
 @[elab_as_elim]
 protected theorem mul_induction_on {C : A → Prop} {r : A} (hr : r ∈ M * N)
     (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
-  AddSubmonoid.mul_induction_on hr hm ha
+  smul_induction_on hr hm ha
 
 /-- A dependent version of `mul_induction_on`. -/
 @[elab_as_elim]
 protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop}
     (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn))
     (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) :
-    C r hr := by
-  refine Exists.elim ?_ fun (hr : r ∈ M * N) (hc : C r hr) ↦ hc
-  exact Submodule.mul_induction_on hr
-    (fun x hx y hy ↦ ⟨_, mem_mul_mem _ hx _ hy⟩)
-    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩
+    C r hr :=
+  smul_induction_on' hr mem_mul_mem add
 
 variable (M)
 
 @[simp]
 theorem mul_bot : M * ⊥ = ⊥ :=
-  toAddSubmonoid_injective (AddSubmonoid.mul_bot _)
+  smul_bot _
 
 @[simp]
 theorem bot_mul : ⊥ * M = ⊥ :=
-  toAddSubmonoid_injective (AddSubmonoid.bot_mul _)
+  bot_smul _
 
-protected theorem one_mul : (1 : Submodule R A) * M = M := by
-  refine le_antisymm (mul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
-  · obtain ⟨r, rfl⟩ := hr
-    rw [LinearMap.toSpanSingleton_apply, smul_one_mul]; exact M.smul_mem r hm
-  · rw [← one_mul m]; exact mul_mem_mul (one_le.mp le_rfl) hm
+protected theorem one_mul : (1 : Submodule R A) * M = M :=
+  Submodule.one_smul _
 
 variable {M}
 
 @[mono]
 theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q :=
-  AddSubmonoid.mul_le_mul hmp hnq
+  smul_mono hmp hnq
 
 theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P :=
-  AddSubmonoid.mul_le_mul_left h
+  smul_mono_left h
 
 theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P :=
-  AddSubmonoid.mul_le_mul_right h
+  smul_mono_right _ h
 
 theorem mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
   toAddSubmonoid_injective <| AddSubmonoid.mul_comm_of_commute h
 
 variable (M N P)
 
 theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P :=
-  toAddSubmonoid_injective <| by
-    simp only [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.mul_sup]
+  smul_sup _ _ _
 
 theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
-  toAddSubmonoid_injective <| by
-    simp only [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.sup_mul]
+  sup_smul _ _ _
 
 theorem mul_subset_mul : (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A) :=
-  AddSubmonoid.mul_subset_mul
+  smul_subset_smul _ _
 
 lemma restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C]
     [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C] [IsScalarTower B C C]
@@ -184,12 +290,10 @@ lemma restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C]
 variable {ι : Sort uι}
 
 theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t :=
-  toAddSubmonoid_injective <| by
-    simp only [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.iSup_mul]
+  iSup_smul
 
 theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i :=
-  toAddSubmonoid_injective <| by
-    simp only [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.mul_iSup]
+  smul_iSup
 
 /-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/
 instance : NonUnitalSemiring (Submodule R A) where
diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -56,116 +56,28 @@ section Semiring
 
 variable [Semiring R] [AddCommMonoid M] [Module R M]
 
-instance : SMul (Ideal R) (Submodule R M) where
-  smul I N :=
-  { __ := I.toAddSubmonoid • N.toAddSubmonoid
-    smul_mem' := fun r m hm ↦ AddSubmonoid.smul_induction_on hm
-      (fun m hm n ↦ by rw [smul_smul]; exact AddSubmonoid.smul_mem_smul <| I.smul_mem _ hm)
-      fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (I.1 • N.1).add_mem h₁ h₂ }
-
 /-- This duplicates the global `smul_eq_mul`, but doesn't have to unfold anywhere near as much to
 apply. -/
 protected theorem _root_.Ideal.smul_eq_mul (I J : Ideal R) : I • J = I * J :=
   rfl
 
-variable {I J : Ideal R} {N P : Submodule R M}
-
-theorem smul_toAddSubmonoid : (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid := rfl
-
-theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N :=
-  AddSubmonoid.smul_mem_smul hr hn
-
-theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P :=
-  AddSubmonoid.smul_le
-
-@[simp, norm_cast]
-lemma coe_set_smul : (I : Set R) • N = I • N :=
-  set_smul_eq_of_le _ _ _
-    (fun _ _ hr hx ↦ smul_mem_smul hr hx)
-    (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx)
-
-@[elab_as_elim]
-theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n))
-    (add : ∀ x y, p x → p y → p (x + y)) : p x :=
-  AddSubmonoid.smul_induction_on H smul add
-
-/-- Dependent version of `Submodule.smul_induction_on`. -/
-@[elab_as_elim]
-theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop}
-    (smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn))
-    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx := by
-  refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
-  exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
-    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩
+variable {I : Ideal R} {N : Submodule R M}
 
 theorem smul_le_right : I • N ≤ N :=
   smul_le.2 fun r _ _ ↦ N.smul_mem r
 
-theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P :=
-  AddSubmonoid.smul_le_smul hij hnp
-
-theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
-  smul_mono h le_rfl
-
-instance : CovariantClass (Ideal R) (Submodule R M) HSMul.hSMul LE.le :=
-  ⟨fun _ _ => smul_mono le_rfl⟩
-
-@[deprecated smul_mono_right (since := "2024-03-31")]
-protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
-  _root_.smul_mono_right I h
-
 theorem map_le_smul_top (I : Ideal R) (f : R →ₗ[R] M) :
     Submodule.map f I ≤ I • (⊤ : Submodule R M) := by
   rintro _ ⟨y, hy, rfl⟩
   rw [← mul_one y, ← smul_eq_mul, f.map_smul]
   exact smul_mem_smul hy mem_top
 
-variable (I J N P)
-
-@[simp]
-theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ :=
-  toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _
-
-@[simp]
-theorem bot_smul : (⊥ : Ideal R) • N = ⊥ :=
-  le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _
+variable (I N)
 
 @[simp]
 theorem top_smul : (⊤ : Ideal R) • N = N :=
   le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri
 
-theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
-  toAddSubmonoid_injective <| by
-    simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]
-
-theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
-  le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by
-    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
-    rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp)
-    (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right)
-
-protected theorem smul_assoc : (I • J) • N = I • J • N :=
-  le_antisymm
-    (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij
-      (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn))
-      fun x y ↦ (add_smul x y t).symm ▸ add_mem)
-    (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn
-      (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
-      fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)
-
-@[deprecated smul_inf_le (since := "2024-03-31")]
-protected theorem smul_inf_le (M₁ M₂ : Submodule R M) :
-    I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _
-
-theorem smul_iSup {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : I • iSup t = ⨆ i, I • t i :=
-  toAddSubmonoid_injective <| by
-    simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]
-
-@[deprecated smul_iInf_le (since := "2024-03-31")]
-protected theorem smul_iInf_le {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} :
-    I • iInf t ≤ ⨅ i, I • t i :=
-  smul_iInf_le
-
 theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M)
     (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by
   suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
