# Change Of Rings #

## Main definitions #

• ModuleCat.restrictScalars: given rings R, S and a ring homomorphism R ⟶ S, then restrictScalars : ModuleCat S ⥤ ModuleCat R is defined by M ↦ M where an S-module M is seen as an R-module by r • m := f r • m and S-linear map l : M ⟶ M' is R-linear as well.

• ModuleCat.extendScalars: given commutative rings R, S and ring homomorphism f : R ⟶ S, then extendScalars : ModuleCat R ⥤ ModuleCat S is defined by M ↦ S ⨂ M where the module structure is defined by s • (s' ⊗ m) := (s * s') ⊗ m and R-linear map l : M ⟶ M' is sent to S-linear map s ⊗ m ↦ s ⊗ l m : S ⨂ M ⟶ S ⨂ M'.

• ModuleCat.coextendScalars: given rings R, S and a ring homomorphism R ⟶ S then coextendScalars : ModuleCat R ⥤ ModuleCat S is defined by M ↦ (S →ₗ[R] M) where S is seen as an R-module by restriction of scalars and l ↦ l ∘ _.

## Main results #

• ModuleCat.extendRestrictScalarsAdj: given commutative rings R, S and a ring homomorphism f : R →+* S, the extension and restriction of scalars by f are adjoint functors.
• ModuleCat.restrictCoextendScalarsAdj: given rings R, S and a ring homomorphism f : R ⟶ S then coextendScalars f is the right adjoint of restrictScalars f.

## List of notations #

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

• if M is an R-module, s : S and m : M, then s ⊗ₜ[R, f] m is the pure tensor s ⊗ m : S ⊗[R, f] M.
noncomputable def ModuleCat.RestrictScalars.obj' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (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
Instances For
noncomputable def ModuleCat.RestrictScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } {M' : } (g : M M') :

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
Instances For
noncomputable def ModuleCat.restrictScalars {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
• = { obj := , map := fun {X Y : } => , map_id := , map_comp := }
Instances For
noncomputable instance ModuleCat.instFaithfulRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
.Faithful
Equations
• =
noncomputable instance ModuleCat.instPreservesMonomorphismsRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
.PreservesMonomorphisms
Equations
• =
noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : } :
Module R (.obj M)
Equations
• ModuleCat.instModuleCarrierObjRestrictScalars =
noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars_1 {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : } :
Module S (.obj M)
Equations
@[simp]
theorem ModuleCat.restrictScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } {M' : } (g : M M') (x : (.obj M)) :
(.map g) x = g x
@[simp]
theorem ModuleCat.restrictScalars.smul_def {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } (r : R) (m : (.obj M)) :
r m = f r m
theorem ModuleCat.restrictScalars.smul_def' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } (r : R) (m : M) :
let m' := m; r m' = f r m
@[instance 100]
noncomputable instance ModuleCat.sMulCommClass_mk {R : Type u₁} {S : Type u₂} [Ring R] [] (f : R →+* S) (M : Type v) [I : ] [Module S M] :
Equations
• =
noncomputable def ModuleCat.semilinearMapAddEquiv {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) (N : ) :
(M →ₛₗ[f] N) ≃+ (M .obj N)

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
@[simp]
theorem ModuleCat.semilinearMapAddEquiv_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) (N : ) (g : M →ₛₗ[f] N) (a : M) :
( g) a = g a
@[simp]
theorem ModuleCat.semilinearMapAddEquiv_symm_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) (N : ) (g : M .obj N) (a : M) :
(.symm g) a = g a
noncomputable def ModuleCat.restrictScalarsId'App {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) (M : ) :
.obj M M

For a R-module M, the restriction of scalars of M by the identity morphisms identifies to M.

Equations
Instances For
theorem ModuleCat.restrictScalarsId'App_hom_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) (M : ) (x : M) :
.hom x = x
theorem ModuleCat.restrictScalarsId'App_inv_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) (M : ) (x : M) :
.inv x = x
noncomputable def ModuleCat.restrictScalarsId' {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) :

The restriction of scalars by a ring morphism that is the identity identify to the identity functor.

Equations
Instances For
@[simp]
theorem ModuleCat.restrictScalarsId'_inv_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) (X : ) :
.inv.app X = .inv
@[simp]
theorem ModuleCat.restrictScalarsId'_hom_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) (X : ) :
.hom.app X = .hom
theorem ModuleCat.restrictScalarsId'App_hom_naturality_assoc {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) {M : } {N : } (φ : M N) {Z : } (h : N Z) :
=
theorem ModuleCat.restrictScalarsId'App_hom_naturality {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) {M : } {N : } (φ : M N) :
theorem ModuleCat.restrictScalarsId'App_inv_naturality_assoc {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) {M : } {N : } (φ : M N) {Z : } (h : .obj N Z) :
=
theorem ModuleCat.restrictScalarsId'App_inv_naturality {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = ) {M : } {N : } (φ : M N) :
@[reducible, inline]
noncomputable abbrev ModuleCat.restrictScalarsId (R : Type u₁) [Ring R] :

