# Restriction of scalars for submodules #

If semiring S acts on a semiring R and M is a module over both (compatibly with this action) then we can turn an R-submodule into an S-submodule by forgetting the action of R. We call this restriction of scalars for submodules.

## Main definitions: #

• Submodule.restrictScalars: regard an R-submodule as an S-submodule if S acts on R
def Submodule.restrictScalars (S : Type u_1) {R : Type u_2} {M : Type u_3} [] [] [] [Module S M] [Module R M] [SMul S R] [] (V : ) :

V.restrictScalars S is the S-submodule of the S-module given by restriction of scalars, corresponding to V, an R-submodule of the original R-module.

Equations
• = { carrier := V, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem Submodule.coe_restrictScalars (S : Type u_1) {R : Type u_2} {M : Type u_3} [] [] [] [Module S M] [Module R M] [SMul S R] [] (V : ) :
= V
@[simp]
theorem Submodule.toAddSubmonoid_restrictScalars (S : Type u_1) {R : Type u_2} {M : Type u_3} [] [] [] [Module S M] [Module R M] [SMul S R] [] (V : ) :
@[simp]
theorem Submodule.restrictScalars_mem (S : Type u_1) {R : Type u_2} {M : Type u_3} [] [] [] [Module S M] [Module R M] [SMul S R] [] (V : ) (m : M) :
m V
@[simp]
theorem Submodule.restrictScalars_self {R : Type u_2} {M : Type u_3} [] [] [Module R M] (V : ) :
theorem Submodule.restrictScalars_injective (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] :
@[simp]
theorem Submodule.restrictScalars_inj (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] {V₁ : } {V₂ : } :
V₁ = V₂
instance Submodule.restrictScalars.origModule (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
Module R

Even though p.restrictScalars S has type Submodule S M, it is still an R-module.

Equations
• = inferInstance
instance Submodule.restrictScalars.isScalarTower (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
Equations
• =
@[simp]
theorem Submodule.restrictScalarsEmbedding_apply (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] (V : ) :
def Submodule.restrictScalarsEmbedding (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] :

restrictScalars S is an embedding of the lattice of R-submodules into the lattice of S-submodules.

Equations
• = { toFun := , inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem Submodule.restrictScalarsEquiv_apply (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
∀ (a : p), a = a
@[simp]
theorem Submodule.restrictScalarsEquiv_symm_apply (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
∀ (a : p), .symm a = a
def Submodule.restrictScalarsEquiv (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
≃ₗ[R] p

Turning p : Submodule R M into an S-submodule gives the same module structure as turning it into a type and adding a module structure.

Equations
• = let __src := ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Submodule.restrictScalars_bot (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] :
@[simp]
theorem Submodule.restrictScalars_eq_bot_iff (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] {p : } :
p =
@[simp]
theorem Submodule.restrictScalars_top (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] :
@[simp]
theorem Submodule.restrictScalars_eq_top_iff (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] {p : } :
p =
def Submodule.restrictScalarsLatticeHom (S : Type u_1) (R : Type u_2) (M : Type u_3) [] [] [] [Module S M] [Module R M] [SMul S R] [] :

If ring S acts on a ring R and M is a module over both (compatibly with this action) then we can turn an R-submodule into an S-submodule by forgetting the action of R.

Equations
• = { toFun := , map_sInf' := , map_sSup' := }
Instances For