# mathlibdocumentation

algebra.module.submodule

# Submodules of a module #

In this file we define

• submodule R M : a subset of a module M that contains zero and is closed with respect to addition and scalar multiplication.

• subspace k M : an abbreviation for submodule assuming that k is a field.

## Tags #

submodule, subspace, linear map

def submodule.to_add_submonoid {R : Type u} {M : Type v} [semiring R] [ M] (self : M) :

Reinterpret a submodule as an add_submonoid.

structure submodule (R : Type u) (M : Type v) [semiring R] [ M] :
Type v

A submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.

def submodule.to_sub_mul_action {R : Type u} {M : Type v} [semiring R] [ M] (self : M) :

Reinterpret a submodule as an sub_mul_action.

@[protected, instance]
def submodule.set_like {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.mem_to_add_submonoid {R : Type u} {M : Type v} [semiring R] [ M] (p : M) (x : M) :
x p
@[simp]
theorem submodule.mk_coe {R : Type u} {M : Type v} [semiring R] [ M] (S : set M) (h₁ : 0 S) (h₂ : ∀ {a b : M}, a Sb Sa + b S) (h₃ : ∀ (c : R) {x : M}, x Sc x S) :
{carrier := S, zero_mem' := h₁, add_mem' := h₂, smul_mem' := h₃} = S
@[ext]
theorem submodule.ext {R : Type u} {M : Type v} [semiring R] [ M] {p q : M} (h : ∀ (x : M), x p x q) :
p = q
@[protected]
def submodule.copy {R : Type u} {M : Type v} [semiring R] [ M] (p : M) (s : set M) (hs : s = p) :
M

Copy of a submodule with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
theorem submodule.to_add_submonoid_injective {R : Type u} {M : Type v} [semiring R] [ M] :
@[simp]
theorem submodule.to_add_submonoid_eq {R : Type u} {M : Type v} [semiring R] [ M] {p q : M} :
p = q
theorem submodule.to_add_submonoid_strict_mono {R : Type u} {M : Type v} [semiring R] [ M] :
theorem submodule.to_add_submonoid_mono {R : Type u} {M : Type v} [semiring R] [ M] :
@[simp]
theorem submodule.coe_to_add_submonoid {R : Type u} {M : Type v} [semiring R] [ M] (p : M) :
theorem submodule.to_sub_mul_action_injective {R : Type u} {M : Type v} [semiring R] [ M] :
@[simp]
theorem submodule.to_sub_mul_action_eq {R : Type u} {M : Type v} [semiring R] [ M] {p q : M} :
p = q
theorem submodule.to_sub_mul_action_strict_mono {R : Type u} {M : Type v} [semiring R] [ M] :
theorem submodule.to_sub_mul_action_mono {R : Type u} {M : Type v} [semiring R] [ M] :
@[simp]
theorem submodule.coe_to_sub_mul_action {R : Type u} {M : Type v} [semiring R] [ M] (p : M) :
@[simp]
theorem submodule.mem_carrier {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) {x : M} :
@[simp]
theorem submodule.zero_mem {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
0 p
theorem submodule.add_mem {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) {x y : M} (h₁ : x p) (h₂ : y p) :
x + y p
theorem submodule.smul_mem {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) {x : M} (r : R) (h : x p) :
r x p
theorem submodule.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [semiring S] [semiring R] {module_M : M} (p : M) {x : M} [ R] [ M] [ M] (r : S) (h : x p) :
r x p
theorem submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] {module_M : M} (p : M) {t : finset ι} {f : ι → M} :
(∀ (c : ι), c tf c p)∑ (i : ι) in t, f i p
theorem submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] {module_M : M} (p : M) {t : finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ (c : ι), c tf c p) :
∑ (i : ι) in t, r i f i p
@[simp]
theorem submodule.smul_mem_iff' {S : Type u'} {R : Type u} {M : Type v} [semiring S] [semiring R] {module_M : M} (p : M) {x : M} [ R] [ M] [ M] (u : units S) :
u x p x p
@[protected, instance]
def submodule.has_add {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
Equations
@[protected, instance]
def submodule.has_zero {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
Equations
@[protected, instance]
def submodule.inhabited {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
Equations
@[protected, instance]
def submodule.has_scalar {S : Type u'} {R : Type u} {M : Type v} [semiring S] [semiring R] {module_M : M} (p : M) [ R] [ M] [ M] :
p
Equations
@[protected]
theorem submodule.nonempty {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
@[simp]
theorem submodule.mk_eq_zero {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) {x : M} (h : x p) :
x, h⟩ = 0 x = 0
@[simp, norm_cast]
theorem submodule.coe_eq_zero {R : Type u} {M : Type v} [semiring R] {module_M : M} {p : M} {x : p} :
x = 0 x = 0
@[simp, norm_cast]
theorem submodule.coe_add {R : Type u} {M : Type v} [semiring R] {module_M : M} {p : M} (x y : p) :
(x + y) = x + y
@[simp, norm_cast]
theorem submodule.coe_zero {R : Type u} {M : Type v} [semiring R] {module_M : M} {p : M} :
0 = 0
@[norm_cast]
theorem submodule.coe_smul {R : Type u} {M : Type v} [semiring R] {module_M : M} {p : M} (r : R) (x : p) :
(r x) = r x
@[simp, norm_cast]
theorem submodule.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [semiring S] [semiring R] {module_M : M} {p : M} [ R] [ M] [ M] (r : S) (x : p) :
(r x) = r x
@[simp, norm_cast]
theorem submodule.coe_mk {R : Type u} {M : Type v} [semiring R] {module_M : M} {p : M} (x : M) (hx : x p) :
x, hx⟩ = x
@[simp]
theorem submodule.coe_mem {R : Type u} {M : Type v} [semiring R] {module_M : M} {p : M} (x : p) :
x p
@[protected, instance]
def submodule.add_comm_monoid {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
Equations
@[protected, instance]
def submodule.module' {S : Type u'} {R : Type u} {M : Type v} [semiring S] [semiring R] {module_M : M} (p : M) [ R] [ M] [ M] :
p
Equations
@[protected, instance]
def submodule.module {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
p
Equations
@[protected, instance]
def submodule.is_scalar_tower {S : Type u'} {R : Type u} {M : Type v} [semiring S] [semiring R] {module_M : M} (p : M) [ R] [ M] [ M] :
p
@[protected, instance]
def submodule.no_zero_smul_divisors {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M)  :
@[protected]
def submodule.subtype {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :

Embedding of a submodule p to the ambient space M.

Equations
@[simp]
theorem submodule.subtype_apply {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) (x : p) :
theorem submodule.subtype_eq_val {R : Type u} {M : Type v} [semiring R] {module_M : M} (p : M) :
theorem submodule.neg_mem {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) {x : M} (hx : x p) :
-x p
def submodule.to_add_subgroup {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) :

Reinterpret a submodule as an additive subgroup.

Equations
@[simp]
theorem submodule.coe_to_add_subgroup {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) :
@[simp]
theorem submodule.mem_to_add_subgroup {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) {x : M} :
x p
theorem submodule.to_add_subgroup_injective {R : Type u} {M : Type v} [ring R] {module_M : M} :
@[simp]
theorem submodule.to_add_subgroup_eq {R : Type u} {M : Type v} [ring R] {module_M : M} (p p' : M) :
p = p'
theorem submodule.to_add_subgroup_strict_mono {R : Type u} {M : Type v} [ring R] {module_M : M} :
theorem submodule.to_add_subgroup_mono {R : Type u} {M : Type v} [ring R] {module_M : M} :
theorem submodule.sub_mem {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) {x y : M} :
x py px - y p
@[simp]
theorem submodule.neg_mem_iff {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) {x : M} :
-x p x p
theorem submodule.add_mem_iff_left {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) {x y : M} :
y p(x + y p x p)
theorem submodule.add_mem_iff_right {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) {x y : M} :
x p(x + y p y p)
@[protected, instance]
def submodule.has_neg {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) :
Equations
@[simp, norm_cast]
theorem submodule.coe_neg {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) (x : p) :
@[protected, instance]
def submodule.add_comm_group {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) :
Equations
@[simp, norm_cast]
theorem submodule.coe_sub {R : Type u} {M : Type v} [ring R] {module_M : M} (p : M) (x y : p) :
(x - y) = x - y
@[protected, instance]
def submodule.to_ordered_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [ M] (S : M) :

A submodule of an ordered_add_comm_monoid is an ordered_add_comm_monoid.

Equations
@[protected, instance]
def submodule.to_linear_ordered_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [ M] (S : M) :

A submodule of a linear_ordered_add_comm_monoid is a linear_ordered_add_comm_monoid.

Equations
@[protected, instance]
def submodule.to_ordered_cancel_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [ M] (S : M) :

A submodule of an ordered_cancel_add_comm_monoid is an ordered_cancel_add_comm_monoid.

Equations
@[protected, instance]
def submodule.to_linear_ordered_cancel_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [ M] (S : M) :

A submodule of a linear_ordered_cancel_add_comm_monoid is a linear_ordered_cancel_add_comm_monoid.

Equations
@[protected, instance]
def submodule.to_ordered_add_comm_group {R : Type u} [ring R] {M : Type u_1} [ M] (S : M) :

A submodule of an ordered_add_comm_group is an ordered_add_comm_group.

Equations
@[protected, instance]
def submodule.to_linear_ordered_add_comm_group {R : Type u} [ring R] {M : Type u_1} [ M] (S : M) :

A submodule of a linear_ordered_add_comm_group is a linear_ordered_add_comm_group.

Equations
theorem submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [semiring R] [ M] [ R] [ M] [ M] (p : M) {s : S} {x : M} (s0 : s 0) :
s x p x p
def subspace (R : Type u) (M : Type v) [field R] [ M] :
Type v

Subspace of a vector space. Defined to equal submodule.