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

theorem Submodule.toAddSubmonoid_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : StrictMono toAddSubmonoid

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

theorem Submodule.toAddSubmonoid_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : Monotone toAddSubmonoid

theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : StrictMono toSubMulAction

theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : Monotone toSubMulAction

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

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

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

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 Submodules

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.

@[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

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) α β

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

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

theorem Submodule.toAddSubgroup_strictMono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} : StrictMono toAddSubgroup

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'

theorem Submodule.toAddSubgroup_mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} : Monotone toAddSubgroup

@[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

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

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

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

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

@[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