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

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.

Instances For
    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') :

    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.

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

        Instances For

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

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

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

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

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

              Instances For
                @[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₃) :

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

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

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

                    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

                    Instances For
                      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₃) :

                      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

                      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' : 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] :

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

                        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)

                        Instances For
                          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 => SM
                          @[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)) :
                          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') :

                          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

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

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

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

                              Instances For
                                @[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) :
                                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

                                Instances For

                                  Auxiliary definition for unit'

                                  Instances For

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

                                    Instances For

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

                                      Instances For

                                        Restriction of scalars is left adjoint to coextension of scalars.

                                        Instances For

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

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

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

                                              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.

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

                                                Instances For

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

                                                  Instances For

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

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

                                                      For any S-module Y, there is a natural R-linear map from S ⨂ Y to Y by s ⊗ y ↦ s • y

                                                      Instances For

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

                                                        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.

                                                          Instances For