Change Of Rings #
Main definitions #
-
ModuleCat.restrictScalars
: given ringsR, S
and a ring homomorphismR ⟶ S
, thenrestrictScalars : ModuleCat S ⥤ ModuleCat R
is defined byM ↦ M
where anS
-moduleM
is seen as anR
-module byr • m := f r • m
andS
-linear mapl : M ⟶ M'
isR
-linear as well. -
ModuleCat.extendScalars
: given commutative ringsR, S
and ring homomorphismf : R ⟶ S
, thenextendScalars : ModuleCat R ⥤ ModuleCat 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'
. -
ModuleCat.coextendScalars
: given ringsR, S
and a ring homomorphismR ⟶ S
thencoextendScalars : ModuleCat R ⥤ ModuleCat S
is defined byM ↦ (S →ₗ[R] M)
whereS
is seen as anR
-module by restriction of scalars andl ↦ l ∘ _
.
Main results #
ModuleCat.extendRestrictScalarsAdj
: given commutative ringsR, S
and a ring homomorphismf : R →+* S
, the extension and restriction of scalars byf
are adjoint functors.ModuleCat.restrictCoextendScalarsAdj
: given ringsR, S
and a ring homomorphismf : R ⟶ S
thencoextendScalars f
is the right adjoint ofrestrictScalars f
.
List of notations #
Let R, S
be rings and f : R →+* S
- if
M
is anR
-module,s : S
andm : M
, thens ⊗ₜ[R, f] m
is the pure tensors ⊗ m : S ⊗[R, f] M
.
Any S
-module M is also an R
-module via a ring homomorphism f : R ⟶ S
by defining
r • m := f r • m
(Module.compHom
). This is called restriction of scalars.
Instances For
The restriction of scalars operation is functorial. For any f : R →+* S
a ring homomorphism,
- an
S
-moduleM
can be considered asR
-module byr • m = f r • m
- an
S
-linear map is alsoR
-linear
Instances For
Semilinear maps M →ₛₗ[f] N
identify to
morphisms M ⟶ (ModuleCat.restrictScalars f).obj N
.
Instances For
The restriction of scalars by a ring morphism that is the identity identify to the identity functor.
Instances For
The restriction of scalars by the identity morphisms identify to the identity functor.
Instances For
The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.
Instances For
The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.
Instances For
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
Instances For
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)
S
acts on Hom(S, M) by s • g = x ↦ g (x • s)
, this action defines an S
-module structure on
Hom(S, M).
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
.
Instances For
Given R
-module X and S
-module Y, any g : (restrictScalars f).obj Y ⟶ X
corresponds to Y ⟶ (coextendScalars f).obj X
by sending y ↦ (s ↦ g (s • y))
Instances For
Given R
-module X and S
-module Y, any g : Y ⟶ (coextendScalars f).obj X
corresponds to (restrictScalars f).obj Y ⟶ X
by y ↦ g y 1
Instances For
Auxiliary definition for unit'
Instances For
Given R
-module X and S
-module Y and a map g : (extendScalars f).obj X ⟶ Y
, i.e. S
-linear
map S ⨂ X → Y
, there is a X ⟶ (restrictScalars f).obj Y
, i.e. R
-linear map X ⟶ Y
by
x ↦ g (1 ⊗ x)
.
Instances For
The map S → X →ₗ[R] Y
given by fun s x => s • (g x)
Instances For
Given R
-module X and S
-module Y and a map X ⟶ (restrictScalars 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
.
Instances For
Given R
-module X and S
-module Y, S
-linear linear maps (extendScalars f).obj X ⟶ Y
bijectively correspond to R
-linear maps X ⟶ (restrictScalars f).obj Y
.
Instances For
For any R
-module X, there is a natural R
-linear map from X
to X ⨂ S
by sending x ↦ x ⊗ 1
Instances For
For any S
-module Y, there is a natural R
-linear map from S ⨂ Y
to Y
by
s ⊗ y ↦ s • y