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 : 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.

Equations

• ModuleCat.RestrictScalars.obj' f M = ModuleCat.mk ↑M

noncomputable 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.

Equations

• ModuleCat.RestrictScalars.map' f g = { toAddHom := g.toAddHom, map_smul' := (_ : ∀ (r : R) (x : ↑M), g (f r • x) = f r • g x) }

noncomputable 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

Equations

• ModuleCat.restrictScalars f = CategoryTheory.Functor.mk { obj := ModuleCat.RestrictScalars.obj' f, map := fun {X Y : ModuleCat S} => ModuleCat.RestrictScalars.map' f }

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

Equations

• (_ : CategoryTheory.Faithful (ModuleCat.restrictScalars f)) = (_ : CategoryTheory.Faithful (ModuleCat.restrictScalars f))

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

Equations

• (_ : CategoryTheory.Functor.PreservesMonomorphisms (ModuleCat.restrictScalars f)) = (_ : CategoryTheory.Functor.PreservesMonomorphisms (ModuleCat.restrictScalars f))

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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).toPrefunctor.obj M)

Equations

• One or more equations did not get rendered due to their size.

@[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).toPrefunctor.obj M)) : ((ModuleCat.restrictScalars f).toPrefunctor.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).toPrefunctor.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

noncomputable 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

Equations

• (_ : SMulCommClass R S M) = (_ : SMulCommClass R S M)

noncomputable 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).toPrefunctor.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.

@[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).toPrefunctor.obj N) (a : ↑M) : ((AddEquiv.symm (ModuleCat.semilinearMapAddEquiv f M N)) g) a = g a

noncomputable 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.

Equations

• ModuleCat.restrictScalarsId' f hf = (_ : RingHom.id R = f) ▸ CategoryTheory.Iso.refl (ModuleCat.restrictScalars (RingHom.id R))

@[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]

noncomputable 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.

Equations

• ModuleCat.restrictScalarsId R = ModuleCat.restrictScalarsId' (RingHom.id R) (_ : RingHom.id R = RingHom.id R)

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 = 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.

Equations

• ModuleCat.restrictScalarsComp' f g gf hgf = (_ : RingHom.comp g f = gf) ▸ CategoryTheory.Iso.refl (ModuleCat.restrictScalars (RingHom.comp g f))

@[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]

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 (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.

Equations

• ModuleCat.restrictScalarsComp f g = ModuleCat.restrictScalarsComp' f g (RingHom.comp g f) (_ : RingHom.comp g f = RingHom.comp g f)

noncomputable instance ModuleCat.restrictScalarsIsEquivalenceOfRingEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) : CategoryTheory.IsEquivalence (ModuleCat.restrictScalars (RingEquiv.toRingHom e))

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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

Equations

• ModuleCat.ExtendScalars.obj' f M = ModuleCat.mk (TensorProduct R ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S)) ↑M)

noncomputable 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

Equations

• ModuleCat.ExtendScalars.map' f l = LinearMap.baseChange S l

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₂₃)

noncomputable 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

Equations

• One or more equations did not get rendered due to their size.

@[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).toPrefunctor.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) [AddCommMonoid M] [Module R M] : SMul S (↑((ModuleCat.restrictScalars f).toPrefunctor.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) [AddCommMonoid M] [Module R M] (s : S) (g : ↑((ModuleCat.restrictScalars f).toPrefunctor.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) [AddCommMonoid M] [Module R M] : MulAction S (↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S)) →ₗ[R] M)

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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).toPrefunctor.obj (ModuleCat.mk S)) →ₗ[R] M)

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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).toPrefunctor.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

• One or more equations did not get rendered due to their size.

noncomputable 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)

Equations

• ModuleCat.CoextendScalars.obj' f M = ModuleCat.mk (↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S)) →ₗ[R] ↑M)

noncomputable 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 : ↑(ModuleCat.CoextendScalars.obj' f M)) => S → ↑M

Equations

• ModuleCat.CoextendScalars.instCoeFunCarrierObj'ForAllCarrier f M = { coe := fun (g : ↑(ModuleCat.CoextendScalars.obj' f M)) => g.toFun }

noncomputable 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

Equations

• One or more equations did not get rendered due to their size.

@[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

noncomputable 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.

Equations

• ModuleCat.coextendScalars f = CategoryTheory.Functor.mk { obj := ModuleCat.CoextendScalars.obj' f, map := fun {X Y : ModuleCat R} => ModuleCat.CoextendScalars.map' f }

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

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 : ModuleCat R) (g : ↑((ModuleCat.coextendScalars f).toPrefunctor.obj M)) (s : S) (s' : S) : (s • g).toAddHom.toFun s' = g.toAddHom.toFun (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).toPrefunctor.obj M)) (s : S) : (((ModuleCat.coextendScalars f).toPrefunctor.map g) x).toAddHom.toFun s = g (x.toAddHom.toFun s)

noncomputable 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).toPrefunctor.obj Y ⟶ X) : Y ⟶ (ModuleCat.coextendScalars f).toPrefunctor.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.

@[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).toPrefunctor.obj Y ⟶ X) (y : ↑Y) (s : S) : ((ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction f g) y) s = g (s • y)

