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.

def ModuleCat.RestrictScalars.obj' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat S) : ModuleCat R

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.

def ModuleCat.RestrictScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat S} {M' : ModuleCat S} (g : M ⟶ M') : ModuleCat.RestrictScalars.obj' f M ⟶ ModuleCat.RestrictScalars.obj' f 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.

def ModuleCat.restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.Functor (ModuleCat S) (ModuleCat R)

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

instance ModuleCat.instFaithfulModuleCatToRingModuleCategoryModuleCatToRingModuleCategoryRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Faithful (ModuleCat.restrictScalars f)

instance ModuleCat.instModuleCarrierObjModuleCatToQuiverToCategoryStructModuleCategoryModuleCatToQuiverToCategoryStructModuleCategoryToPrefunctorRestrictScalarsToSemiringToAddCommMonoidIsAddCommGroup {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : ModuleCat S} : Module R ↑((ModuleCat.restrictScalars f).obj M)

instance ModuleCat.instModuleCarrierObjModuleCatToQuiverToCategoryStructModuleCategoryModuleCatToQuiverToCategoryStructModuleCategoryToPrefunctorRestrictScalarsToSemiringToAddCommMonoidIsAddCommGroup_1 {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : ModuleCat S} : Module S ↑((ModuleCat.restrictScalars f).obj M)

@[simp]

theorem ModuleCat.restrictScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat S} {M' : ModuleCat S} (g : M ⟶ M') (x : ↑((ModuleCat.restrictScalars f).obj M)) : ↑((ModuleCat.restrictScalars f).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 : ModuleCat S} (r : R) (m : ↑((ModuleCat.restrictScalars f).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 : ModuleCat S} (r : R) (m : ↑M) : let m' := m; r • m' = ↑f r • m

instance ModuleCat.sMulCommClass_mk {R : Type u₁} {S : Type u₂} [Ring R] [CommRing S] (f : R →+* S) (M : Type v) [I : AddCommGroup M] [Module S M] : SMulCommClass R S M

@[simp]

theorem ModuleCat.semilinearMapAddEquiv_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S) (g : ↑M →ₛₗ[f] ↑N) (a : ↑M) : ↑(↑(ModuleCat.semilinearMapAddEquiv f M N) 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 : ModuleCat R) (N : ModuleCat S) (g : M ⟶ (ModuleCat.restrictScalars f).obj N) (a : ↑M) : ↑(↑(AddEquiv.symm (ModuleCat.semilinearMapAddEquiv f M N)) g) a = ↑g a

def ModuleCat.semilinearMapAddEquiv {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S) : (↑M →ₛₗ[f] ↑N) ≃+ (M ⟶ (ModuleCat.restrictScalars f).obj N)

Semilinear maps M →ₛₗ[f] N identify to morphisms M ⟶ (ModuleCat.restrictScalars f).obj N.

def ModuleCat.restrictScalarsId' {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) : ModuleCat.restrictScalars f ≅ CategoryTheory.Functor.id (ModuleCat R)

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

@[simp]

theorem ModuleCat.restrictScalarsId'_inv_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M) : ↑((ModuleCat.restrictScalarsId' f hf).inv.app M) x = x

@[simp]

theorem ModuleCat.restrictScalarsId'_hom_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M) : ↑((ModuleCat.restrictScalarsId' f hf).hom.app M) x = x

@[inline, reducible]

abbrev ModuleCat.restrictScalarsId (R : Type u₁) [Ring R] : ModuleCat.restrictScalars (RingHom.id R) ≅ CategoryTheory.Functor.id (ModuleCat R)

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

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 = RingHom.comp g f) : ModuleCat.restrictScalars gf ≅ CategoryTheory.Functor.comp (ModuleCat.restrictScalars g) (ModuleCat.restrictScalars f)

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

@[simp]

theorem ModuleCat.restrictScalarsComp'_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 = RingHom.comp g f) (M : ModuleCat R₃) (x : ↑M) : ↑((ModuleCat.restrictScalarsComp' f g gf hgf).hom.app M) x = x

@[simp]

theorem ModuleCat.restrictScalarsComp'_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 = RingHom.comp g f) (M : ModuleCat R₃) (x : ↑M) : ↑((ModuleCat.restrictScalarsComp' f g gf hgf).inv.app M) x = x

@[inline, reducible]

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 (RingHom.comp g f) ≅ CategoryTheory.Functor.comp (ModuleCat.restrictScalars g) (ModuleCat.restrictScalars f)

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

def ChangeOfRings.«term_⊗ₜ[_,_]_» : Lean.TrailingParserDescr

def ModuleCat.ExtendScalars.obj' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat R) : ModuleCat S

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

