# Submodules of a module #

This file contains basic results on submodules that require further theory to be defined. As such it is a good target for organizing and splitting further.

## Tags #

submodule, subspace, linear map

source
theorem Submodule.toAddSubmonoid_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
StrictMono toAddSubmonoid
source
theorem Submodule.toAddSubmonoid_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :
p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q
source
theorem Submodule.toAddSubmonoid_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
Monotone toAddSubmonoid
source
theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
StrictMono toSubMulAction
source
theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
Monotone toSubMulAction
source
theorem Submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ι → M} :
(∀ c ∈ t, f c ∈ p) → ∑ i ∈ t, f i ∈ p
source
theorem Submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ c ∈ t, f c ∈ p) :
∑ i ∈ t, r i • f i ∈ p
source
instance Submodule.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul S ᵐᵒᵖ R] [SMul S ᵐᵒᵖ M] [IsScalarTower S ᵐᵒᵖ R M] [IsCentralScalar S M] :
IsCentralScalar S ↥p
source
instance Submodule.noZeroSMulDivisors {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [NoZeroSMulDivisors R M] :
NoZeroSMulDivisors R ↥p

### Additive actions by `Submodule`s #

These instances transfer the action by an element `m : M` of an `R`-module `M` written as `m +ᵥ a` onto the action by an element `s : S` of a submodule `S : Submodule R M` such that `s +ᵥ a = (s : M) +ᵥ a`. These instances work particularly well in conjunction with `AddGroup.toAddAction`, enabling `s +ᵥ m` as an alias for `↑s + m`.

source
instance Submodule.instVAddSubtypeMem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] :
VAdd (↥p) α
Equations

- p.instVAddSubtypeMem = p.vadd

source
instance Submodule.vaddCommClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} {β : Type u_2} [VAdd M β] [VAdd α β] [VAddCommClass M α β] :
VAddCommClass (↥p) α β
source
instance Submodule.instFaithfulVAddSubtypeMem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] [FaithfulVAdd M α] :
FaithfulVAdd (↥p) α
source
theorem Submodule.vadd_def {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {α : Type u_1} [VAdd M α] (g : ↥p) (m : α) :
g +ᵥ m = ↑g +ᵥ m
source
theorem Submodule.toAddSubgroup_strictMono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :
StrictMono toAddSubgroup
source
theorem Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p p' : Submodule R M) :
p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p'
source
theorem Submodule.toAddSubgroup_mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :
Monotone toAddSubgroup
source
theorem GCongr.Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p p' : Submodule R M) :
p ≤ p' → p.toAddSubgroup ≤ p'.toAddSubgroup

Alias of the reverse direction of `Submodule.toAddSubgroup_le`.

source
theorem Submodule.neg_coe {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
-↑p = ↑p
source
theorem Submodule.notMem_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) :
x ∉ N
source
@[deprecated Submodule.notMem_of_ortho (since := "2025-05-23")]
theorem Submodule.not_mem_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) :
x ∉ N

Alias of `Submodule.notMem_of_ortho`.

source
theorem Submodule.ne_zero_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) :
x ≠ 0
source
theorem Submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [DivisionSemiring S] [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] (p : Submodule R M) {s : S} {x : M} (s0 : s ≠ 0) :
s • x ∈ p ↔ x ∈ p
source
@[reducible, inline]
abbrev Subspace (R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [Module R M] :
Type v

Subspace of a vector space. Defined to equal `Submodule`.

Equations

- Subspace R M = Submodule R M

Instances For