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

theorem Submodule.restrictScalars_le (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] {s t : Submodule R M} :

restrictScalars S s ≤ restrictScalars S t ↔ s ≤ t

source

theorem Submodule.restrictScalars_lt (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] {s t : Submodule R M} :

restrictScalars S s < restrictScalars S t ↔ s < t

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

theorem Submodule.restrictScalars_monotone (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] :

Monotone (restrictScalars S)

source

theorem Submodule.restrictScalars_mono (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] {s t : Submodule R M} (hst : s ≤ t) :

restrictScalars S s ≤ restrictScalars S t

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

@[simp]

theorem Submodule.restrictScalars_sInf (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] (s : Set (Submodule R M)) :

restrictScalars S (sInf s) = sInf (restrictScalars S '' s)

source

@[simp]

theorem Submodule.restrictScalars_sSup (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] (s : Set (Submodule R M)) :

restrictScalars S (sSup s) = sSup (restrictScalars S '' s)

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.restrictScalars_iInf (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] {ι : Sort u_4} (s : ι → Submodule R M) :

restrictScalars S (iInf s) = ⨅ (i : ι), restrictScalars S (s i)

source

@[simp]

theorem Submodule.restrictScalars_iSup (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] {ι : Sort u_4} (s : ι → Submodule R M) :

restrictScalars S (iSup s) = ⨆ (i : ι), restrictScalars S (s i)

source

@[simp]

theorem Submodule.restrictScalars_inf (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] (s t : Submodule R M) :

restrictScalars S (s ⊓ t) = restrictScalars S s ⊓ restrictScalars S t

source

@[simp]

theorem Submodule.restrictScalars_sup (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] (s t : Submodule R M) :

restrictScalars S (s ⊔ t) = restrictScalars S s ⊔ restrictScalars S t

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

Documentation

Mathlib.Algebra.Module.Submodule.RestrictScalars

Restriction of scalars for submodules #

Main definitions: #