mathlib documentation

algebra.module.submodule

Submodules of a module

In this file we define

Tags

submodule, subspace, linear map

def submodule.to_add_submonoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Reinterpret a submodule as an add_submonoid.

structure submodule (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule 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.

@[instance]
def submodule.has_coe_t {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def submodule.has_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[instance]
def submodule.has_coe_to_sort {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[simp]
theorem submodule.coe_sort_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :

theorem submodule.exists {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p : submodule R M} {q : p → Prop} :
(∃ (x : p), q x) ∃ (x : M) (H : x p), q x, H⟩

theorem submodule.forall {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p : submodule R M} {q : p → Prop} :
(∀ (x : p), q x) ∀ (x : M) (H : x p), q x, H⟩

theorem submodule.coe_injective {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem submodule.coe_set_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p q : submodule R M} :
p = q p = q

theorem submodule.ext'_iff {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p q : submodule R M} :
p = q p = q

@[ext]
theorem submodule.ext {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p q : submodule R M} :
(∀ (x : M), x p x q)p = q

@[simp]
theorem submodule.to_add_submonoid_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule R M] {p q : submodule R M} :

@[simp]
theorem submodule.mem_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) {x : M} :
x p x p

@[simp]
theorem submodule.zero_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :
0 p

theorem submodule.add_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) {x y : M} :
x py px + y p

theorem submodule.smul_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) {x : M} (r : R) :
x pr x p

theorem submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R 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] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) {t : finset ι} {f : ι → M} (r : ι → R) :
(∀ (c : ι), c tf c p)∑ (i : ι) in t, r i f i p

@[simp]
theorem submodule.smul_mem_iff' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) {x : M} (u : units R) :
u x p x p

@[instance]
def submodule.has_add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[instance]
def submodule.has_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[instance]
def submodule.inhabited {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[instance]
def submodule.has_scalar {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[simp]
theorem submodule.mk_eq_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) {x : M} (h : x p) :
x, h⟩ = 0 x = 0

@[simp]
theorem submodule.coe_eq_coe {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} {x y : p} :
x = y x = y

@[simp]
theorem submodule.coe_eq_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} {x : p} :
x = 0 x = 0

@[simp]
theorem submodule.coe_add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} (x y : p) :
(x + y) = x + y

@[simp]
theorem submodule.coe_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} :
0 = 0

@[simp]
theorem submodule.coe_smul {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} (r : R) (x : p) :
(r x) = r x

@[simp]
theorem submodule.coe_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} (x : M) (hx : x p) :
x, hx⟩ = x

@[simp]
theorem submodule.coe_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} (x : p) :
x p

@[simp]
theorem submodule.eta {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {p : submodule R M} (x : p) (hx : x p) :
x, hx⟩ = x

@[instance]
def submodule.add_comm_monoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[instance]
def submodule.semimodule {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
def submodule.subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R 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] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) (x : p) :

theorem submodule.subtype_eq_val {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} (p : submodule R M) :

theorem submodule.neg_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) {x : M} :
x p-x p

def submodule.to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} :

Reinterpret a submodule as an additive subgroup.

Equations
@[simp]
theorem submodule.coe_to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) :

theorem submodule.sub_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) {x y : M} :
x py px - y p

@[simp]
theorem submodule.neg_mem_iff {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) {x : M} :
-x p x p

theorem submodule.add_mem_iff_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R 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] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) {x y : M} :
x p(x + y p y p)

@[instance]
def submodule.has_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[simp]
theorem submodule.coe_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) (x : p) :

@[instance]
def submodule.add_comm_group {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) :

Equations
@[simp]
theorem submodule.coe_sub {R : Type u} {M : Type v} [ring R] [add_comm_group M] {semimodule_M : semimodule R M} (p : submodule R M) (x y : p) :
(x - y) = x - y

theorem submodule.smul_mem_iff {R : Type u} {M : Type v} [division_ring R] [add_comm_group M] [module R M] (p : submodule R M) {r : R} {x : M} :
r 0(r x p x p)

def subspace (R : Type u) (M : Type v) [field R] [add_comm_group M] [vector_space R M] :
Type v

Subspace of a vector space. Defined to equal submodule.