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
- ModuleCat.RestrictScalars.obj' f M = ModuleCat.of R ↑M
Instances For
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 = ModuleCat.ofHom (let __src := g.hom; { toAddHom := __src.toAddHom, map_smul' := ⋯ })
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
Equations
- ModuleCat.restrictScalars f = { obj := ModuleCat.RestrictScalars.obj' f, map := fun {X Y : ModuleCat S} => ModuleCat.RestrictScalars.map' f, map_id := ⋯, map_comp := ⋯ }
Instances For
Equations
- ModuleCat.instModuleCarrierObjRestrictScalars = inferInstanceAs (Module S ↑M)
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.
Instances For
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
Instances For
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) ⋯
Instances For
The restriction of scalars by the identity morphisms identify to the identity functor.
Equations
Instances For
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
Instances For
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) ⋯
Instances For
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) ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extension of scalars turn an R
-module into S
-module by M ↦ S ⨂ M
Equations
- ModuleCat.ExtendScalars.obj' f M = ModuleCat.of S (TensorProduct R ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) ↑M)
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
Equations
- ModuleCat.ExtendScalars.map' f l = ModuleCat.ofHom (LinearMap.baseChange S l.hom)
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
Equations
- One or more equations did not get rendered due to their size.
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)
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.of S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] ↑M)
Instances For
Equations
- One or more equations did not get rendered due to their size.
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 = ModuleCat.ofHom { toFun := fun (h : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] ↑M) => g.hom ∘ₗ h, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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 := ⋯ }
Instances For
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.
Instances For
This should be autogenerated by @[simps]
but we need to give s
the correct type here.
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 = ModuleCat.ofHom { toFun := fun (y : ↑Y) => (g.hom y) 1, map_add' := ⋯, map_smul' := ⋯ }
Instances For
This should be autogenerated by @[simps]
but we need to give 1
the correct type here.
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' := ⋯ }
Instances For
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.ofHom (ModuleCat.RestrictionCoextensionAdj.app' f Y), naturality := ⋯ }
Instances For
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.
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)
.
Equations
- ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g = ModuleCat.ofHom { toFun := fun (x : ↑X) => g.hom (1 ⊗ₜ[R] x), map_add' := ⋯, map_smul' := ⋯ }
Instances For
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.hom x, map_add' := ⋯, map_smul' := ⋯ }
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 = ModuleCat.ofHom { toFun := fun (x : ↑X) => 1 ⊗ₜ[R] x, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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 := ⋯ }
Instances For
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.
Instances For
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 := ⋯ }
Instances For
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.