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
Instances For
    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
    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
      Instances For
        instance ModuleCat.instFaithfulRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
        instance ModuleCat.instPreservesMonomorphismsRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
        (ModuleCat.restrictScalars f).PreservesMonomorphisms
        noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars {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).hom x = g.hom 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 let_fun this := m; this
        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) :
        (r let_fun this := m; this) = f r m
        @[instance 100]
        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] :
        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.
        Instances For
          @[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.hom a
          @[simp]
          theorem ModuleCat.semilinearMapAddEquiv_apply_hom_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).hom a = g a
          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
          Instances For
            @[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) :
            (ModuleCat.restrictScalarsId'App f hf M).hom.hom x = x
            @[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) :
            (ModuleCat.restrictScalarsId'App f hf M).inv.hom x = x

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

            Equations
            Instances For
              @[simp]
              theorem ModuleCat.restrictScalarsId'_hom_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R) :
              @[simp]
              theorem ModuleCat.restrictScalarsId'_inv_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
              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 : ModuleCat R₃) :

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

                Equations
                Instances For
                  @[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.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.hom 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 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
                    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
                        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
                        • 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₂} [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
                          Instances For
                            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
                            Instances For
                              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.
                              Instances For
                                @[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).hom (s ⊗ₜ[R] m) = s ⊗ₜ[R] g.hom 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.of S 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
                                Instances For
                                  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
                                  • One or more equations did not get rendered due to their size.
                                  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
                                  Instances For
                                    @[simp]
                                    theorem ModuleCat.CoextendScalars.map'_hom_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M M') (h : ((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] M) :
                                    (ModuleCat.CoextendScalars.map' f g).hom h = g.hom ∘ₗ 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
                                    Instances For
                                      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) s' = g (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).hom x) s = g.hom (x 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.
                                      Instances For
                                        @[simp]
                                        theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction_hom_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) :

                                        This should be autogenerated by @[simps] but we need to give s the correct type here.

                                        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
                                        Instances For
                                          @[simp]

                                          This should be autogenerated by @[simps] but we need to give 1 the correct type here.

                                          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
                                          Instances For

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

                                            Equations
                                            Instances For

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

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem ModuleCat.RestrictionCoextensionAdj.counit'_app_hom_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (X : ModuleCat R) (g : ((ModuleCat.restrictScalars f).obj ((ModuleCat.coextendScalars f).obj X))) :

                                                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
                                                  instance ModuleCat.instIsLeftAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
                                                  (ModuleCat.restrictScalars f).IsLeftAdjoint
                                                  instance ModuleCat.instIsRightAdjointCoextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
                                                  (ModuleCat.coextendScalars f).IsRightAdjoint
                                                  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
                                                  Instances For
                                                    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
                                                    Instances For
                                                      @[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.
                                                      Instances For
                                                        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.
                                                        Instances For
                                                          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
                                                          Instances For

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

                                                            Equations
                                                            Instances For
                                                              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.
                                                              Instances For
                                                                @[simp]
                                                                theorem ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_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).hom 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
                                                                Instances For

                                                                  Given commutative rings R, S and a ring hom f : R →+* S, the extension and restriction of scalars by f are adjoint to each other.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    instance ModuleCat.instIsLeftAdjointExtendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
                                                                    (ModuleCat.extendScalars f).IsLeftAdjoint
                                                                    instance ModuleCat.instIsRightAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
                                                                    (ModuleCat.restrictScalars f).IsRightAdjoint