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) :

Module R

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

category_theory.Module.restrict_scalars.obj' f M = Module.mk ↥M

source

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') :

category_theory.Module.restrict_scalars.obj' f M ⟶ category_theory.Module.restrict_scalars.obj' f 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

category_theory.Module.restrict_scalars.map' f g = {to_fun := g.to_fun, map_add' := _, map_smul' := _}

source

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

Module S ⥤ Module R

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

category_theory.Module.restrict_scalars f = {obj := category_theory.Module.restrict_scalars.obj' f, map := λ (_x _x_1 : Module S), category_theory.Module.restrict_scalars.map' f, map_id' := _, map_comp' := _}

source

@[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 : ↥((category_theory.Module.restrict_scalars f).obj M)) :

⇑((category_theory.Module.restrict_scalars f).map g) x = ⇑g x

source

@[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 : ↥((category_theory.Module.restrict_scalars f).obj M)) :

r • m = ⇑f r • m

source

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

source

@[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) [add_comm_group M] [module S M] :

smul_comm_class R S M

source

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) :

Module S

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

Equations

category_theory.Module.extend_scalars.obj' f M = Module.mk (tensor_product R ↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) ↥M)

source

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) :

category_theory.Module.extend_scalars.obj' f M1 ⟶ category_theory.Module.extend_scalars.obj' f 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

category_theory.Module.extend_scalars.map' f l = linear_map.base_change S l

source

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} :

category_theory.Module.extend_scalars.map' f (𝟙 M) = 𝟙 (category_theory.Module.extend_scalars.obj' f M)

source

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₃) :

category_theory.Module.extend_scalars.map' f (l₁₂ ≫ l₂₃) = category_theory.Module.extend_scalars.map' f l₁₂ ≫ category_theory.Module.extend_scalars.map' f l₂₃

source

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

Module R ⥤ Module 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

category_theory.Module.extend_scalars f = {obj := λ (M : Module R), category_theory.Module.extend_scalars.obj' f M, map := λ (M1 M2 : Module R) (l : M1 ⟶ M2), category_theory.Module.extend_scalars.map' f l, map_id' := _, map_comp' := _}

source

@[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

source

@[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) :

⇑((category_theory.Module.extend_scalars f).map g) (s ⊗ₜ[R] m) = s ⊗ₜ[R] ⇑g m