Change Of Rings #
Main definitions #
-
category_theory.Module.restrict_scalars
: given ringsR, S
and a ring homomorphismR ⟶ S
, thenrestrict_scalars : Module S ⥤ Module R
is defined byM ↦ M
whereM : S-module
is seen asR-module
byr • m := f r • m
andS
-linear mapl : M ⟶ M'
isR
-linear as well. -
category_theory.Module.extend_scalars
: given commutative ringsR, S
and ring homomorphismf : R ⟶ S
, thenextend_scalars : Module R ⥤ Module S
is defined byM ↦ S ⨂ M
where the module structure is defined bys • (s' ⊗ m) := (s * s') ⊗ m
andR
-linear mapl : M ⟶ M'
is sent toS
-linear maps ⊗ m ↦ s ⊗ l m : S ⨂ M ⟶ S ⨂ M'
.
List of notations #
Let R, S
be rings and f : R →+* 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
The restriction of scalars operation is functorial. For any f : R →+* S
a ring homomorphism,
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' := _}
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' := _}