def ModuleCat.ExtendScalars.map' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M1 : ModuleCat R} {M2 : ModuleCat R} (l : M1 ⟶ M2) : ModuleCat.ExtendScalars.obj' f M1 ⟶ ModuleCat.ExtendScalars.obj' f 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

theorem ModuleCat.ExtendScalars.map'_id {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M : ModuleCat R} : ModuleCat.ExtendScalars.map' f (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (ModuleCat.ExtendScalars.obj' f M)

theorem ModuleCat.ExtendScalars.map'_comp {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M₁ : ModuleCat R} {M₂ : ModuleCat R} {M₃ : ModuleCat R} (l₁₂ : M₁ ⟶ M₂) (l₂₃ : M₂ ⟶ M₃) : ModuleCat.ExtendScalars.map' f (CategoryTheory.CategoryStruct.comp l₁₂ l₂₃) = CategoryTheory.CategoryStruct.comp (ModuleCat.ExtendScalars.map' f l₁₂) (ModuleCat.ExtendScalars.map' f l₂₃)

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

@[simp]

theorem ModuleCat.ExtendScalars.smul_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M : ModuleCat R} (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₂} [CommRing R] [CommRing S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') (s : S) (m : ↑M) : ↑((ModuleCat.extendScalars f).map g) (s ⊗ₜ[R] m) = s ⊗ₜ[R] ↑g m

instance ModuleCat.CoextendScalars.hasSMul {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : SMul S (↑((ModuleCat.restrictScalars f).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)

@[simp]

theorem ModuleCat.CoextendScalars.smul_apply' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] (s : S) (g : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M) (s' : S) : ↑(s • g) s' = ↑g (s' * s)

instance ModuleCat.CoextendScalars.mulAction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : MulAction S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M)

instance ModuleCat.CoextendScalars.distribMulAction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : DistribMulAction S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M)

instance ModuleCat.CoextendScalars.isModule {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : Module S (↑((ModuleCat.restrictScalars f).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).

def ModuleCat.CoextendScalars.obj' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) : ModuleCat S

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)

instance ModuleCat.CoextendScalars.instCoeFunCarrierObj'ForAllCarrier {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) : CoeFun ↑(ModuleCat.CoextendScalars.obj' f M) fun x => S → ↑M

@[simp]

theorem ModuleCat.CoextendScalars.map'_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') (h : ↑(ModuleCat.CoextendScalars.obj' f M)) : ↑(ModuleCat.CoextendScalars.map' f g) h = LinearMap.comp g h

def ModuleCat.CoextendScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') : ModuleCat.CoextendScalars.obj' f M ⟶ ModuleCat.CoextendScalars.obj' f 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

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

instance ModuleCat.CoextendScalars.instCoeFunCarrierObjModuleCatToQuiverToCategoryStructModuleCategoryModuleCatToQuiverToCategoryStructModuleCategoryToPrefunctorCoextendScalarsForAllCarrier {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) : CoeFun ↑((ModuleCat.coextendScalars f).obj M) fun x => S → ↑M

theorem ModuleCat.CoextendScalars.smul_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (g : ↑((ModuleCat.coextendScalars f).obj M)) (s : S) (s' : S) : AddHom.toFun (s • g).toAddHom s' = AddHom.toFun g.toAddHom (s' * s)

@[simp]

theorem ModuleCat.CoextendScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') (x : ↑((ModuleCat.coextendScalars f).obj M)) (s : S) : AddHom.toFun (↑((ModuleCat.coextendScalars f).map g) x).toAddHom s = ↑g (AddHom.toFun x.toAddHom s)

@[simp]

theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.restrictScalars f).obj Y ⟶ X) (y : ↑Y) (s : S) : ↑(↑(ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction f g) y) s = ↑g (s • y)

def ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.restrictScalars f).obj Y ⟶ X) : Y ⟶ (ModuleCat.coextendScalars f).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))

@[simp]

theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : Y ⟶ (ModuleCat.coextendScalars f).obj X) (y : ↑Y) : ↑(ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g) y = AddHom.toFun (↑g y).toAddHom 1

def ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : Y ⟶ (ModuleCat.coextendScalars f).obj X) : (ModuleCat.restrictScalars f).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

def ModuleCat.RestrictionCoextensionAdj.app' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (Y : ModuleCat S) : ↑Y →ₗ[S] ↑((CategoryTheory.Functor.comp (ModuleCat.restrictScalars f) (ModuleCat.coextendScalars f)).obj Y)

Auxiliary definition for unit'

def ModuleCat.RestrictionCoextensionAdj.unit' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.Functor.id (ModuleCat S) ⟶ CategoryTheory.Functor.comp (ModuleCat.restrictScalars f) (ModuleCat.coextendScalars f)

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

def ModuleCat.RestrictionCoextensionAdj.counit' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.Functor.comp (ModuleCat.coextendScalars f) (ModuleCat.restrictScalars f) ⟶ CategoryTheory.Functor.id (ModuleCat R)

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