The restriction of scalars by the identity morphisms identify to the identity functor.

Equations
Instances For
noncomputable def ModuleCat.restrictScalarsComp'App {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ) :
.obj M .obj (.obj M)

For each R₃-module M, restriction of scalars of M by a composition of ring morphisms identifies to successively restricting scalars.

Equations
Instances For
theorem ModuleCat.restrictScalarsComp'App_hom_apply {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ) (x : M) :
(ModuleCat.restrictScalarsComp'App f g gf hgf M).hom x = x
theorem ModuleCat.restrictScalarsComp'App_inv_apply {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ) (x : M) :
(ModuleCat.restrictScalarsComp'App f g gf hgf M).inv x = x
noncomputable def ModuleCat.restrictScalarsComp' {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) :

The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.

Equations
Instances For
@[simp]
theorem ModuleCat.restrictScalarsComp'_inv_app {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (X : ) :
(ModuleCat.restrictScalarsComp' f g gf hgf).inv.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).inv
@[simp]
theorem ModuleCat.restrictScalarsComp'_hom_app {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (X : ) :
(ModuleCat.restrictScalarsComp' f g gf hgf).hom.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).hom
theorem ModuleCat.restrictScalarsComp'App_hom_naturality_assoc {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : } {N : } (φ : M N) {Z : } (h : .obj (.obj N) Z) :
theorem ModuleCat.restrictScalarsComp'App_hom_naturality {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : } {N : } (φ : M N) :
theorem ModuleCat.restrictScalarsComp'App_inv_naturality_assoc {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : } {N : } (φ : M N) {Z : } (h : .obj N Z) :
theorem ModuleCat.restrictScalarsComp'App_inv_naturality {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : } {N : } (φ : M N) :
@[reducible, inline]
noncomputable abbrev ModuleCat.restrictScalarsComp {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) :
ModuleCat.restrictScalars (g.comp f) .comp

The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.

Equations
Instances For
noncomputable def ModuleCat.restrictScalarsEquivalenceOfRingEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) :

The equivalence of categories ModuleCat S ≌ ModuleCat R induced by e : R ≃+* S.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance ModuleCat.restrictScalars_isEquivalence_of_ringEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) :
(ModuleCat.restrictScalars e.toRingHom).IsEquivalence
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def ModuleCat.ExtendScalars.obj' {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) (M : ) :

Extension of scalars turn an R-module into S-module by M ↦ S ⨂ M

Equations
Instances For
noncomputable def ModuleCat.ExtendScalars.map' {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {M1 : } {M2 : } (l : M1 M2) :

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
theorem ModuleCat.ExtendScalars.map'_id {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {M : } :
theorem ModuleCat.ExtendScalars.map'_comp {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {M₁ : } {M₂ : } {M₃ : } (l₁₂ : M₁ M₂) (l₂₃ : M₂ M₃) :
noncomputable def ModuleCat.extendScalars {R : Type u₁} {S : Type u₂} [] [] (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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ModuleCat.ExtendScalars.smul_tmul {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {M : } (s : S) (s' : S) (m : M) :
s s' ⊗ₜ[R] m = (s * s') ⊗ₜ[R] m
@[simp]
theorem ModuleCat.ExtendScalars.map_tmul {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {M : } {M' : } (g : M M') (s : S) (m : M) :
(.map g) (s ⊗ₜ[R] m) = s ⊗ₜ[R] g m
noncomputable instance ModuleCat.CoextendScalars.hasSMul {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [] [Module R M] :
SMul S ((.obj (ModuleCat.mk S)) →ₗ[R] M)

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.
@[simp]
theorem ModuleCat.CoextendScalars.smul_apply' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [] [Module R M] (s : S) (g : (.obj (ModuleCat.mk S)) →ₗ[R] M) (s' : S) :
(s g) s' = g (s' * s)
noncomputable instance ModuleCat.CoextendScalars.mulAction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [] [Module R M] :
MulAction S ((.obj (ModuleCat.mk S)) →ₗ[R] M)
Equations
• = let __src := ;
noncomputable instance ModuleCat.CoextendScalars.distribMulAction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [] [Module R M] :
Equations
• = let __src := ;
noncomputable instance ModuleCat.CoextendScalars.isModule {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [] [Module R M] :
Module S ((.obj (ModuleCat.mk S)) →ₗ[R] M)

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
• = let __src := ;
noncomputable def ModuleCat.CoextendScalars.obj' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) :

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
noncomputable instance ModuleCat.CoextendScalars.instCoeFunCarrierObj'Forall {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) :
CoeFun fun (x : ) => SM
Equations
• = { coe := fun (g : ) => g.toFun }
noncomputable def ModuleCat.CoextendScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } {M' : } (g : M M') :

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
• = { toFun := fun (h : ) => g ∘ₗ h, map_add' := , map_smul' := }
Instances For
@[simp]
theorem ModuleCat.CoextendScalars.map'_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } {M' : } (g : M M') (h : ) :
= g ∘ₗ h
noncomputable def ModuleCat.coextendScalars {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
• = { obj := , map := fun {X Y : } => , map_id := , map_comp := }
Instances For
noncomputable instance ModuleCat.CoextendScalars.instCoeFunCarrierObjCoextendScalarsForall {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) :
CoeFun (.obj M) fun (x : (.obj M)) => SM
Equations
• One or more equations did not get rendered due to their size.
theorem ModuleCat.CoextendScalars.smul_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ) (g : (.obj M)) (s : S) (s' : S) :
(s g).toFun s' = g.toFun (s' * s)
@[simp]
theorem ModuleCat.CoextendScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : } {M' : } (g : M M') (x : (.obj M)) (s : S) :
((.map g) x).toFun s = g (x.toFun s)
noncomputable def ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : } {Y : } (g : .obj Y X) :
Y .obj X

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
@[simp]
theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : } {Y : } (g : .obj Y X) (y : Y) (s : S) :
= g (s y)
noncomputable def ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : } {Y : } (g : Y .obj X) :
.obj Y X

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
• = { toFun := fun (y : Y) => (g y).toFun 1, map_add' := , map_smul' := }
Instances For
@[simp]
theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : } {Y : } (g : Y .obj X) (y : Y) :
= (g y).toFun 1
noncomputable def ModuleCat.RestrictionCoextensionAdj.app' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (Y : ) :
Y →ₗ[S] ((.comp ).obj Y)

