Documentation

Mathlib.Algebra.Module.Submodule.RestrictScalars

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

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

V.restrict_scalars 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 = { toAddSubmonoid := { toAddSubsemigroup := { 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} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
    @[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) :
    @[simp]
    theorem Submodule.restrictScalars_self {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (V : Submodule R M) :
    @[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} :
    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) :

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

    Equations
    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) :
    Equations
    • =
    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] :

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

    Equations
    Instances For
      @[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), (LinearEquiv.symm (Submodule.restrictScalarsEquiv S R M p)) 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) :

      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
      • One or more equations did not get rendered due to their size.
      Instances For
        @[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] :
        @[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} :
        @[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] :
        @[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} :
        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] :

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