# 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`

source
def Submodule.restrictScalars (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
Submodule S M

`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

- Submodule.restrictScalars S V = { carrier := ↑V, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.coe_restrictScalars (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
↑(restrictScalars S V) = ↑V
source
@[simp]
theorem Submodule.toAddSubmonoid_restrictScalars (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
(restrictScalars S V).toAddSubmonoid = V.toAddSubmonoid
source
@[simp]
theorem Submodule.restrictScalars_mem (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) (m : M) :
m ∈ restrictScalars S V ↔ m ∈ V
source
@[simp]
theorem Submodule.restrictScalars_self {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (V : Submodule R M) :
restrictScalars R V = V
source
theorem Submodule.restrictScalars_injective (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :
Function.Injective (restrictScalars S)
source
@[simp]
theorem Submodule.restrictScalars_inj (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {V₁ V₂ : Submodule R M} :
restrictScalars S V₁ = restrictScalars S V₂ ↔ V₁ = V₂
source
instance Submodule.restrictScalars.origModule (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
Module R ↥(restrictScalars S p)

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

Equations

- Submodule.restrictScalars.origModule S R M p = inferInstance

source
instance Submodule.restrictScalars.isScalarTower (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
IsScalarTower S R ↥(restrictScalars S p)
source
def Submodule.restrictScalarsEmbedding (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :
Submodule R M ↪o Submodule S M

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

Equations

- Submodule.restrictScalarsEmbedding S R M = { toFun := Submodule.restrictScalars S, inj' := ⋯, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.restrictScalarsEmbedding_apply (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
(restrictScalarsEmbedding S R M) V = restrictScalars S V
source
def Submodule.restrictScalarsEquiv (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
↥(restrictScalars S 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

- Submodule.restrictScalarsEquiv S R M p = { toFun := (AddEquiv.refl ↥p).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (AddEquiv.refl ↥p).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Submodule.restrictScalarsEquiv_apply (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) (a✝ : ↥p) :
(restrictScalarsEquiv S R M p) a✝ = a✝
source
@[simp]
theorem Submodule.restrictScalarsEquiv_symm_apply (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) (a✝ : ↥p) :
(restrictScalarsEquiv S R M p).symm a✝ = a✝
source
@[simp]
theorem Submodule.restrictScalars_bot (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :
restrictScalars S ⊥ = ⊥
source
@[simp]
theorem Submodule.restrictScalars_eq_bot_iff (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} :
restrictScalars S p = ⊥ ↔ p = ⊥
source
@[simp]
theorem Submodule.restrictScalars_top (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :
restrictScalars S ⊤ = ⊤
source
@[simp]
theorem Submodule.restrictScalars_eq_top_iff (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} :
restrictScalars S p = ⊤ ↔ p = ⊤
source
def Submodule.restrictScalarsLatticeHom (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :
CompleteLatticeHom (Submodule R M) (Submodule S M)

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

- Submodule.restrictScalarsLatticeHom S R M = { toFun := Submodule.restrictScalars S, map_sInf' := ⋯, map_sSup' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.toIntSubmodule_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) :
AddSubgroup.toIntSubmodule N.toAddSubgroup = restrictScalars ℤ N