The span of a set of vectors, as a submodule #
Submodule.span sis defined to be the smallest submodule containing the sets.
Notation #
- We introduce the notation
R ∙ vfor the span of a singleton,Submodule.span R {v}. This is\span, not the same as the scalar multiplication•/\bub.
theorem
Submodule.isPrincipal_iff
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Submodule R M)
:
instance
Submodule.instIsPrincipalSpanSingletonSet
{R : Type u_1}
[Semiring R]
(x : R)
:
(R ∙ x).IsPrincipal
noncomputable def
Submodule.IsPrincipal.generator
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
:
M
generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I
Equations
Instances For
theorem
Submodule.IsPrincipal.span_singleton_generator
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
:
@[simp]
theorem
Submodule.subset_span
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
s ⊆ ↑(span R s)
theorem
Submodule.span_monotone
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.span_eq
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
theorem
Submodule.coe_span_eq_self
{R : Type u_1}
{M : Type u_2}
{S : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[SetLike S M]
[AddSubmonoidClass S M]
[SMulMemClass S R M]
(s : S)
:
A version of Submodule.span_eq for subobjects closed under addition and scalar multiplication
and containing zero. In general, this should not be used directly, but can be used to quickly
generate proofs for specific types of subobjects.
theorem
Submodule.closure_subset_span
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
↑(AddSubmonoid.closure s) ⊆ ↑(span R s)
theorem
Submodule.closure_le_toAddSubmonoid_span
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
@[simp]
theorem
Submodule.span_closure
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
theorem
Submodule.span_induction
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{p : (x : M) → x ∈ span R s → Prop}
(mem : ∀ (x : M) (h : x ∈ s), p x ⋯)
(zero : p 0 ⋯)
(add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯)
(smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯)
{x : M}
(hx : x ∈ span R s)
:
p x hx
An induction principle for span membership. If p holds for 0 and all elements of s, and is
preserved under addition and scalar multiplication, then p holds for all elements of the span of
s.
theorem
Submodule.span_induction₂
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{N : Type u_6}
[AddCommMonoid N]
[Module R N]
{t : Set N}
{p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop}
(mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯)
(zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy)
(zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯)
(add_left :
∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz)
(add_right :
∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
p x y hx hy → p x z hx hz → p x (y + z) hx ⋯)
(smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy)
(smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯)
{a : M}
{b : N}
(ha : a ∈ span R s)
(hb : b ∈ span R t)
:
p a b ha hb
An induction principle for span membership. This is a version of Submodule.span_induction
for binary predicates.
theorem
Submodule.span_eq_closure
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
theorem
Submodule.closure_induction
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{p : (x : M) → x ∈ span R s → Prop}
(zero : p 0 ⋯)
(add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯)
(smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯)
{x : M}
(hx : x ∈ span R s)
:
p x hx
A variant of span_induction that combines ∀ x ∈ s, p x and ∀ r x, p x → p (r • x)
into a single condition ∀ r, ∀ x ∈ s, p (r • x), which can be easier to verify.
@[simp]
theorem
Submodule.span_span_coe_preimage
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
@[simp]
@[simp]
theorem
Disjoint.of_span
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s t : Set M}
(hst : Disjoint (Submodule.span R s) (Submodule.span R t))
:
theorem
Disjoint.of_span₀
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s t : Set M}
(hst : Disjoint (Submodule.span R s) (Submodule.span R t))
(h0s : 0 ∉ s)
:
Disjoint s t
span forms a Galois insertion with the coercion from submodule to set.
Equations
- Submodule.gi R M = { choice := fun (s : Set M) (x : ↑(Submodule.span R s) ⊆ s) => Submodule.span R s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Equations
- Submodule.«term_∙_» = Lean.ParserDescr.trailingNode `Submodule.«term_∙_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 70))
Instances For
Unexpander for R ∙ x notation. This needs to be defined separately because the {_}
notation is ambiguous, so we have to specify that it is the «term{_}» notation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Submodule.coe_sup
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p p' : Submodule R M)
:
theorem
Submodule.sup_toAddSubmonoid
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p p' : Submodule R M)
:
@[simp]
theorem
Submodule.mem_span_singleton_self
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
theorem
Submodule.nontrivial_span_singleton
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
(h : x ≠ 0)
:
Nontrivial ↥(R ∙ x)
theorem
Submodule.eq_span_singleton_of_surjective
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Submodule R M}
{f : R →ₗ[R] ↥s}
(hf : Function.Surjective ⇑f)
:
@[simp]
theorem
Submodule.span_zero_singleton
(R : Type u_1)
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.span_singleton_smul_le
(R : Type u_1)
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_6}
[SMul S R]
[SMul S M]
[IsScalarTower S R M]
(r : S)
(x : M)
:
@[simp]
theorem
Submodule.span_zero
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.mem_span_finite_of_mem_span
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Set M}
{x : M}
(hx : x ∈ span R S)
:
For every element in the span of a set, there exists a finite subset of the set such that the element is contained in the span of the subset.
theorem
Submodule.sup_toAddSubgroup
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
(p p' : Submodule R M)
:
theorem
Submodule.span_range_update_add_smul
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
[DecidableEq ι]
{i j : ι}
(hij : i ≠ j)
(v : ι → M)
(r : R)
:
theorem
Submodule.span_range_update_sub_smul
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
[DecidableEq ι]
{i j : ι}
(hij : i ≠ j)
(v : ι → M)
(r : R)
:
@[reducible, inline]
abbrev
Module.IsPrincipal
(R : Type u_1)
(M : Type u_2)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
A module is principal if it is generated by a single element.
Equations
Instances For
theorem
Module.isPrincipal_def
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Module.isPrincipal_submodule_iff
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
:
theorem
Module.IsPrincipal.of_surjective
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(f : M →ₗ[R] M₂)
(hf : Function.Surjective ⇑f)
[IsPrincipal R M]
:
IsPrincipal R M₂
theorem
LinearEquiv.isPrincipal_iff
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(e : M ≃ₗ[R] M₂)
:
theorem
Commute.span_left
{R : Type u_6}
{A : Type u_7}
[Semiring R]
[NonUnitalNonAssocSemiring A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
{s : Set A}
{x : A}
(h : ∀ y ∈ s, Commute y x)
(y : A)
:
y ∈ Submodule.span R s → Commute y x
In a non-unital algebra, if every element of a set s commutes with x, then every element of
Submodule.span R s commutes with x.
theorem
Commute.span_right
{R : Type u_6}
{A : Type u_7}
[Semiring R]
[NonUnitalNonAssocSemiring A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
{s : Set A}
{x : A}
(h : ∀ y ∈ s, Commute x y)
(y : A)
:
y ∈ Submodule.span R s → Commute x y
In a non-unital algebra, if x commutes with every element of a set s, then x commutes
with every element of Submodule.span R s.