mathlib3 documentation

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 #

Main results #

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
Instances for category_theory.Module.restrict_scalars
@[simp]
@[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
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
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) :
@[protected, instance]

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) [add_comm_monoid M] [module R M] (s : S) (g : ((category_theory.Module.restrict_scalars f).obj (Module.mk S)) →ₗ[R] M) (s' : S) :
(s g) s' = g (s' * s)
@[protected, instance]

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'

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
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 : ((category_theory.Module.coextend_scalars f).obj M)) (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 : ((category_theory.Module.coextend_scalars f).obj M)) (s : S) :

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

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

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

Equations
@[protected]

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

Equations

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

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

Equations

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

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

Equations