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} [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' := ⋯ }

@[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) : ↑(Submodule.restrictScalars S V) = ↑V

@[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) : (Submodule.restrictScalars S V).toAddSubmonoid = V.toAddSubmonoid

@[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 ∈ Submodule.restrictScalars S V ↔ m ∈ V

@[simp]

theorem Submodule.restrictScalars_self {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (V : Submodule R M) : Submodule.restrictScalars R V = V

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 (Submodule.restrictScalars S)

@[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₁ : Submodule R M} {V₂ : Submodule R M} : Submodule.restrictScalars S V₁ = Submodule.restrictScalars S V₂ ↔ V₁ = V₂

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 ↥(Submodule.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

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 ↥(Submodule.restrictScalars S p)

Equations

• ⋯ = ⋯

@[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) : (Submodule.restrictScalarsEmbedding S R M) V = Submodule.restrictScalars S V

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' := ⋯ }

@[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), (Submodule.restrictScalarsEquiv S R M p) a = a

@[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), (Submodule.restrictScalarsEquiv S R M p).symm a = a

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) : ↥(Submodule.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 = let __src := AddEquiv.refl ↥p; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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] : Submodule.restrictScalars S ⊥ = ⊥

@[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} : Submodule.restrictScalars S p = ⊥ ↔ p = ⊥

@[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] : Submodule.restrictScalars S ⊤ = ⊤

@[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} : Submodule.restrictScalars S p = ⊤ ↔ p = ⊤

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' := ⋯ }