[Merged by Bors] - feat(ring_theory/algebra): more on restrict_scalars

src/ring_theory/algebra.lean

@@ -565,7 +565,7 @@ variables (R : Type*) [comm_ring R] (S : Type*) [ring S] [algebra R S]
 (E : Type*) [add_comm_group E] [module S E] {F : Type*} [add_comm_group F] [module S F]
 
 /-- When `E` is a module over a ring `S`, and `S` is an algebra over `R`, then `E` inherits a
-module structure over `R`, called `module.restrict S R E`.
+module structure over `R`, called `module.restrict_scalars R S E`.
 Not registered as an instance as `S` can not be inferred. -/
 def module.restrict_scalars : module R E :=
 { smul      := λc x, (algebra_map R S c) • x,
@@ -576,10 +576,38 @@ def module.restrict_scalars : module R E :=
   add_smul  := by simp [add_smul],
   zero_smul := by simp [zero_smul] }
 
+/--
+The identity function, considered as an `R`-linear map from an `R`-algebra `S` to itself,
+with `module.restrict_scalars R S S` as the module structure in the source,
+and `algebra.to_module` as the module structure in the target.
+
+Unfortunately these structures are not generally definitionally equal,
+so we sometimes need to insert this map in order to typecheck.
+-/
+def algebra.restrict_scalars_iso :
+  @linear_map R S S _ _ _ (module.restrict_scalars R S S) (algebra.to_module) :=
+{ to_fun := λ s, s,
+  add := λ x y, rfl,
+  smul := λ c x, (algebra.smul_def' _ _).symm,  }
+
+@[simp]
+lemma algebra.restrict_scalars_iso_apply (s : S) : algebra.restrict_scalars_iso R S s = s := rfl
+
 variables {S E}
 
 local attribute [instance] module.restrict_scalars
 
+/--
+The `R`-submodule of the `R`-module given by restriction of scalars,
+corresponding to an `S`-submodule of the original `S`-module.
+-/
+@[simps]
+def submodule.restrict_scalars (V : submodule S E) : submodule R E :=
+{ carrier := V.carrier,
+  zero := V.zero,
+  smul := λ c e h, V.smul _ h,
+  add := λ x y hx hy, V.add hx hy, }
+
 /-- The `R`-linear map induced by an `S`-linear map when `S` is an algebra over `R`. -/
 def linear_map.restrict_scalars (f : E →ₗ[S] F) : E →ₗ[R] F :=
 { to_fun := f.to_fun,