Auxiliary definition for unit'

Equations
• = { toFun := fun (y : Y) => { toFun := fun (s : S) => s y, map_add' := , map_smul' := }, map_add' := , map_smul' := }
Instances For
noncomputable def ModuleCat.RestrictionCoextensionAdj.unit' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :

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

Equations
• = { app := fun (Y : ) => , naturality := }
Instances For
noncomputable def ModuleCat.RestrictionCoextensionAdj.counit' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :

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
noncomputable def ModuleCat.restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :

Restriction of scalars is left adjoint to coextension of scalars.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance ModuleCat.instIsLeftAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
Equations
• =
noncomputable instance ModuleCat.instIsRightAdjointCoextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
Equations
• =
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (g : .obj X Y) :
X .obj Y

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
• = { toFun := fun (x : X) => g (1 ⊗ₜ[R] x), map_add' := , map_smul' := }
Instances For
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_apply {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (g : .obj X Y) (x : X) :
= g (1 ⊗ₜ[R] x)
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (s : S) (g : X .obj Y) :
let_fun this := Module.compHom (↑Y) f; X →ₗ[R] Y

The map S → X →ₗ[R] Y given by fun s x => s • (g x)

Equations
• = { toFun := fun (x : X) => s g x, map_add' := , map_smul' := }
Instances For
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (s : S) (g : X .obj Y) (x : X) :
= s g x
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (g : X .obj Y) :
.obj X Y

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
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_apply {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (g : X .obj Y) (z : (.obj X)) :
= (TensorProduct.lift { toFun := fun (s : (.obj (ModuleCat.mk S))) => , map_add' := , map_smul' := }) z
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.homEquiv {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } :
(.obj X Y) (X .obj Y)

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
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } {Y : } (g : X .obj Y) :
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.Unit.map {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {X : } :
X (.comp ).obj X

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

Equations
• = { toFun := fun (x : X) => 1 ⊗ₜ[R] x, map_add' := , map_smul' := }
Instances For
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.unit {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) :

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

Equations
• = { app := fun (x : ) => , naturality := }
Instances For
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.unit_app {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) :
∀ (x : ),
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.Counit.map {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {Y : } :
(.comp ).obj Y Y

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
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.Counit.map_apply {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) {Y : } (a : TensorProduct R S Y) :
= (TensorProduct.lift { toFun := fun (s : S) => { toFun := fun (y : Y) => s y, map_add' := , map_smul' := }, map_add' := , map_smul' := }) a
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.counit {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) :

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

Equations
• = { app := fun (x : ) => , naturality := }
Instances For
@[simp]
theorem ModuleCat.ExtendRestrictScalarsAdj.counit_app {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) :
noncomputable def ModuleCat.extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) :

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.
Instances For
noncomputable instance ModuleCat.instIsLeftAdjointExtendScalars {R : Type u₁} {S : Type u₂} [] [] (f : R →+* S) :