mathlib documentation

algebra.category.Module.change_of_rings

Change Of Rings #

Main definitions #

List of notations #

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

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

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 : ((category_theory.Module.restrict_scalars f).obj 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 : ((category_theory.Module.restrict_scalars f).obj 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) [add_comm_group M] [module S 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

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