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]
[semimodule R M]
(s : submodule 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
- 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.
@[instance]
def
submodule.has_coe_t
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[instance]
@[instance]
def
submodule.has_coe_to_sort
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
has_coe_to_sort (submodule R M)
@[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} :
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} :
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} :
theorem
submodule.ext'_iff
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p q : submodule R M} :
@[ext]
theorem
submodule.ext
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{p q : submodule R M}
(h : ∀ (x : M), x ∈ p ↔ x ∈ q) :
p = q
theorem
submodule.to_add_submonoid_injective
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[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} :
p.to_add_submonoid = q.to_add_submonoid ↔ p = q
@[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} :
@[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}
(h₁ : x ∈ p)
(h₂ : 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)
(h : 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}
(a : ∀ (c : ι), c ∈ t → f 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)
(hyp : ∀ (c : ι), c ∈ t → f c ∈ 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) :
@[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) :
@[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) :
@[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) :
has_scalar R ↥p
@[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) :
@[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} :
@[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} :
@[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) :
@[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} :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
semimodule R ↥p
Equations
- p.semimodule = {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 := _}
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.
@[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) :
⇑(p.subtype) = subtype.val
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}
(hx : x ∈ p) :
def
submodule.to_add_subgroup
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
{semimodule_M : semimodule 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]
{semimodule_M : semimodule R M}
(p : submodule R M) :
↑(p.to_add_subgroup) = ↑p
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}
(a : x ∈ p)
(a_1 : 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} :
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}
(a : y ∈ 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}
(a : x ∈ p) :
@[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
- p.add_comm_group = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg p.has_neg, add_left_neg := _, add_comm := _}
@[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) :
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}
(r0 : r ≠ 0) :
Subspace of a vector space. Defined to equal submodule.