def ModuleCat.restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : ModuleCat.restrictScalars f ⊣ ModuleCat.coextendScalars f

Restriction of scalars is left adjoint to coextension of scalars.

instance ModuleCat.instIsLeftAdjointModuleCatModuleCategoryModuleCatModuleCategoryRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.IsLeftAdjoint (ModuleCat.restrictScalars f)

instance ModuleCat.instIsRightAdjointModuleCatModuleCategoryModuleCatModuleCategoryCoextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.IsRightAdjoint (ModuleCat.coextendScalars f)

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.extendScalars f).obj X ⟶ Y) (x : ↑X) : ↑(ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g) x = ↑g (1 ⊗ₜ[R] x)

def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.extendScalars f).obj X ⟶ Y) : X ⟶ (ModuleCat.restrictScalars f).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).

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (s : S) (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) (x : ↑X) : ↑(ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) x = s • ↑g x

def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (s : S) (g : X ⟶ (ModuleCat.restrictScalars f).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)

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) (z : ↑((ModuleCat.extendScalars f).obj X)) : ↑(ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g) z = ↑(TensorProduct.lift { toAddHom := { toFun := fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := (_ : ∀ (s₁ s₂ : S), (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) (s₁ + s₂) = (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₁ + (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₂) }, map_smul' := (_ : ∀ (r : R) (s : S), AddHom.toFun { toFun := fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := (_ : ∀ (s₁ s₂ : S), (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) (s₁ + s₂) = (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₁ + (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₂) } (r • s) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := (_ : ∀ (s₁ s₂ : S), (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) (s₁ + s₂) = (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₁ + (fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₂) } s) }) z

def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) : (ModuleCat.extendScalars f).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.

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) : ↑(ModuleCat.ExtendRestrictScalarsAdj.homEquiv f).symm g = ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g

def ModuleCat.ExtendRestrictScalarsAdj.homEquiv {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} : ((ModuleCat.extendScalars f).obj X ⟶ Y) ≃ (X ⟶ (ModuleCat.restrictScalars f).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.

def ModuleCat.ExtendRestrictScalarsAdj.Unit.map {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} : X ⟶ (CategoryTheory.Functor.comp (ModuleCat.extendScalars f) (ModuleCat.restrictScalars f)).obj X

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

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.unit_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : ∀ (x : ModuleCat R), (ModuleCat.ExtendRestrictScalarsAdj.unit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Unit.map f

def ModuleCat.ExtendRestrictScalarsAdj.unit {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Functor.id (ModuleCat R) ⟶ CategoryTheory.Functor.comp (ModuleCat.extendScalars f) (ModuleCat.restrictScalars f)

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

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.Counit.map_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {Y : ModuleCat S} (a : TensorProduct R S ↑Y) : ↑(ModuleCat.ExtendRestrictScalarsAdj.Counit.map f) a = ↑(TensorProduct.lift { toAddHom := { toFun := fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }, map_add' := (_ : ∀ (s₁ s₂ : S), (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) (s₁ + s₂) = (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) s₁ + (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) s₂) }, map_smul' := (_ : ∀ (r : R) (s : S), AddHom.toFun { toFun := fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }, map_add' := (_ : ∀ (s₁ s₂ : S), (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) (s₁ + s₂) = (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) s₁ + (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) s₂) } (r • s) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }, map_add' := (_ : ∀ (s₁ s₂ : S), (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) (s₁ + s₂) = (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) s₁ + (fun s => { toAddHom := { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := fun r y => (_ : AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } (r • y) = ↑(RingHom.id R) r • AddHom.toFun { toFun := fun y => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) } y) }) s₂) } s) }) a

def ModuleCat.ExtendRestrictScalarsAdj.Counit.map {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {Y : ModuleCat S} : (CategoryTheory.Functor.comp (ModuleCat.restrictScalars f) (ModuleCat.extendScalars f)).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

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.counit_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : ∀ (x : ModuleCat S), (ModuleCat.ExtendRestrictScalarsAdj.counit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Counit.map f

def ModuleCat.ExtendRestrictScalarsAdj.counit {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Functor.comp (ModuleCat.restrictScalars f) (ModuleCat.extendScalars f) ⟶ CategoryTheory.Functor.id (ModuleCat S)

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

def ModuleCat.extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : ModuleCat.extendScalars f ⊣ ModuleCat.restrictScalars f

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.

instance ModuleCat.instIsLeftAdjointModuleCatToRingModuleCategoryModuleCatToRingModuleCategoryExtendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.IsLeftAdjoint (ModuleCat.extendScalars f)

instance ModuleCat.instIsRightAdjointModuleCatToRingModuleCategoryModuleCatToRingModuleCategoryRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.IsRightAdjoint (ModuleCat.restrictScalars f)