mathlib3 documentation

algebra.module.submodule.basic

Submodules of a module #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] [module R M] (self : submodule R M) :

Reinterpret a submodule as an add_submonoid.

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

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.

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

Reinterpret a submodule as an sub_mul_action.

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

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

Equations
@[simp]
theorem submodule.coe_copy {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (S : submodule R M) (s : set M) (hs : s = S) :
(S.copy s hs) = s
theorem submodule.copy_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (S : submodule R M) (s : set M) (hs : s = S) :
S.copy s hs = S
@[simp]
@[simp]
theorem submodule.coe_to_add_submonoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
@[simp]
@[simp]
@[protected, instance]
def smul_mem_class.to_module {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {A : Type u_1} [set_like A M] [add_submonoid_class A M] [hA : smul_mem_class A R M] (S' : A) :

A submodule of a module is a module.

Equations
@[protected]
def smul_mem_class.subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {A : Type u_1} [set_like A M] [add_submonoid_class A M] [hA : smul_mem_class A R M] (S' : A) :

The natural R-linear map from a submodule of an R-module M to M.

Equations
@[protected, simp]
theorem smul_mem_class.coe_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {A : Type u_1} [set_like A M] [add_submonoid_class A M] [hA : smul_mem_class A R M] (S' : A) :
@[simp]
theorem submodule.mem_carrier {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} :
@[protected, simp]
theorem submodule.zero_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
0 p
@[protected]
theorem submodule.add_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R 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] [add_comm_monoid M] {module_M : module R M} (p : submodule R 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 R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (r : S) (h : x p) :
r x p
@[protected]
theorem submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {t : finset ι} {f : ι M} :
( (c : ι), c t f c p) t.sum (λ (i : ι), f i) p
theorem submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {t : finset ι} {f : ι M} (r : ι R) (hyp : (c : ι), c t f c p) :
t.sum (λ (i : ι), r i f i) p
@[simp]
theorem submodule.smul_mem_iff' {G : Type u''} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} [group G] [mul_action G M] [has_smul G R] [is_scalar_tower G R M] (g : G) :
g x p x p
@[protected, instance]
def submodule.has_add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
Equations
@[protected, instance]
def submodule.has_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
Equations
@[protected, instance]
def submodule.inhabited {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
Equations
@[protected, instance]
def submodule.has_smul {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [has_smul S R] [has_smul S M] [is_scalar_tower S R M] :
Equations
@[protected, instance]
def submodule.is_scalar_tower {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [has_smul S R] [has_smul S M] [is_scalar_tower S R M] :
@[protected, instance]
def submodule.is_scalar_tower' {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {S' : Type u_1} [has_smul S R] [has_smul S M] [has_smul S' R] [has_smul S' M] [has_smul S S'] [is_scalar_tower S' R M] [is_scalar_tower S S' M] [is_scalar_tower S R M] :
@[protected, instance]
@[protected]
theorem submodule.nonempty {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
@[simp]
theorem submodule.mk_eq_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R 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] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} {x : p} :
x = 0 x = 0
@[simp, norm_cast]
theorem submodule.coe_add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} (x y : p) :
(x + y) = x + y
@[simp, norm_cast]
theorem submodule.coe_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} :
0 = 0
@[norm_cast]
theorem submodule.coe_smul {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R 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 R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (r : S) (x : p) :
(r x) = r x
@[simp, norm_cast]
theorem submodule.coe_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module 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] {module_M : module R M} {p : submodule R M} (x : p) :
x p
@[protected, instance]
def submodule.add_comm_monoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
Equations
@[protected, instance]
def submodule.module' {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [semiring S] [has_smul S R] [module S M] [is_scalar_tower S R M] :
Equations
@[protected, instance]
def submodule.module {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
Equations
@[protected, instance]
@[protected]
def submodule.subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

Embedding of a submodule p to the ambient space M.

Equations
theorem submodule.subtype_apply {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) (x : p) :
@[simp]
theorem submodule.coe_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
theorem submodule.injective_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :
@[simp]
theorem submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) (x : ι p) (s : finset ι) :
(s.sum (λ (i : ι), x i)) = s.sum (λ (i : ι), (x i))

Note the add_submonoid version of this lemma is called add_submonoid.coe_finset_sum.

Additive actions by submodules #

These instances transfer the action by an element m : M of a 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 add_group.to_add_action, enabling s +ᵥ m as an alias for ↑s + m.

@[protected, instance]
def submodule.has_vadd {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {α : Type u_1} [has_vadd M α] :
Equations
@[protected, instance]
def submodule.vadd_comm_class {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {α : Type u_1} {β : Type u_2} [has_vadd M β] [has_vadd α β] [vadd_comm_class M α β] :
@[protected, instance]
def submodule.has_faithful_vadd {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {α : Type u_1} [has_vadd M α] [has_faithful_vadd M α] :
@[protected, instance]
def submodule.add_action {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {α : Type u_1} [add_action M α] :

The action by a submodule is the action by the underlying module.

Equations
theorem submodule.vadd_def {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} {α : Type u_1} [has_vadd M α] (g : p) (m : α) :
g +ᵥ m = g +ᵥ m
def submodule.restrict_scalars (S : Type u') {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) :

V.restrict_scalars S is the S-submodule of the S-module given by restriction of scalars, corresponding to V, an R-submodule of the original R-module.

Equations
Instances for submodule.restrict_scalars
@[simp]
theorem submodule.coe_restrict_scalars (S : Type u') {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) :
@[simp]
theorem submodule.restrict_scalars_mem (S : Type u') {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) (m : M) :
@[simp]
@[simp]
theorem submodule.restrict_scalars_inj (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] {V₁ V₂ : submodule R M} :
@[protected, instance]

Even though p.restrict_scalars S has type submodule S M, it is still an R-module.

Equations
@[protected, instance]
def submodule.restrict_scalars_embedding (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] :

restrict_scalars S is an embedding of the lattice of R-submodules into the lattice of S-submodules.

Equations

Turning p : submodule R M into an S-submodule gives the same module structure as turning it into a type and adding a module structure.

Equations
@[simp]
@[simp]
theorem submodule.restrict_scalars_equiv_symm_apply (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (p : submodule R M) (a : p) :
@[protected, instance]
@[protected]
theorem submodule.neg_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x : M} (hx : x p) :
-x p
def submodule.to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule 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] {module_M : module R M} (p : submodule R M) :
@[simp]
theorem submodule.mem_to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x : M} :
@[simp]
theorem submodule.to_add_subgroup_eq {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p p' : submodule R M) :
theorem submodule.to_add_subgroup_le {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p p' : submodule R M) :
@[protected]
theorem submodule.sub_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} :
x p y p x - y p
@[protected]
theorem submodule.neg_mem_iff {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x : M} :
-x p x p
@[protected]
theorem submodule.add_mem_iff_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} :
y p (x + y p x p)
@[protected]
theorem submodule.add_mem_iff_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} :
x p (x + y p y p)
@[protected]
theorem submodule.coe_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) (x : p) :
@[protected]
theorem submodule.coe_sub {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) (x y : p) :
(x - y) = x - y
theorem submodule.sub_mem_iff_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} (hy : y p) :
x - y p x p
theorem submodule.sub_mem_iff_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} (hx : x p) :
x - y p y p
theorem submodule.not_mem_of_ortho {R : Type u} {M : Type v} [ring R] [is_domain R] [add_comm_group M] [module R M] {x : M} {N : submodule R M} (ortho : (c : R) (y : M), y N c x + y = 0 c = 0) :
x N
theorem submodule.ne_zero_of_ortho {R : Type u} {M : Type v} [ring R] [is_domain R] [add_comm_group M] [module R M] {x : M} {N : submodule R M} (ortho : (c : R) (y : M), y N c x + y = 0 c = 0) :
x 0
theorem submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [division_ring S] [semiring R] [add_comm_monoid M] [module R M] [has_smul S R] [module S M] [is_scalar_tower S R M] (p : submodule R M) {s : S} {x : M} (s0 : s 0) :
s x p x p
@[reducible]
def subspace (R : Type u) (M : Type v) [division_ring R] [add_comm_group M] [module R M] :

Subspace of a vector space. Defined to equal submodule.