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.instIsTorsionFree {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [Module.IsTorsionFree R M] :

Module.IsTorsionFree 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_reducible]

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 = AddSubmonoid.instVAddSubtypeMem p

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

@[simp]

theorem Submodule.toAddSubgroup_toAddSubmonoid {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

p.toAddSubgroup.toAddSubmonoid = p.toAddSubmonoid

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

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