Mathlib.Algebra.Module.Submodule.RestrictScalars._auxLemma.1
theorem Mathlib.Algebra.Module.Submodule.RestrictScalars._auxLemma.1 :
∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
[inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (V : Submodule R M)
(m : M), (m ∈ Submodule.restrictScalars S V) = (m ∈ V)
This theorem states that for any semiring `S`, another semiring `R`, and an additive commutative monoid `M`, given certain module and scalar multiplication structures and provided that `S`, `R`, and `M` form a scalar tower, any element `m` of `M` belongs to the `Submodule.restrictScalars S V` if and only if it belongs to `V`. `V` here is a submodule of `M` over `R`. Essentially, this theorem shows that restricting scalars does not change the membership of elements in `M` with respect to the submodule `V`.
More concisely: For any semirings S and R, additive commutative monoid M, submodule V of M over R, and given module and scalar multiplication structures making S, R, and M a scalar tower, an element m of M belongs to the submodule V over R if and only if it belongs to V.
|
Submodule.restrictScalars_injective
theorem Submodule.restrictScalars_injective :
∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
[inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M],
Function.Injective (Submodule.restrictScalars S)
The theorem `Submodule.restrictScalars_injective` states that for all Types `S`, `R`, `M`, given a semiring structure on `R`, an additive commutative monoid structure on `M`, a semiring structure on `S`, a module structure over `S` on `M`, a module structure over `R` on `M`, a scalar multiplication of `S` on `R` and a scalar tower of `S`, `R` and `M`, the function `Submodule.restrictScalars S` is injective. In other words, if `Submodule.restrictScalars S` is applied to two objects and gives the same result, then those two objects were already the same. This is a property of how scalar multiplication is restricted to a submodule.
More concisely: Given a semiring `S`, a semiring `R`, an additive commutative monoid `M` with module structures over `S` and `R`, and a scalar multiplication of `S` on `R`, the restriction of scalar multiplication from `S` to a submodule of `M` is an injective function.
|