Submodules of a module #
In this file we define
-
submodule R M: a subset of amoduleMthat contains zero and is closed with respect to addition and scalar multiplication. -
subspace k M: an abbreviation forsubmoduleassuming thatkis afield.
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] :
Type v
- carrier : set M
- zero_mem' : 0 ∈ c.carrier
- add_mem' : ∀ {a b : M}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
- smul_mem' : ∀ (c_1 : R) {x : M}, x ∈ c.carrier → c_1 • x ∈ c.carrier
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]
[add_comm_monoid M]
[module R M]
(self : submodule R M) :
sub_mul_action R M
Reinterpret a submodule as an sub_mul_action.
@[protected, instance]
Equations
- submodule.set_like = {coe := submodule.carrier _inst_3, coe_injective' := _}
@[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) :
x ∈ p.to_add_submonoid ↔ x ∈ p
@[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) :
submodule R M
Copy of a submodule with a new carrier equal to the old one. Useful to fix definitional
equalities.
theorem
submodule.to_add_submonoid_injective
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
submodule.to_add_submonoid_eq
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{p q : submodule R M} :
p.to_add_submonoid = q.to_add_submonoid ↔ p = q
theorem
submodule.to_add_submonoid_strict_mono
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
submodule.to_add_submonoid_mono
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[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) :
↑(p.to_add_submonoid) = ↑p
theorem
submodule.to_sub_mul_action_injective
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
submodule.to_sub_mul_action_eq
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{p q : submodule R M} :
p.to_sub_mul_action = q.to_sub_mul_action ↔ p = q
theorem
submodule.to_sub_mul_action_strict_mono
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
submodule.to_sub_mul_action_mono
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
submodule.coe_to_sub_mul_action
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M) :
↑(p.to_sub_mul_action) = ↑p
@[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
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) :
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) :
theorem
submodule.smul_of_tower_mem
{S : Type u'}
{R : Type u}
{M : Type v}
[semiring S]
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M)
{x : M}
[has_scalar S R]
[module S M]
[is_scalar_tower S R M]
(r : S)
(h : x ∈ p) :
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} :
@[simp]
theorem
submodule.smul_mem_iff'
{S : Type u'}
{R : Type u}
{M : Type v}
[semiring S]
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M)
{x : M}
[has_scalar S R]
[module S M]
[is_scalar_tower S R M]
(u : units S) :
@[protected, instance]
def
submodule.has_scalar
{S : Type u'}
{R : Type u}
{M : Type v}
[semiring S]
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M)
[has_scalar S R]
[module S M]
[is_scalar_tower S R M] :
has_scalar S ↥p
@[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, 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} :
@[simp, norm_cast]
theorem
submodule.coe_smul_of_tower
{S : Type u'}
{R : Type u}
{M : Type v}
[semiring S]
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
{p : submodule R M}
[has_scalar S R]
[module S M]
[is_scalar_tower S R M]
(r : S)
(x : ↥p) :
@[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) :
@[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) :
@[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
- p.add_comm_monoid = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul p.to_add_submonoid.to_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
def
submodule.module'
{S : Type u'}
{R : Type u}
{M : Type v}
[semiring S]
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M)
[has_scalar S R]
[module S M]
[is_scalar_tower S R M] :
Equations
- p.module' = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul p.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[protected, instance]
def
submodule.is_scalar_tower
{S : Type u'}
{R : Type u}
{M : Type v}
[semiring S]
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M)
[has_scalar S R]
[module S M]
[is_scalar_tower S R M] :
is_scalar_tower S R ↥p
@[protected, instance]
def
submodule.no_zero_smul_divisors
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M)
[no_zero_smul_divisors R M] :
theorem
submodule.subtype_eq_val
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
{module_M : module R M}
(p : submodule R M) :
⇑(p.subtype) = subtype.val
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) :
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
- p.to_add_subgroup = {carrier := p.to_add_submonoid.carrier, zero_mem' := _, add_mem' := _, neg_mem' := _}
@[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) :
↑(p.to_add_subgroup) = ↑p
@[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} :
x ∈ p.to_add_subgroup ↔ x ∈ p
theorem
submodule.to_add_subgroup_injective
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
{module_M : module R 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) :
p.to_add_subgroup = p'.to_add_subgroup ↔ p = p'
theorem
submodule.to_add_subgroup_strict_mono
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
{module_M : module R M} :
theorem
submodule.to_add_subgroup_mono
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
{module_M : module R M} :
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} :
@[simp]
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} :
@[protected, instance]
def
submodule.add_comm_group
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
{module_M : module R M}
(p : submodule R M) :
Equations
- p.add_comm_group = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul p.to_add_subgroup.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg p.has_neg, sub := add_comm_group.sub p.to_add_subgroup.to_add_comm_group, sub_eq_add_neg := _, gsmul := add_comm_group.gsmul p.to_add_subgroup.to_add_comm_group, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
submodule.to_ordered_add_comm_monoid
{R : Type u}
[semiring R]
{M : Type u_1}
[ordered_add_comm_monoid M]
[module R M]
(S : submodule R 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}
[linear_ordered_add_comm_monoid M]
[module R M]
(S : submodule R M) :
A submodule of a linear_ordered_add_comm_monoid is a linear_ordered_add_comm_monoid.
@[protected, instance]
def
submodule.to_ordered_cancel_add_comm_monoid
{R : Type u}
[semiring R]
{M : Type u_1}
[ordered_cancel_add_comm_monoid M]
[module R M]
(S : submodule R M) :
A submodule of an ordered_cancel_add_comm_monoid is an ordered_cancel_add_comm_monoid.
@[protected, instance]
def
submodule.to_linear_ordered_cancel_add_comm_monoid
{R : Type u}
[semiring R]
{M : Type u_1}
[linear_ordered_cancel_add_comm_monoid M]
[module R M]
(S : submodule R M) :
A submodule of a linear_ordered_cancel_add_comm_monoid is a
linear_ordered_cancel_add_comm_monoid.
@[protected, instance]
def
submodule.to_ordered_add_comm_group
{R : Type u}
[ring R]
{M : Type u_1}
[ordered_add_comm_group M]
[module R M]
(S : submodule R 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}
[linear_ordered_add_comm_group M]
[module R M]
(S : submodule R 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}
[division_ring S]
[semiring R]
[add_comm_monoid M]
[module R M]
[has_scalar S R]
[module S M]
[is_scalar_tower S R M]
(p : submodule R M)
{s : S}
{x : M}
(s0 : s ≠ 0) :