fix(algebra/module/submodule): fix incorrectly generalized arguments …

…to `smul_mem_iff'` and `smul_of_tower_mem` (#9851)

These put unnecessary requirements on `S`.

src/algebra/module/submodule.lean

@@ -25,8 +25,8 @@ submodule, subspace, linear map
 open function
 open_locale big_operators
 
-universes u' u v w
-variables {S : Type u'} {R : Type u} {M : Type v} {ι : Type w}
+universes u'' u' u v w
+variables {G : Type u''} {S : Type u'} {R : Type u} {M : Type v} {ι : Type w}
 
 set_option old_structure_cmd true
 
@@ -121,16 +121,14 @@ namespace submodule
 
 section add_comm_monoid
 
-variables [semiring S] [semiring R] [add_comm_monoid M]
+variables [semiring R] [add_comm_monoid M]
 
 -- We can infer the module structure implicitly from the bundled submodule,
 -- rather than via typeclass resolution.
 variables {module_M : module R M}
 variables {p q : submodule R M}
 variables {r : R} {x y : M}
 
-variables [has_scalar S R] [module S M] [is_scalar_tower S R M]
-
 variables (p)
 @[simp] lemma mem_carrier : x ∈ p.carrier ↔ x ∈ (p : set M) := iff.rfl
 
@@ -139,7 +137,8 @@ variables (p)
 lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := p.add_mem' h₁ h₂
 
 lemma smul_mem (r : R) (h : x ∈ p) : r • x ∈ p := p.smul_mem' r h
-lemma smul_of_tower_mem (r : S) (h : x ∈ p) : r • x ∈ p :=
+lemma smul_of_tower_mem [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M]
+  (r : S) (h : x ∈ p) : r • x ∈ p :=
 p.to_sub_mul_action.smul_of_tower_mem r h
 
 lemma sum_mem {t : finset ι} {f : ι → M} : (∀c∈t, f c ∈ p) → (∑ i in t, f i) ∈ p :=
@@ -149,13 +148,18 @@ lemma sum_smul_mem {t : finset ι} {f : ι → M} (r : ι → R)
     (hyp : ∀ c ∈ t, f c ∈ p) : (∑ i in t, r i • f i) ∈ p :=
 submodule.sum_mem _ (λ i hi, submodule.smul_mem  _ _ (hyp i hi))
 
-@[simp] lemma smul_mem_iff' (u : units S) : (u:S) • x ∈ p ↔ x ∈ p :=
-p.to_sub_mul_action.smul_mem_iff' u
+@[simp] lemma smul_mem_iff' [group G] [mul_action G M] [has_scalar G R] [is_scalar_tower G R M]
+  (g : G) : g • x ∈ p ↔ x ∈ p :=
+p.to_sub_mul_action.smul_mem_iff' g
 
 instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem _ x.2 y.2⟩⟩
 instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
 instance : inhabited p := ⟨0⟩
-instance : has_scalar S p := ⟨λ c x, ⟨c • x.1, smul_of_tower_mem _ c x.2⟩⟩
+instance [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] :
+  has_scalar S p := ⟨λ c x, ⟨c • x.1, smul_of_tower_mem _ c x.2⟩⟩
+
+instance [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] : is_scalar_tower S R p :=
+p.to_sub_mul_action.is_scalar_tower
 
 protected lemma nonempty : (p : set M).nonempty := ⟨0, p.zero_mem⟩
 
@@ -167,7 +171,8 @@ variables {p}
 @[simp, norm_cast] lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : p) : M) = 0 := rfl
 @[norm_cast] lemma coe_smul (r : R) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
-@[simp, norm_cast] lemma coe_smul_of_tower (r : S) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
+@[simp, norm_cast] lemma coe_smul_of_tower [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M]
+  (r : S) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
 @[simp, norm_cast] lemma coe_mk (x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x := rfl
 @[simp] lemma coe_mem (x : p) : (x : M) ∈ p := x.2
 
@@ -176,14 +181,11 @@ variables (p)
 instance : add_comm_monoid p :=
 { add := (+), zero := 0, .. p.to_add_submonoid.to_add_comm_monoid }
 
-instance module' : module S p :=
+instance module' [semiring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] : module S p :=
 by refine {smul := (•), ..p.to_sub_mul_action.mul_action', ..};
    { intros, apply set_coe.ext, simp [smul_add, add_smul, mul_smul] }
 instance : module R p := p.module'
 
-instance : is_scalar_tower S R p :=
-p.to_sub_mul_action.is_scalar_tower
-
 instance no_zero_smul_divisors [no_zero_smul_divisors R M] : no_zero_smul_divisors R p :=
 ⟨λ c x h,
   have c = 0 ∨ (x : M) = 0,
@@ -203,7 +205,7 @@ lemma subtype_eq_val : ((submodule.subtype p) : p → M) = subtype.val := rfl
 p.subtype.map_sum
 
 section restrict_scalars
-variables (S) [module R M] [is_scalar_tower S R M]
+variables (S) [semiring S] [module S M] [module R M] [has_scalar S R] [is_scalar_tower S R M]
 
 /--
 `V.restrict_scalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,

src/group_theory/group_action/sub_mul_action.lean

@@ -30,8 +30,8 @@ submodule, mul_action
 
 open function
 
-universes u u' v
-variables {S : Type u'} {R : Type u} {M : Type v}
+universes u u' u'' v
+variables {S : Type u'} {T : Type u''} {R : Type u} {M : Type v}
 
 set_option old_structure_cmd true
 
@@ -102,14 +102,13 @@ end has_scalar
 
 section mul_action
 
-variables [monoid S] [monoid R]
+variables [monoid R] [mul_action R M]
 
-variables [mul_action R M]
-variables [has_scalar S R] [mul_action S M] [is_scalar_tower S R M]
+section
+variables [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M]
 variables (p : sub_mul_action R M)
-variables {r : R} {x : M}
 
-lemma smul_of_tower_mem (s : S) (h : x ∈ p) : s • x ∈ p :=
+lemma smul_of_tower_mem (s : S) {x : M} (h : x ∈ p) : s • x ∈ p :=
 by { rw [←one_smul R x, ←smul_assoc], exact p.smul_mem _ h }
 
 instance has_scalar' : has_scalar S p :=
@@ -120,9 +119,16 @@ instance : is_scalar_tower S R p :=
 
 @[simp, norm_cast] lemma coe_smul_of_tower (s : S) (x : p) : ((s • x : p) : M) = s • ↑x := rfl
 
-@[simp] lemma smul_mem_iff' (u : units S) : (u : S) • x ∈ p ↔ x ∈ p :=
-⟨λ h, by simpa only [smul_smul, u.inv_mul, one_smul] using p.smul_of_tower_mem (↑u⁻¹ : S) h,
-  p.smul_of_tower_mem u⟩
+@[simp] lemma smul_mem_iff' {G} [group G] [has_scalar G R] [mul_action G M]
+  [is_scalar_tower G R M] (g : G) {x : M} :
+  g • x ∈ p ↔ x ∈ p :=
+⟨λ h, inv_smul_smul g x ▸ p.smul_of_tower_mem g⁻¹ h, p.smul_of_tower_mem g⟩
+
+end
+
+section
+variables [monoid S] [has_scalar S R] [mul_action S M] [is_scalar_tower S R M]
+variables (p : sub_mul_action R M)
 
 /-- If the scalar product forms a `mul_action`, then the subset inherits this action -/
 instance mul_action' : mul_action S p :=
@@ -132,6 +138,8 @@ instance mul_action' : mul_action S p :=
 
 instance : mul_action R p := p.mul_action'
 
+end
+
 end mul_action
 
 section module

src/topology/algebra/module.lean

@@ -94,10 +94,10 @@ begin
     from tendsto_const_nhds.add ((tendsto_nhds_within_of_tendsto_nhds tendsto_id).smul
       tendsto_const_nhds),
   rw [zero_smul, add_zero] at this,
-  rcases nonempty_of_mem (inter_mem (mem_map.1 (this hy)) self_mem_nhds_within)
-    with ⟨_, hu, u, rfl⟩,
+  obtain ⟨_, hu : y + _ • _ ∈ s, u, rfl⟩ :=
+    nonempty_of_mem (inter_mem (mem_map.1 (this hy)) self_mem_nhds_within),
   have hy' : y ∈ ↑s := mem_of_mem_nhds hy,
-  exact (s.smul_mem_iff' _).1 ((s.add_mem_iff_right hy').1 hu)
+  rwa [s.add_mem_iff_right hy', ←units.smul_def, s.smul_mem_iff' u] at hu,
 end
 
 variables (R M)