# mathlibdocumentation

algebra.category.Module.change_of_rings

# 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.

• category_theory.Module.extend_scalars: given commutative rings R, S and ring homomorphism f : R ⟶ S, then extend_scalars : Module R ⥤ Module S is defined by M ↦ S ⨂ M where the module structure is defined by s • (s' ⊗ m) := (s * s') ⊗ m and R-linear map l : M ⟶ M' is sent to S-linear map s ⊗ m ↦ s ⊗ l m : S ⨂ M ⟶ S ⨂ M'.

## List of notations #

Let R, S be rings and f : R →+* S

• if M is an R-module, s : S and m : M, then s ⊗ₜ[R, f] m is the pure tensor s ⊗ m : S ⊗[R, f] M.
def category_theory.Module.restrict_scalars.obj' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module 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.

Equations
def category_theory.Module.restrict_scalars.map' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module S} (g : M M') :

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.

Equations
def category_theory.Module.restrict_scalars {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

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
Equations
@[simp]
theorem category_theory.Module.restrict_scalars.map_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module S} (g : M M') (x : ) :
= g x
@[simp]
theorem category_theory.Module.restrict_scalars.smul_def {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M : Module S} (r : R) (m : ) :
r m = f r m
@[simp]
theorem category_theory.Module.restrict_scalars.smul_def' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M : Module S} (r : R) (m : M) :
r m = f r m
@[protected, instance]
def category_theory.Module.smul_comm_class_mk {R : Type u₁} {S : Type u₂} [ring R] [comm_ring S] (f : R →+* S) (M : Type v) [ M] :
M
def category_theory.Module.extend_scalars.obj' {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (M : Module R) :

Extension of scalars turn an R-module into S-module by M ↦ S ⨂ M

Equations
def category_theory.Module.extend_scalars.map' {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M1 M2 : Module R} (l : M1 M2) :

Extension of scalars is a functor where an R-module M is sent to S ⊗ M and l : M1 ⟶ M2 is sent to s ⊗ m ↦ s ⊗ l m

Equations
theorem category_theory.Module.extend_scalars.map'_id {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M : Module R} :
theorem category_theory.Module.extend_scalars.map'_comp {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M₁ M₂ M₃ : Module R} (l₁₂ : M₁ M₂) (l₂₃ : M₂ M₃) :
def category_theory.Module.extend_scalars {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

Extension of scalars is a functor where an R-module M is sent to S ⊗ M and l : M1 ⟶ M2 is sent to s ⊗ m ↦ s ⊗ l m

Equations
@[protected, simp]
theorem category_theory.Module.extend_scalars.smul_tmul {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M : Module R} (s s' : S) (m : M) :
s s' ⊗ₜ[R] m = (s * s') ⊗ₜ[R] m
@[simp]
theorem category_theory.Module.extend_scalars.map_tmul {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M M' : Module R} (g : M M') (s : S) (m : M) :
(s ⊗ₜ[R] m) = s ⊗ₜ[R] g m