noncomputable 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).toPrefunctor.obj X) : (ModuleCat.restrictScalars f).toPrefunctor.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

• One or more equations did not get rendered due to their size.

@[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).toPrefunctor.obj X) (y : ↑Y) : (ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g) y = (g y).toAddHom.toFun 1

noncomputable 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)).toPrefunctor.obj Y)

Auxiliary definition for unit'

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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.

Equations

• ModuleCat.RestrictionCoextensionAdj.unit' f = CategoryTheory.NatTrans.mk fun (Y : ModuleCat S) => ModuleCat.RestrictionCoextensionAdj.app' f Y

noncomputable 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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ModuleCat.instIsLeftAdjointModuleCatModuleCategoryModuleCatModuleCategoryRestrictScalars f = { right := ModuleCat.coextendScalars f, adj := ModuleCat.restrictCoextendScalarsAdj f }

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

Equations

• ModuleCat.instIsRightAdjointModuleCatModuleCategoryModuleCatModuleCategoryCoextendScalars f = { left := ModuleCat.restrictScalars f, adj := ModuleCat.restrictCoextendScalarsAdj f }

noncomputable 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).toPrefunctor.obj X ⟶ Y) : X ⟶ (ModuleCat.restrictScalars f).toPrefunctor.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

• One or more equations did not get rendered due to their size.

@[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).toPrefunctor.obj X ⟶ Y) (x : ↑X) : (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g) x = g (1 ⊗ₜ[R] x)

noncomputable 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).toPrefunctor.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

• One or more equations did not get rendered due to their size.

@[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).toPrefunctor.obj Y) (x : ↑X) : (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) x = s • g x

noncomputable 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).toPrefunctor.obj Y) : (ModuleCat.extendScalars f).toPrefunctor.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.

@[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).toPrefunctor.obj Y) (z : ↑((ModuleCat.extendScalars f).toPrefunctor.obj X)) : (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g) z = (TensorProduct.lift { toAddHom := { toFun := fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := (_ : ∀ (s₁ s₂ : S), (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) (s₁ + s₂) = (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₁ + (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₂) }, map_smul' := (_ : ∀ (r : R) (s : S), { toFun := fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := (_ : ∀ (s₁ s₂ : S), (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) (s₁ + s₂) = (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₁ + (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₂) }.toFun (r • s) = (RingHom.id R) r • { toFun := fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := (_ : ∀ (s₁ s₂ : S), (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) (s₁ + s₂) = (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₁ + (fun (s : ↑((ModuleCat.restrictScalars f).toPrefunctor.obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) s₂) }.toFun s) }) z

noncomputable 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).toPrefunctor.obj X ⟶ Y) ≃ (X ⟶ (ModuleCat.restrictScalars f).toPrefunctor.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.

@[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).toPrefunctor.obj Y) : (ModuleCat.ExtendRestrictScalarsAdj.homEquiv f).symm g = ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g

noncomputable 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)).toPrefunctor.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

• One or more equations did not get rendered due to their size.

noncomputable 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.

Equations

• ModuleCat.ExtendRestrictScalarsAdj.unit f = CategoryTheory.NatTrans.mk fun (x : ModuleCat R) => ModuleCat.ExtendRestrictScalarsAdj.Unit.map f

@[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

noncomputable 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)).toPrefunctor.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.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 : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }, map_add' := (_ : ∀ (s₁ s₂ : S), (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) (s₁ + s₂) = (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) s₁ + (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) s₂) }, map_smul' := (_ : ∀ (r : R) (s : S), { toFun := fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }, map_add' := (_ : ∀ (s₁ s₂ : S), (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) (s₁ + s₂) = (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) s₁ + (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) s₂) }.toFun (r • s) = (RingHom.id R) r • { toFun := fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }, map_add' := (_ : ∀ (s₁ s₂ : S), (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) (s₁ + s₂) = (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) s₁ + (fun (s : S) => { toAddHom := { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }, map_smul' := (_ : ∀ (r : R) (y : ↑Y), { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun (r • y) = (RingHom.id R) r • { toFun := fun (y : ↑Y) => s • y, map_add' := (_ : ∀ (b₁ b₂ : ↑Y), s • (b₁ + b₂) = s • b₁ + s • b₂) }.toFun y) }) s₂) }.toFun s) }) a

noncomputable 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.

Equations

• ModuleCat.ExtendRestrictScalarsAdj.counit f = CategoryTheory.NatTrans.mk fun (x : ModuleCat S) => ModuleCat.ExtendRestrictScalarsAdj.Counit.map f

@[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

noncomputable 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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ModuleCat.instIsLeftAdjointModuleCatToRingModuleCategoryModuleCatToRingModuleCategoryExtendScalars f = { right := ModuleCat.restrictScalars f, adj := ModuleCat.extendRestrictScalarsAdj f }

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

Equations

• ModuleCat.instIsRightAdjointModuleCatToRingModuleCategoryModuleCatToRingModuleCategoryRestrictScalars f = { left := ModuleCat.extendScalars f, adj := ModuleCat.extendRestrictScalarsAdj f }