Documentation

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Change Of Rings #

Main definitions #

Main results #

List of notations #

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

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

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
noncomputable def ModuleCat.RestrictScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat S} (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
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
noncomputable instance ModuleCat.instFaithfulRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
Equations
  • =
noncomputable instance ModuleCat.instPreservesMonomorphismsRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
(ModuleCat.restrictScalars f).PreservesMonomorphisms
Equations
  • =
noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : ModuleCat S} :
Equations
noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars_1 {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : ModuleCat S} :
Equations
@[simp]
theorem ModuleCat.restrictScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M 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 100]
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] :
Equations
  • =
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).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_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) :
((ModuleCat.semilinearMapAddEquiv f M N).symm g) a = g a
@[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) :
noncomputable def ModuleCat.restrictScalarsId'App {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) :

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

Equations
@[simp]
theorem ModuleCat.restrictScalarsId'App_hom_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : M) :
@[simp]
theorem ModuleCat.restrictScalarsId'App_inv_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : M) :

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

Equations
@[simp]
theorem ModuleCat.restrictScalarsId'_inv_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R) :
@[simp]
theorem ModuleCat.restrictScalarsId'_hom_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R) :
@[reducible, inline]

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

Equations
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 : ModuleCat R₃) :

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

Equations
@[simp]
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 : ModuleCat R₃) (x : M) :
(ModuleCat.restrictScalarsComp'App f g gf hgf M).hom x = x
@[simp]
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 : ModuleCat R₃) (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
@[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 R₃) :
(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 R₃) :
(ModuleCat.restrictScalarsComp' f g gf hgf).hom.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).hom
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 : ModuleCat R₃} (φ : M N) :
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 : ModuleCat R₃} (φ : M N) {Z : ModuleCat R₁} (h : (ModuleCat.restrictScalars f).obj ((ModuleCat.restrictScalars g).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 : ModuleCat R₃} (φ : 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 : ModuleCat R₃} (φ : M N) {Z : ModuleCat R₁} (h : (ModuleCat.restrictScalars gf).obj N Z) :
@[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₃) :

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

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

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

Equations
noncomputable def ModuleCat.ExtendScalars.map' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M1 M2 : ModuleCat R} (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
theorem ModuleCat.ExtendScalars.map'_comp {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M₁ M₂ M₃ : ModuleCat R} (l₁₂ : M₁ M₂) (l₂₃ : M₂ M₃) :
noncomputable def ModuleCat.extendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (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.
@[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) (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 M' : ModuleCat R} (g : M M') (s : S) (m : M) :
((ModuleCat.extendScalars f).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] :

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).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] :
Equations
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] :

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

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
noncomputable instance ModuleCat.CoextendScalars.instCoeFunCarrierObj'Forall {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)) => SM
Equations
noncomputable def ModuleCat.CoextendScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat R} (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
@[simp]
theorem ModuleCat.CoextendScalars.map'_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M M') (h : (ModuleCat.CoextendScalars.obj' f M)) :
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
noncomputable instance ModuleCat.CoextendScalars.instCoeFunCarrierObjCoextendScalarsForall {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) :
CoeFun ((ModuleCat.coextendScalars f).obj M) fun (x : ((ModuleCat.coextendScalars f).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 : ModuleCat R) (g : ((ModuleCat.coextendScalars f).obj M)) (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' : ModuleCat R} (g : M M') (x : ((ModuleCat.coextendScalars f).obj M)) (s : S) :
(((ModuleCat.coextendScalars f).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 : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.restrictScalars f).obj Y 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]
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).obj 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
@[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) :
noncomputable def ModuleCat.RestrictionCoextensionAdj.app' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (Y : ModuleCat S) :

Auxiliary definition for unit'

Equations

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

Equations

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.

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.instIsLeftAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
(ModuleCat.restrictScalars f).IsLeftAdjoint
Equations
  • =
noncomputable instance ModuleCat.instIsRightAdjointCoextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
(ModuleCat.coextendScalars f).IsRightAdjoint
Equations
  • =
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).obj X 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
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).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
@[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) :
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).obj 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.
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.homEquiv {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} :

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

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

Equations

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

Equations
noncomputable def ModuleCat.ExtendRestrictScalarsAdj.Counit.map {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {Y : ModuleCat S} :

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.
@[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 { toFun := fun (s : S) => { toFun := fun (y : Y) => s y, map_add' := , map_smul' := }, map_add' := , map_smul' := }) a

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

Equations

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.instIsLeftAdjointExtendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
(ModuleCat.extendScalars f).IsLeftAdjoint
Equations
  • =
noncomputable instance ModuleCat.instIsRightAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
(ModuleCat.restrictScalars f).IsRightAdjoint
Equations
  • =