# mathlib3documentation

algebra.category.Module.change_of_rings

# Change Of Rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

• category_theory.Module.coextend_scalars: given rings R, S and a ring homomorphism R ⟶ S then coextend_scalars : Module R ⥤ Module S is defined by M ↦ (S →ₗ[R] M) where S is seen as R-module by restriction of scalars and l ↦ l ∘ _.

## Main results #

• category_theory.Module.extend_restrict_scalars_adj: given commutative rings R, S and a ring homomorphism f : R →+* S, the extension and restriction of scalars by f are adjoint functors.
• category_theory.Module.restrict_coextend_scalars_adj: given rings R, S and a ring homomorphism f : R ⟶ S then coextend_scalars f is the right adjoint of restrict_scalars f.

## 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
Instances for category_theory.Module.restrict_scalars
@[protected, instance]
@[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
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
Instances for category_theory.Module.extend_scalars
@[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
@[protected, instance]
def category_theory.Module.coextend_scalars.has_smul {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [ M] :

Given an R-module M, consider Hom(S, M) -- the R-linear maps between S (as an R-module by means of restriction of scalars) and M. S acts on Hom(S, M) by s • g = x ↦ g (x • s)

Equations
@[simp]
theorem category_theory.Module.coextend_scalars.smul_apply' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [ M] (s : S) (g : →ₗ[R] M) (s' : S) :
(s g) s' = g (s' * s)
@[protected, instance]
def category_theory.Module.coextend_scalars.mul_action {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [ M] :
Equations
@[protected, instance]
def category_theory.Module.coextend_scalars.distrib_mul_action {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [ M] :
Equations
@[protected, instance]
def category_theory.Module.coextend_scalars.is_module {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [ M] :

S acts on Hom(S, M) by s • g = x ↦ g (x • s), this action defines an S-module structure on Hom(S, M).

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

If M is an R-module, then the set of R-linear maps S →ₗ[R] M is an S-module with scalar multiplication defined by s • l := x ↦ l (x • s)

Equations
Instances for ↥category_theory.Module.coextend_scalars.obj'
@[protected, instance]
def category_theory.Module.coextend_scalars.obj'.has_coe_to_fun {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) :
(λ (g : , S M)
Equations
@[simp]
theorem category_theory.Module.coextend_scalars.map'_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module R} (g : M M')  :
def category_theory.Module.coextend_scalars.map' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module R} (g : M M') :

If M, M' are R-modules, then any R-linear map g : M ⟶ M' induces an S-linear map (S →ₗ[R] M) ⟶ (S →ₗ[R] M') defined by h ↦ g ∘ h

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

For any rings R, S and a ring homomorphism f : R →+* S, there is a functor from R-module to S-module defined by M ↦ (S →ₗ[R] M) where S is considered as an R-module via restriction of scalars and g : M ⟶ M' is sent to h ↦ g ∘ h.

Equations
Instances for category_theory.Module.coextend_scalars
@[protected, instance]
def category_theory.Module.coextend_scalars.obj.has_coe_to_fun {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) :
(λ (g : , S M)
Equations
theorem category_theory.Module.coextend_scalars.smul_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) (g : ) (s s' : S) :
(s g) s' = g (s' * s)
@[simp]
theorem category_theory.Module.coextend_scalars.map_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module R} (g : M M') (x : ) (s : S) :
x) s = g (x s)
@[simp]
theorem category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction_apply_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X) (y : Y) (s : S) :
def category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X) :

Given R-module X and S-module Y, any g : (restrict_of_scalars f).obj Y ⟶ X corresponds to Y ⟶ (coextend_scalars f).obj X by sending y ↦ (s ↦ g (s • y))

Equations
@[simp]
theorem category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : Y ) (y : Y) :
def category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : Y ) :

Given R-module X and S-module Y, any g : Y ⟶ (coextend_scalars f).obj X corresponds to (restrict_scalars f).obj Y ⟶ X by y ↦ g y 1

Equations
@[simp]
theorem category_theory.Module.restriction_coextension_adj.unit'_app_apply_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (Y : Module S) (y : Y) (s : S) :
= s y
@[protected]
def category_theory.Module.restriction_coextension_adj.unit' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

The natural transformation from identity functor to the composition of restriction and coextension of scalars.

Equations
@[simp]
theorem category_theory.Module.restriction_coextension_adj.counit'_app_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (X : Module R)  :
@[protected]
def category_theory.Module.restriction_coextension_adj.counit' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

The natural transformation from the composition of coextension and restriction of scalars to identity functor.

Equations
@[simp]
theorem category_theory.Module.restrict_coextend_scalars_adj_unit {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :
@[simp]
theorem category_theory.Module.restrict_coextend_scalars_adj_counit {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :
@[simp]
theorem category_theory.Module.restrict_coextend_scalars_adj_hom_equiv_symm_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (X : Module S) (Y : Module R) (g : X ) :
def category_theory.Module.restrict_coextend_scalars_adj {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

Restriction of scalars is left adjoint to coextension of scalars.

Equations
@[simp]
theorem category_theory.Module.restrict_coextend_scalars_adj_hom_equiv_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (X : Module S) (Y : Module R) (g : Y) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : Y) (x : X) :

Given R-module X and S-module Y and a map g : (extend_scalars f).obj X ⟶ Y, i.e. S-linear map S ⨂ X → Y, there is a X ⟶ (restrict_scalars f).obj Y, i.e. R-linear map X ⟶ Y by x ↦ g (1 ⊗ x).

Equations

Given R-module X and S-module Y and a map X ⟶ (restrict_scalars f).obj Y, i.e R-linear map X ⟶ Y, there is a map (extend_scalars f).obj X ⟶ Y, i.e S-linear map S ⨂ X → Y by s ⊗ x ↦ s • g x.

Equations
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X ) (z : ) :
= (tensor_product.lift {to_fun := λ (s : , {to_fun := λ (x : X), s g x, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}) z
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv_symm_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X ) :
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : Y) :
def category_theory.Module.extend_restrict_scalars_adj.hom_equiv {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} :

Given R-module X and S-module Y, S-linear linear maps (extend_scalars f).obj X ⟶ Y bijectively correspond to R-linear maps X ⟶ (restrict_scalars f).obj Y.

Equations

For any R-module X, there is a natural R-linear map from X to X ⨂ S by sending x ↦ x ⊗ 1

Equations
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.unit.map_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} (x : X) :
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.unit_app {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (_x : Module R) :

The natural transformation from identity functor on R-module to the composition of extension and restriction of scalars.

Equations

For any S-module Y, there is a natural R-linear map from S ⨂ Y to Y by s ⊗ y ↦ s • y

Equations
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.counit.map_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {Y : Module S} (ᾰ : Y) :
= (tensor_product.lift {to_fun := λ (s : S), {to_fun := λ (y : Y), s y, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _})

The natural transformation from the composition of restriction and extension of scalars to the identity functor on S-module.

Equations
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj.counit_app {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (_x : Module S) :
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj_hom_equiv {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (_x : Module R) (_x_1 : Module S) :
def category_theory.Module.extend_restrict_scalars_adj {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

Given commutative rings R, S and a ring hom f : R →+* S, the extension and restriction of scalars by f are adjoint to each other.

Equations
@[simp]
theorem category_theory.Module.extend_restrict_scalars_adj_unit {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations