refactor(algebra/algebra/basic): change submodule.restrict_scalars to…

… use is_scalar_tower (#6745)

src/algebra/algebra/basic.lean

@@ -1449,14 +1449,17 @@ restrict_scalars.is_scalar_tower R A V
 
 end type_synonym
 
+/-! TODO: The following lemmas no longer involve `algebra` at all, and could be moved closer
+to `algebra/module/submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
+are all defined in `linear_algebra/basic.lean`. -/
 section semimodule
 open semimodule
 
-variables (R A M N : Type*) [comm_semiring R] [semiring A] [algebra R A]
-variables [add_comm_monoid M] [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
-variables [add_comm_monoid N] [semimodule R N] [semimodule A N] [is_scalar_tower R A N]
+variables (R S M N : Type*) [semiring R] [semiring S] [has_scalar R S]
+variables [add_comm_monoid M] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
+variables [add_comm_monoid N] [semimodule R N] [semimodule S N] [is_scalar_tower R S N]
 
-variables {A M N}
+variables {S M N}
 
 namespace submodule
 
@@ -1465,38 +1468,55 @@ namespace submodule
 corresponding to `V`, an `S`-submodule of the original `S`-module.
 -/
 @[simps]
-def restrict_scalars (V : submodule A M) : submodule R M :=
+def restrict_scalars (V : submodule S M) : submodule R M :=
 { carrier := V.carrier,
   zero_mem' := V.zero_mem,
-  smul_mem' := λ c m h, by { rw algebra_compatible_smul A c m, exact V.smul_mem _ h },
+  smul_mem' := λ c m h, V.smul_of_tower_mem c h,
   add_mem' := λ x y hx hy, V.add_mem hx hy }
 
 @[simp]
-lemma restrict_scalars_mem (V : submodule A M) (m : M) :
+lemma restrict_scalars_mem (V : submodule S M) (m : M) :
   m ∈ V.restrict_scalars R ↔ m ∈ V :=
 iff.refl _
 
-variables (R A M)
+variables (R S M)
 
 lemma restrict_scalars_injective :
-  function.injective (restrict_scalars R : submodule A M → submodule R M) :=
+  function.injective (restrict_scalars R : submodule S M → submodule R M) :=
 λ V₁ V₂ h, ext $ by convert set.ext_iff.1 (ext'_iff.1 h); refl
 
-@[simp] lemma restrict_scalars_inj {V₁ V₂ : submodule A M} :
+@[simp] lemma restrict_scalars_inj {V₁ V₂ : submodule S M} :
   restrict_scalars R V₁ = restrict_scalars R V₂ ↔ V₁ = V₂ :=
-⟨λ h, restrict_scalars_injective R _ _ h, congr_arg _⟩
+(restrict_scalars_injective R _ _).eq_iff
 
 @[simp]
-lemma restrict_scalars_bot : restrict_scalars R (⊥ : submodule A M) = ⊥ := rfl
+lemma restrict_scalars_bot : restrict_scalars R (⊥ : submodule S M) = ⊥ := rfl
 
 @[simp]
-lemma restrict_scalars_top : restrict_scalars R (⊤ : submodule A M) = ⊤ := rfl
+lemma restrict_scalars_top : restrict_scalars R (⊤ : submodule S M) = ⊤ := rfl
 
-/-- If `A` is an `R`-algebra, then the `R`-module generated by a set `X` is included in the
-`A`-module generated by `X`. -/
-lemma span_le_restrict_scalars (X : set M) : span R (X : set M) ≤ restrict_scalars R (span A X) :=
+/-- If `S` is an `R`-algebra, then the `R`-module generated by a set `X` is included in the
+`S`-module generated by `X`. -/
+lemma span_le_restrict_scalars (X : set M) : span R (X : set M) ≤ restrict_scalars R (span S X) :=
 submodule.span_le.mpr submodule.subset_span
 
+end submodule
+
+@[simp]
+lemma linear_map.ker_restrict_scalars (f : M →ₗ[S] N) :
+  (f.restrict_scalars R).ker = f.ker.restrict_scalars R :=
+rfl
+
+end semimodule
+
+end restrict_scalars
+
+namespace submodule
+
+variables (R A M : Type*)
+variables [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M]
+variables [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
+
 /-- If `A` is an `R`-algebra such that the induced morhpsim `R →+* A` is surjective, then the
 `R`-module generated by a set `X` equals the `A`-module generated by `X`. -/
 lemma span_eq_restrict_scalars (X : set M) (hsur : function.surjective (algebra_map R A)) :
@@ -1509,12 +1529,3 @@ begin
 end
 
 end submodule
-
-@[simp]
-lemma linear_map.ker_restrict_scalars (f : M →ₗ[A] N) :
-  (f.restrict_scalars R).ker = submodule.restrict_scalars R f.ker :=
-rfl
-
-end semimodule
-
-end restrict_scalars