feat(ring_theory/algebra): more on restrict_scalars (#2445)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/analysis/normed_space/basic.lean

@@ -900,12 +900,14 @@ variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_field 𝕜'
 
 /-- `𝕜`-normed space structure induced by a `𝕜'`-normed space structure when `𝕜'` is a
 normed algebra over `𝕜`. Not registered as an instance as `𝕜'` can not be inferred. -/
+-- We could add a type synonym equipped with this as an instance,
+-- as we've done for `module.restrict_scalars`.
 def normed_space.restrict_scalars : normed_space 𝕜 E :=
 { norm_smul_le := λc x, le_of_eq $ begin
     change ∥(algebra_map 𝕜 𝕜' c) • x∥ = ∥c∥ * ∥x∥,
     simp [norm_smul]
   end,
-  ..module.restrict_scalars 𝕜 𝕜' E }
+  ..module.restrict_scalars' 𝕜 𝕜' E }
 
 end restrict_scalars
 

src/data/complex/module.lean

@@ -21,5 +21,5 @@ end complex
 /- Register as an instance (with low priority) the fact that a complex vector space is also a real
 vector space. -/
 instance module.complex_to_real (E : Type*) [add_comm_group E] [module ℂ E] : module ℝ E :=
-module.restrict_scalars ℝ ℂ E
+module.restrict_scalars' ℝ ℂ E
 attribute [instance, priority 900] module.complex_to_real

src/ring_theory/algebra.lean

@@ -723,33 +723,111 @@ section restrict_scalars
 `S`-modules are also `R`-modules. -/
 
 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]
+variables (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`.
-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,
+/--
+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_scalars' R S E`.
+We do not register this 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,
   one_smul  := by simp,
   mul_smul  := by simp [mul_smul],
   smul_add  := by simp [smul_add],
   smul_zero := by simp [smul_zero],
   add_smul  := by simp [add_smul],
   zero_smul := by simp [zero_smul] }
 
+/--
+When `E` is a module over a ring `S`, and `S` is an algebra over `R`, then `E` inherits a
+module structure over `R`, provided as a type synonym `module.restrict_scalars R S E := E`.
+-/
+@[nolint unused_arguments]
+def module.restrict_scalars (R : Type*) (S : Type*) (E : Type*) : Type* := E
+
+instance (R : Type*) (S : Type*) (E : Type*) [I : inhabited E] :
+  inhabited (module.restrict_scalars R S E) := I
+
+instance (R : Type*) (S : Type*) (E : Type*) [I : add_comm_group E] :
+   add_comm_group (module.restrict_scalars R S E) := I
+
+instance : module R (module.restrict_scalars R S E) :=
+(module.restrict_scalars' R S E : module R E)
+
+lemma module.restrict_scalars_smul_def (c : R) (x : module.restrict_scalars R S E) :
+  c • x = ((algebra_map R S c) • x : E) := rfl
+
+/--
+`module.restrict_scalars R S S` is `R`-linearly equivalent to the original algebra `S`.
+
+Unfortunately these structures are not generally definitionally equal:
+the `R`-module structure on `S` is part of the data of `S`,
+while the `R`-module structure on `module.restrict_scalars R S S`
+comes from the ring homomorphism `R →+* S`, which is a separate part of the data of `S`.
+The field `algebra.smul_def'` gives the equation we need here.
+-/
+def algebra.restrict_scalars_equiv :
+  (module.restrict_scalars R S S) ≃ₗ[R] S :=
+{ to_fun := λ s, s,
+  inv_fun := λ s, s,
+  left_inv := λ s, rfl,
+  right_inv := λ s, rfl,
+  add := λ x y, rfl,
+  smul := λ c x, (algebra.smul_def' _ _).symm, }
+
+@[simp]
+lemma algebra.restrict_scalars_equiv_apply (s : S) :
+  algebra.restrict_scalars_equiv R S s = s := rfl
+@[simp]
+lemma algebra.restrict_scalars_equiv_symm_apply (s : S) :
+  (algebra.restrict_scalars_equiv R S).symm s = s := rfl
+
 variables {S E}
 
-local attribute [instance] module.restrict_scalars
+open module
+
+/--
+`V.restrict_scalars R` is the `R`-submodule of the `R`-module given by restriction of scalars,
+corresponding to `V`, an `S`-submodule of the original `S`-module.
+-/
+@[simps]
+def submodule.restrict_scalars (V : submodule S E) : submodule R (restrict_scalars R S E) :=
+{ carrier := V.carrier,
+  zero := V.zero,
+  smul := λ c e h, V.smul _ h,
+  add := λ x y hx hy, V.add hx hy, }
+
+@[simp]
+lemma submodule.restrict_scalars_mem (V : submodule S E) (e : E) :
+  e ∈ V.restrict_scalars R ↔ e ∈ V :=
+iff.refl _
+
+@[simp]
+lemma submodule.restrict_scalars_bot :
+  submodule.restrict_scalars R (⊥ : submodule S E) = ⊥ :=
+rfl
+
+@[simp]
+lemma submodule.restrict_scalars_top :
+  submodule.restrict_scalars R (⊤ : submodule S E) = ⊤ :=
+rfl
 
 /-- 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 :=
+def linear_map.restrict_scalars (f : E →ₗ[S] F) :
+  (restrict_scalars R S E) →ₗ[R] (restrict_scalars R S F) :=
 { to_fun := f.to_fun,
   add := λx y, f.map_add x y,
   smul := λc x, f.map_smul (algebra_map R S c) x }
 
 @[simp, norm_cast squash] lemma linear_map.coe_restrict_scalars_eq_coe (f : E →ₗ[S] F) :
   (f.restrict_scalars R : E → F) = f := rfl
 
+@[simp]
+lemma restrict_scalars_ker (f : E →ₗ[S] F) :
+  (f.restrict_scalars R).ker = submodule.restrict_scalars R f.ker :=
+rfl
+
 end restrict_scalars
 
 
@@ -790,4 +868,15 @@ def linear_map_algebra_module : module R (V →ₗ[S] W) :=
   zero_smul := λ f, by { ext v, dsimp [(•)], simp, },
   add_smul := λ r r' f, by { ext v, dsimp [(•)], simp [add_smul], }, }
 
+local attribute [instance] linear_map_algebra_module
+
+variables {R S V W}
+@[simp]
+lemma linear_map_algebra_module.smul_apply (c : R) (f : V →ₗ[S] W) (v : V) :
+  (c • f) v = (c • (f v) : module.restrict_scalars R S W) :=
+begin
+  erw [linear_map.map_smul],
+  refl,
+end
+
 end module_of_linear_maps