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.
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
- ModuleCat.RestrictScalars.map' f g = { toAddHom := g.toAddHom, map_smul' := ⋯ }
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
Equations
- ModuleCat.restrictScalars f = { obj := ModuleCat.RestrictScalars.obj' f, map := fun {X Y : ModuleCat S} => ModuleCat.RestrictScalars.map' f, map_id := ⋯, map_comp := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ModuleCat.instModuleCarrierObjRestrictScalars = inferInstanceAs (Module R ↑(ModuleCat.RestrictScalars.obj' f M))
Equations
- ModuleCat.instModuleCarrierObjRestrictScalars_1 = inferInstanceAs (Module S ↑M)
Equations
- ⋯ = ⋯
Semilinear maps M →ₛₗ[f] N
identify to
morphisms M ⟶ (ModuleCat.restrictScalars f).obj N
.
Equations
- One or more equations did not get rendered due to their size.
For a R
-module M
, the restriction of scalars of M
by the identity morphisms identifies
to M
.
Equations
- ModuleCat.restrictScalarsId'App f hf M = ((AddEquiv.refl ↑((ModuleCat.restrictScalars f).obj M)).toLinearEquiv ⋯).toModuleIso'
The restriction of scalars by a ring morphism that is the identity identify to the identity functor.
Equations
- ModuleCat.restrictScalarsId' f hf = CategoryTheory.NatIso.ofComponents (fun (M : ModuleCat R) => ModuleCat.restrictScalarsId'App f hf M) ⋯
The restriction of scalars by the identity morphisms identify to the identity functor.
Equations
For each R₃
-module M
, restriction of scalars of M
by a composition of ring morphisms
identifies to successively restricting scalars.
Equations
- ModuleCat.restrictScalarsComp'App f g gf hgf M = ((AddEquiv.refl ↑((ModuleCat.restrictScalars gf).obj M)).toLinearEquiv ⋯).toModuleIso'
The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.
Equations
- ModuleCat.restrictScalarsComp' f g gf hgf = CategoryTheory.NatIso.ofComponents (fun (M : ModuleCat R₃) => ModuleCat.restrictScalarsComp'App f g gf hgf M) ⋯
The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.
Equations
- ModuleCat.restrictScalarsComp f g = ModuleCat.restrictScalarsComp' f g (g.comp f) ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Extension of scalars turn an R
-module into S
-module by M ↦ S ⨂ M
Equations
- ModuleCat.ExtendScalars.obj' f M = ModuleCat.mk (TensorProduct R ↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) ↑M)
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Equations
Equations
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
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
- ModuleCat.CoextendScalars.obj' f M = ModuleCat.mk (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] ↑M)
Equations
- ModuleCat.CoextendScalars.instCoeFunCarrierObj'Forall f M = { coe := fun (g : ↑(ModuleCat.CoextendScalars.obj' f M)) => g.toFun }
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
- ModuleCat.CoextendScalars.map' f g = { toFun := fun (h : ↑(ModuleCat.CoextendScalars.obj' f M)) => g ∘ₗ h, map_add' := ⋯, map_smul' := ⋯ }
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
- ModuleCat.coextendScalars f = { obj := ModuleCat.CoextendScalars.obj' f, map := fun {X Y : ModuleCat R} => ModuleCat.CoextendScalars.map' f, map_id := ⋯, map_comp := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
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))
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g = { toFun := fun (y : ↑Y) => (g y).toFun 1, map_add' := ⋯, map_smul' := ⋯ }
Auxiliary definition for unit'
Equations
- ModuleCat.RestrictionCoextensionAdj.app' f Y = { toFun := fun (y : ↑Y) => { toFun := fun (s : S) => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
The natural transformation from identity functor to the composition of restriction and coextension of scalars.
Equations
- ModuleCat.RestrictionCoextensionAdj.unit' f = { app := fun (Y : ModuleCat S) => ModuleCat.RestrictionCoextensionAdj.app' f Y, naturality := ⋯ }
The natural transformation from the composition of coextension and restriction of scalars to identity functor.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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)
.
Equations
- ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g = { toFun := fun (x : ↑X) => g (1 ⊗ₜ[R] x), map_add' := ⋯, map_smul' := ⋯ }
The map S → X →ₗ[R] Y
given by fun s x => s • (g x)
Equations
- ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g = { toFun := fun (x : ↑X) => s • g x, map_add' := ⋯, map_smul' := ⋯ }
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
For any R
-module X, there is a natural R
-linear map from X
to X ⨂ S
by sending x ↦ x ⊗ 1
Equations
- ModuleCat.ExtendRestrictScalarsAdj.Unit.map f = { toFun := fun (x : ↑X) => 1 ⊗ₜ[R] x, map_add' := ⋯, map_smul' := ⋯ }
The natural transformation from identity functor on R
-module to the composition of extension and
restriction of scalars.
Equations
- ModuleCat.ExtendRestrictScalarsAdj.unit f = { app := fun (x : ModuleCat R) => ModuleCat.ExtendRestrictScalarsAdj.Unit.map f, naturality := ⋯ }
For any S
-module Y, there is a natural R
-linear map from S ⨂ Y
to Y
by
s ⊗ y ↦ s • y
Equations
- One or more equations did not get rendered due to their size.
The natural transformation from the composition of restriction and extension of scalars to the
identity functor on S
-module.
Equations
- ModuleCat.ExtendRestrictScalarsAdj.counit f = { app := fun (x : ModuleCat S) => ModuleCat.ExtendRestrictScalarsAdj.Counit.map f, naturality := ⋯ }
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
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