feat(algebra/category/Module/change_of_rings): restriction of scalars (…

…#15672)

Given a ring homomorphism $f : R\to S$, there is a functor from $S$-module to $R$-module.

In #15564, it will proven that extension of scalars $\dashv$ restriction of scalars

src/algebra/category/Module/change_of_rings.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import algebra.category.Module.basic
+
+/-!
+# Change Of Rings
+
+## Main definitions
+
+* `category_theory.Module.restrict_scalars`: given rings `R, S` and a ring homomorphism `R ⟶ S`,
+  then `restrict_scalars : Module S ⥤ Module R` is defined by `M ↦ M` where `M : S-module` is seen
+  as `R-module` by `r • m := f r • m` and `S`-linear map `l : M ⟶ M'` is `R`-linear as well.
+-/
+
+
+namespace category_theory.Module
+
+universes v u₁ u₂
+
+namespace restrict_scalars
+
+variables {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
+variable (M : Module.{v} S)
+
+/-- Any `S`-module M is also an `R`-module via a ring homomorphism `f : R ⟶ S` by defining
+    `r • m := f r • m` (`module.comp_hom`). This is called restriction of scalars. -/
+def obj' : Module R :=
+{ carrier := M,
+  is_module := module.comp_hom M f }
+
+/--
+Given an `S`-linear map `g : M → M'` between `S`-modules, `g` is also `R`-linear between `M` and
+`M'` by means of restriction of scalars.
+-/
+def map' {M M' : Module.{v} S} (g : M ⟶ M') :
+  obj' f M ⟶ obj' f M' :=
+{ map_smul' := λ r, g.map_smul (f r), ..g }
+
+end restrict_scalars
+
+/--
+The restriction of scalars operation is functorial. For any `f : R →+* S` a ring homomorphism,
+* an `S`-module `M` can be considered as `R`-module by `r • m = f r • m`
+* an `S`-linear map is also `R`-linear
+-/
+def restrict_scalars {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :
+  Module.{v} S ⥤ Module.{v} R :=
+{ obj := restrict_scalars.obj' f,
+  map := λ _ _, restrict_scalars.map' f,
+  map_id' := λ _, linear_map.ext $ λ m, rfl,
+  map_comp' := λ _ _ _ g h, linear_map.ext $ λ m, rfl }
+
+@[simp] lemma restrict_scalars.map_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
+  {M M' : Module.{v} S} (g : M ⟶ M') (x) : (restrict_scalars f).map g x = g x := rfl
+
+@[simp] lemma restrict_scalars.smul_def {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
+  {M : Module.{v} S} (r : R) (m : (restrict_scalars f).obj M) : r • m = (f r • m : M) := rfl
+
+@[simp] lemma restrict_scalars.smul_def' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
+  {M : Module.{v} S} (r : R) (m : M) : (r • m : (restrict_scalars f).obj M) = (f r • m : M) := rfl
+
+end category_theory.Module