Mathlib.Algebra.Module.Submodule.RestrictScalars

Submodule.restrictScalars definition

(V : Submodule R M) : Submodule S M

Full source

/-- `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.
-/
def restrictScalars (V : Submodule R M) : Submodule S M where
  carrier := V
  zero_mem' := V.zero_mem
  smul_mem' c _ h := V.smul_of_tower_mem c h
  add_mem' hx hy := V.add_mem hx hy

Restriction of scalars for submodules

Informal description

Given a semiring $S$ acting on a semiring $R$ and a module $M$ over both $R$ and $S$ (with compatible actions), the function `Submodule.restrictScalars` takes an $R$-submodule $V$ of $M$ and returns the corresponding $S$-submodule by forgetting the $R$-action. The resulting $S$-submodule has: 1. The same underlying set as $V$ 2. The same additive structure as $V$ 3. Scalar multiplication restricted to $S$-action only

Submodule.coe_restrictScalars theorem

(V : Submodule R M) : (V.restrictScalars S : Set M) = V

Full source

@[simp]
theorem coe_restrictScalars (V : Submodule R M) : (V.restrictScalars S : Set M) = V :=
  rfl

Underlying Set Preservation under Scalar Restriction

Informal description

For any $R$-submodule $V$ of $M$, the underlying set of the $S$-submodule obtained by restricting scalars from $R$ to $S$ is equal to $V$ itself. That is, $(V.\text{restrictScalars}\, S) = V$ as sets.

Submodule.toAddSubmonoid_restrictScalars theorem

(V : Submodule R M) : (V.restrictScalars S).toAddSubmonoid = V.toAddSubmonoid

Full source

@[simp]
theorem toAddSubmonoid_restrictScalars (V : Submodule R M) :
    (V.restrictScalars S).toAddSubmonoid = V.toAddSubmonoid :=
  rfl

Additive Submonoid Preservation Under Restriction of Scalars

Informal description

For any $R$-submodule $V$ of $M$, the underlying additive submonoid of the restricted $S$-submodule $V.\text{restrictScalars}\,S$ is equal to the underlying additive submonoid of $V$.

Submodule.restrictScalars_mem theorem

(V : Submodule R M) (m : M) : m ∈ V.restrictScalars S ↔ m ∈ V

Full source

@[simp]
theorem restrictScalars_mem (V : Submodule R M) (m : M) : m ∈ V.restrictScalars Sm ∈ V.restrictScalars S ↔ m ∈ V :=
  Iff.refl _

Membership in Restricted Scalar Submodule is Equivalent to Original Membership

Informal description

Let $S$ and $R$ be semirings with $S$ acting on $R$, and let $M$ be a module over both $R$ and $S$ with compatible actions. For any $R$-submodule $V$ of $M$ and any element $m \in M$, we have $m \in V.\text{restrictScalars}(S)$ if and only if $m \in V$.

Submodule.restrictScalars_self theorem

(V : Submodule R M) : V.restrictScalars R = V

Full source

@[simp]
theorem restrictScalars_self (V : Submodule R M) : V.restrictScalars R = V :=
  SetLike.coe_injective rfl

Restriction of Scalars to Same Semiring Preserves Submodule

Informal description

For any $R$-submodule $V$ of $M$, the restriction of scalars of $V$ to $R$ is equal to $V$ itself, i.e., $V.\text{restrictScalars}\, R = V$.

Submodule.restrictScalars_injective theorem

: Function.Injective (restrictScalars S : Submodule R M → Submodule S M)

Full source

theorem restrictScalars_injective :
    Function.Injective (restrictScalars S : Submodule R M → Submodule S M) := fun _ _ h =>
  ext <| Set.ext_iff.1 (SetLike.ext'_iff.1 h :)

Injectivity of Restriction of Scalars for Submodules

Informal description

The restriction of scalars map from $R$-submodules to $S$-submodules is injective. That is, for any two $R$-submodules $V_1$ and $V_2$ of $M$, if their restrictions to $S$-submodules are equal, then $V_1 = V_2$.

Submodule.restrictScalars_inj theorem

{V₁ V₂ : Submodule R M} : restrictScalars S V₁ = restrictScalars S V₂ ↔ V₁ = V₂

Full source

@[simp]
theorem restrictScalars_inj {V₁ V₂ : Submodule R M} :
    restrictScalarsrestrictScalars S V₁ = restrictScalars S V₂ ↔ V₁ = V₂ :=
  (restrictScalars_injective S _ _).eq_iff

Injectivity of Restriction of Scalars: $V_1|_S = V_2|_S \leftrightarrow V_1 = V_2$

Informal description

For any two $R$-submodules $V_1$ and $V_2$ of $M$, the restriction of scalars to $S$ yields equal $S$-submodules if and only if $V_1 = V_2$ as $R$-submodules. In other words, the map $V \mapsto V.\text{restrictScalars}\,S$ is injective.

Submodule.restrictScalars.origModule instance

(p : Submodule R M) : Module R (p.restrictScalars S)

Full source

/-- Even though `p.restrictScalars S` has type `Submodule S M`, it is still an `R`-module. -/
instance restrictScalars.origModule (p : Submodule R M) : Module R (p.restrictScalars S) :=
  (by infer_instance : Module R p)

Original Module Structure on Restricted Submodules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the restricted submodule $p.\text{restrictScalars}\,S$ retains its original $R$-module structure.

Submodule.restrictScalars.isScalarTower instance

(p : Submodule R M) : IsScalarTower S R (p.restrictScalars S)

Full source

instance restrictScalars.isScalarTower (p : Submodule R M) :
    IsScalarTower S R (p.restrictScalars S) where
  smul_assoc r s x := Subtype.ext <| smul_assoc r s (x : M)

Scalar Tower Property for Restricted Submodules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the restricted submodule $p.\text{restrictScalars}\,S$ satisfies the scalar tower property with respect to the scalar multiplications of $S$ on $R$ and $R$ on $p.\text{restrictScalars}\,S$. That is, for any $s \in S$, $r \in R$, and $x \in p.\text{restrictScalars}\,S$, we have $(s \cdot r) \bullet x = s \bullet (r \bullet x)$.

Submodule.restrictScalarsEmbedding definition

: Submodule R M ↪o Submodule S M

Full source

/-- `restrictScalars S` is an embedding of the lattice of `R`-submodules into
the lattice of `S`-submodules. -/
@[simps]
def restrictScalarsEmbedding : SubmoduleSubmodule R M ↪o Submodule S M where
  toFun := restrictScalars S
  inj' := restrictScalars_injective S R M
  map_rel_iff' := by simp [SetLike.le_def]

Order embedding of submodules via restriction of scalars

Informal description

The order embedding that maps an $R$-submodule of $M$ to its corresponding $S$-submodule by restricting the scalar multiplication from $R$ to $S$. This embedding is injective and preserves the order structure, meaning for any two $R$-submodules $V_1$ and $V_2$, we have $V_1 \subseteq V_2$ if and only if their restricted $S$-submodules satisfy the same inclusion.

Submodule.restrictScalarsEquiv definition

(p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p

Full source

/-- 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. -/
@[simps +simpRhs]
def restrictScalarsEquiv (p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p :=
  { AddEquiv.refl p with
    map_smul' := fun _ _ => rfl }

Linear equivalence between restricted and original submodules

Informal description

For any $R$-submodule $p$ of a module $M$ over semirings $R$ and $S$ with compatible actions, the linear equivalence `Submodule.restrictScalarsEquiv` maps the restricted submodule $p.\text{restrictScalars}\,S$ (viewed as an $S$-submodule) back to $p$ (viewed as an $R$-submodule), preserving both the additive structure and the scalar multiplication by elements of $R$. More precisely, this equivalence: 1. Is the identity map on the underlying set of $p$ 2. Preserves addition: $f(x + y) = f(x) + f(y)$ 3. Preserves $R$-scalar multiplication: $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in p$

Submodule.restrictScalars_bot theorem

: restrictScalars S (⊥ : Submodule R M) = ⊥

Full source

@[simp]
theorem restrictScalars_bot : restrictScalars S (⊥ : Submodule R M) = ⊥ :=
  rfl

Restriction of Scalars Preserves the Zero Submodule

Informal description

For any module $M$ over semirings $R$ and $S$ with compatible actions, the restriction of scalars of the zero submodule $\{0\}$ (as an $R$-submodule) is equal to the zero submodule $\{0\}$ (as an $S$-submodule). That is, $\text{restrictScalars}_S(\{0\}) = \{0\}$.

Submodule.restrictScalars_eq_bot_iff theorem

{p : Submodule R M} : restrictScalars S p = ⊥ ↔ p = ⊥

Full source

@[simp]
theorem restrictScalars_eq_bot_iff {p : Submodule R M} : restrictScalarsrestrictScalars S p = ⊥ ↔ p = ⊥ := by
  simp [SetLike.ext_iff]

Zero Submodule Criterion under Restriction of Scalars

Informal description

For any $R$-submodule $p$ of $M$, the restriction of scalars of $p$ to $S$ is the zero submodule if and only if $p$ itself is the zero submodule. In other words, $\text{restrictScalars}_S(p) = \{0\} \leftrightarrow p = \{0\}$.

Submodule.restrictScalars_top theorem

: restrictScalars S (⊤ : Submodule R M) = ⊤

Full source

@[simp]
theorem restrictScalars_top : restrictScalars S (⊤ : Submodule R M) = ⊤ :=
  rfl

Restriction of Scalars Preserves the Top Submodule

Informal description

Let $S$ and $R$ be semirings with $S$ acting on $R$, and let $M$ be a module over both $R$ and $S$ with compatible actions. Then the restriction of scalars of the top $R$-submodule of $M$ (i.e., $M$ itself) is equal to the top $S$-submodule of $M$. In other words, if we regard $M$ as an $R$-submodule of itself and then restrict scalars to $S$, we obtain $M$ as an $S$-submodule.

Submodule.restrictScalars_eq_top_iff theorem

{p : Submodule R M} : restrictScalars S p = ⊤ ↔ p = ⊤

Full source

@[simp]
theorem restrictScalars_eq_top_iff {p : Submodule R M} : restrictScalarsrestrictScalars S p = ⊤ ↔ p = ⊤ := by
  simp [SetLike.ext_iff]

Restriction of Scalars Preserves Top Submodule

Informal description

Let $S$ and $R$ be semirings with $S$ acting on $R$, and let $M$ be a module over both $R$ and $S$ with compatible actions. For any $R$-submodule $p$ of $M$, the restriction of scalars of $p$ to $S$ equals the top $S$-submodule of $M$ if and only if $p$ itself is the top $R$-submodule of $M$.

Submodule.restrictScalarsLatticeHom definition

: CompleteLatticeHom (Submodule R M) (Submodule S M)

Full source

/-- 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`. -/
def restrictScalarsLatticeHom : CompleteLatticeHom (Submodule R M) (Submodule S M) where
  toFun := restrictScalars S
  map_sInf' s := by ext; simp
  map_sSup' s := by rw [← toAddSubmonoid_inj, toAddSubmonoid_sSup, ← Set.image_comp]; simp

Complete lattice homomorphism for restriction of scalars on submodules

Informal description

Given semirings $S$ and $R$ with $S$ acting on $R$, and a module $M$ over both $R$ and $S$ with compatible actions, the function `Submodule.restrictScalarsLatticeHom` is a complete lattice homomorphism from the lattice of $R$-submodules of $M$ to the lattice of $S$-submodules of $M$. This homomorphism maps each $R$-submodule $V$ to its underlying set viewed as an $S$-submodule (by forgetting the $R$-action), and preserves arbitrary infima and suprema of submodules.

Main definitions: