The span of a set of vectors, as a submodule #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
submodule.span sis defined to be the smallest submodule containing the sets.
Notations #
- We introduce the notation
R ∙ vfor the span of a singleton,submodule.span R {v}. This is\., not the same as the scalar multiplication•/\bub.
def
submodule.span
(R : Type u_1)
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M) :
submodule R M
The span of a set s ⊆ M is the smallest submodule of M that contains s.
Equations
- submodule.span R s = has_Inf.Inf {p : submodule R M | s ⊆ ↑p}
Instances for ↥submodule.span
theorem
submodule.subset_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
s ⊆ ↑(submodule.span R s)
theorem
submodule.span_le
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M}
{p : submodule R M} :
submodule.span R s ≤ p ↔ s ⊆ ↑p
theorem
submodule.span_mono
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s t : set M}
(h : s ⊆ t) :
submodule.span R s ≤ submodule.span R t
theorem
submodule.span_monotone
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
submodule.span_eq_of_le
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
{s : set M}
(h₁ : s ⊆ ↑p)
(h₂ : p ≤ submodule.span R s) :
submodule.span R s = p
theorem
submodule.span_eq
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M) :
submodule.span R ↑p = p
theorem
submodule.span_eq_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s t : set M}
(hs : s ⊆ ↑(submodule.span R t))
(ht : t ⊆ ↑(submodule.span R s)) :
submodule.span R s = submodule.span R t
@[simp]
theorem
submodule.span_coe_eq_restrict_scalars
{R : Type u_1}
{M : Type u_4}
{S : Type u_7}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
[semiring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M] :
A version of submodule.span_eq for when the span is by a smaller ring.
theorem
submodule.map_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(s : set M) :
submodule.map f (submodule.span R s) = submodule.span R₂ (⇑f '' s)
theorem
linear_map.map_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(s : set M) :
submodule.map f (submodule.span R s) = submodule.span R₂ (⇑f '' s)
Alias of submodule.map_span.
theorem
submodule.map_span_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(s : set M)
(N : submodule R₂ M₂) :
submodule.map f (submodule.span R s) ≤ N ↔ ∀ (m : M), m ∈ s → ⇑f m ∈ N
theorem
linear_map.map_span_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
(s : set M)
(N : submodule R₂ M₂) :
submodule.map f (submodule.span R s) ≤ N ↔ ∀ (m : M), m ∈ s → ⇑f m ∈ N
Alias of submodule.map_span_le.
@[simp]
theorem
submodule.span_insert_zero
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
submodule.span R (has_insert.insert 0 s) = submodule.span R s
theorem
submodule.span_preimage_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
(f : M →ₛₗ[σ₁₂] M₂)
(s : set M₂) :
submodule.span R (⇑f ⁻¹' s) ≤ submodule.comap f (submodule.span R₂ s)
theorem
linear_map.span_preimage_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
(f : M →ₛₗ[σ₁₂] M₂)
(s : set M₂) :
submodule.span R (⇑f ⁻¹' s) ≤ submodule.comap f (submodule.span R₂ s)
Alias of submodule.span_preimage_le.
theorem
submodule.closure_subset_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
↑(add_submonoid.closure s) ⊆ ↑(submodule.span R s)
theorem
submodule.closure_le_to_add_submonoid_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
@[simp]
theorem
submodule.span_closure
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
submodule.span R ↑(add_submonoid.closure s) = submodule.span R s
theorem
submodule.span_induction
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x : M}
{s : set M}
{p : M → Prop}
(h : x ∈ submodule.span R s)
(Hs : ∀ (x : M), x ∈ s → p x)
(H0 : p 0)
(H1 : ∀ (x y : M), p x → p y → p (x + y))
(H2 : ∀ (a : R) (x : M), p x → p (a • x)) :
p x
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_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M}
{p : Π (x : M), x ∈ submodule.span R s → Prop}
(Hs : ∀ (x : M) (h : x ∈ s), p x _)
(H0 : p 0 _)
(H1 : ∀ (x : M) (hx : x ∈ submodule.span R s) (y : M) (hy : y ∈ submodule.span R s), p x hx → p y hy → p (x + y) _)
(H2 : ∀ (a : R) (x : M) (hx : x ∈ submodule.span R s), p x hx → p (a • x) _)
{x : M}
(hx : x ∈ submodule.span R s) :
p x hx
A dependent version of submodule.span_induction.
@[simp]
theorem
submodule.span_span_coe_preimage
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
submodule.span R (coe ⁻¹' s) = ⊤
theorem
submodule.span_nat_eq_add_submonoid_closure
{M : Type u_4}
[add_comm_monoid M]
(s : set M) :
@[simp]
theorem
submodule.span_nat_eq
{M : Type u_4}
[add_comm_monoid M]
(s : add_submonoid M) :
(submodule.span ℕ ↑s).to_add_submonoid = s
@[simp]
theorem
submodule.span_int_eq
{M : Type u_1}
[add_comm_group M]
(s : add_subgroup M) :
(submodule.span ℤ ↑s).to_add_subgroup = s
@[protected]
span forms a Galois insertion with the coercion from submodule to set.
Equations
- submodule.gi R M = {choice := λ (s : set M) (_x : ↑(submodule.span R s) ≤ s), submodule.span R s, gc := _, le_l_u := _, choice_eq := _}
@[simp]
theorem
submodule.span_empty
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
submodule.span R ∅ = ⊥
@[simp]
theorem
submodule.span_univ
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
submodule.span_union
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(s t : set M) :
submodule.span R (s ∪ t) = submodule.span R s ⊔ submodule.span R t
theorem
submodule.span_Union
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Sort u_2}
(s : ι → set M) :
submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), submodule.span R (s i)
theorem
submodule.span_Union₂
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Sort u_2}
{κ : ι → Sort u_3}
(s : Π (i : ι), κ i → set M) :
submodule.span R (⋃ (i : ι) (j : κ i), s i j) = ⨆ (i : ι) (j : κ i), submodule.span R (s i j)
theorem
submodule.span_attach_bUnion
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
[decidable_eq M]
{α : Type u_2}
(s : finset α)
(f : ↥s → finset M) :
submodule.span R ↑(s.attach.bUnion f) = ⨆ (x : ↥s), submodule.span R ↑(f x)
theorem
submodule.sup_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
{s : set M} :
p ⊔ submodule.span R s = submodule.span R (↑p ∪ s)
theorem
submodule.span_sup
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
{s : set M} :
submodule.span R s ⊔ p = submodule.span R (s ∪ ↑p)
theorem
submodule.span_eq_supr_of_singleton_spans
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M) :
submodule.span R s = ⨆ (x : M) (H : x ∈ s), submodule.span R {x}
theorem
submodule.span_range_eq_supr
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Type u_2}
{v : ι → M} :
submodule.span R (set.range v) = ⨆ (i : ι), submodule.span R {v i}
theorem
submodule.span_smul_le
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M)
(r : R) :
submodule.span R (r • s) ≤ submodule.span R s
theorem
submodule.subset_span_trans
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{U V W : set M}
(hUV : U ⊆ ↑(submodule.span R V))
(hVW : V ⊆ ↑(submodule.span R W)) :
U ⊆ ↑(submodule.span R W)
theorem
submodule.span_smul_eq_of_is_unit
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M)
(r : R)
(hr : is_unit r) :
submodule.span R (r • s) = submodule.span R s
See submodule.span_smul_eq (in ring_theory.ideal.operations) for
span R (r • s) = r • span R s that holds for arbitrary r in a comm_semiring.
theorem
submodule.mem_Sup_of_directed
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set (submodule R M)}
{z : M}
(hs : s.nonempty)
(hdir : directed_on has_le.le s) :
theorem
submodule.coe_scott_continuous
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
We can regard coe_supr_of_chain as the statement that coe : (submodule R M) → set M is
Scott continuous for the ω-complete partial order induced by the complete lattice structures.
theorem
submodule.sup_to_add_submonoid
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p p' : submodule R M) :
(p ⊔ p').to_add_submonoid = p.to_add_submonoid ⊔ p'.to_add_submonoid
theorem
submodule.sup_to_add_subgroup
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
(p ⊔ p').to_add_subgroup = p.to_add_subgroup ⊔ p'.to_add_subgroup
theorem
submodule.mem_span_singleton_self
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
x ∈ submodule.span R {x}
theorem
submodule.nontrivial_span_singleton
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x : M}
(h : x ≠ 0) :
nontrivial ↥(submodule.span R {x})
theorem
submodule.mem_span_singleton
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x y : M} :
@[simp]
theorem
submodule.span_zero_singleton
(R : Type u_1)
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
submodule.span R {0} = ⊥
theorem
submodule.span_singleton_eq_range
(R : Type u_1)
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(y : M) :
↑(submodule.span R {y}) = set.range (λ (_x : R), _x • y)
theorem
submodule.span_singleton_smul_le
(R : Type u_1)
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{S : Type u_2}
[monoid S]
[has_smul S R]
[mul_action S M]
[is_scalar_tower S R M]
(r : S)
(x : M) :
submodule.span R {r • x} ≤ submodule.span R {x}
theorem
submodule.span_singleton_group_smul_eq
(R : Type u_1)
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{G : Type u_2}
[group G]
[has_smul G R]
[mul_action G M]
[is_scalar_tower G R M]
(g : G)
(x : M) :
submodule.span R {g • x} = submodule.span R {x}
theorem
submodule.span_singleton_smul_eq
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{r : R}
(hr : is_unit r)
(x : M) :
submodule.span R {r • x} = submodule.span R {x}
theorem
submodule.disjoint_span_singleton
{K : Type u_1}
{E : Type u_2}
[division_ring K]
[add_comm_group E]
[module K E]
{s : submodule K E}
{x : E} :
theorem
submodule.disjoint_span_singleton'
{K : Type u_1}
{E : Type u_2}
[division_ring K]
[add_comm_group E]
[module K E]
{p : submodule K E}
{x : E}
(x0 : x ≠ 0) :
disjoint p (submodule.span K {x}) ↔ x ∉ p
theorem
submodule.mem_span_singleton_trans
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x y z : M}
(hxy : x ∈ submodule.span R {y})
(hyz : y ∈ submodule.span R {z}) :
x ∈ submodule.span R {z}
theorem
submodule.mem_span_insert
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x : M}
{s : set M}
{y : M} :
x ∈ submodule.span R (has_insert.insert y s) ↔ ∃ (a : R) (z : M) (H : z ∈ submodule.span R s), x = a • y + z
theorem
submodule.span_insert
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M)
(s : set M) :
submodule.span R (has_insert.insert x s) = submodule.span R {x} ⊔ submodule.span R s
theorem
submodule.span_insert_eq_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x : M}
{s : set M}
(h : x ∈ submodule.span R s) :
submodule.span R (has_insert.insert x s) = submodule.span R s
theorem
submodule.span_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
submodule.span R ↑(submodule.span R s) = submodule.span R s
theorem
submodule.span_le_restrict_scalars
(R : Type u_1)
{M : Type u_4}
(S : Type u_7)
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M)
[semiring S]
[has_smul R S]
[module S M]
[is_scalar_tower R S M] :
submodule.span R s ≤ submodule.restrict_scalars R (submodule.span S s)
If R is "smaller" ring than S then the span by R is smaller than the span by S.
@[simp]
theorem
submodule.span_subset_span
(R : Type u_1)
{M : Type u_4}
(S : Type u_7)
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M)
[semiring S]
[has_smul R S]
[module S M]
[is_scalar_tower R S M] :
↑(submodule.span R s) ⊆ ↑(submodule.span S s)
A version of submodule.span_le_restrict_scalars with coercions.
theorem
submodule.span_span_of_tower
(R : Type u_1)
{M : Type u_4}
(S : Type u_7)
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M)
[semiring S]
[has_smul R S]
[module S M]
[is_scalar_tower R S M] :
submodule.span S ↑(submodule.span R s) = submodule.span S s
Taking the span by a large ring of the span by the small ring is the same as taking the span by just the large ring.
@[simp]
theorem
submodule.span_singleton_eq_bot
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{x : M} :
submodule.span R {x} = ⊥ ↔ x = 0
@[simp]
theorem
submodule.span_zero
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
submodule.span R 0 = ⊥
theorem
submodule.span_singleton_eq_span_singleton
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
{x y : M} :
submodule.span R {x} = submodule.span R {y} ↔ ∃ (z : Rˣ), z • x = y
@[simp]
theorem
submodule.span_image
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
{s : set M}
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂) :
submodule.span R₂ (⇑f '' s) = submodule.map f (submodule.span R s)
theorem
submodule.apply_mem_span_image_of_mem_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
{x : M}
{s : set M}
(h : x ∈ submodule.span R s) :
⇑f x ∈ submodule.span R₂ (⇑f '' s)
@[simp]
theorem
submodule.map_subtype_span_singleton
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{p : submodule R M}
(x : ↥p) :
submodule.map p.subtype (submodule.span R {x}) = submodule.span R {↑x}
theorem
submodule.not_mem_span_of_apply_not_mem_span_image
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[add_comm_monoid M₂]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
{x : M}
{s : set M}
(h : ⇑f x ∉ submodule.span R₂ (⇑f '' s)) :
x ∉ submodule.span R s
f is an explicit argument so we can apply this theorem and obtain h as a new goal.
theorem
submodule.supr_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Sort u_2}
(p : ι → set M) :
(⨆ (i : ι), submodule.span R (p i)) = submodule.span R (⋃ (i : ι), p i)
theorem
submodule.supr_to_add_submonoid
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Sort u_2}
(p : ι → submodule R M) :
(⨆ (i : ι), p i).to_add_submonoid = ⨆ (i : ι), (p i).to_add_submonoid
theorem
submodule.supr_induction
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Sort u_2}
(p : ι → submodule R M)
{C : M → Prop}
{x : M}
(hx : x ∈ ⨆ (i : ι), p i)
(hp : ∀ (i : ι) (x : M), x ∈ p i → C x)
(h0 : C 0)
(hadd : ∀ (x y : M), C x → C y → C (x + y)) :
C x
An induction principle for elements of ⨆ i, p i.
If C holds for 0 and all elements of p i for all i, and is preserved under addition,
then it holds for all elements of the supremum of p.
theorem
submodule.supr_induction'
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Sort u_2}
(p : ι → submodule R M)
{C : Π (x : M), (x ∈ ⨆ (i : ι), p i) → Prop}
(hp : ∀ (i : ι) (x : M) (H : x ∈ p i), C x _)
(h0 : C 0 _)
(hadd : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i), C x hx → C y hy → C (x + y) _)
{x : M}
(hx : x ∈ ⨆ (i : ι), p i) :
C x hx
A dependent version of submodule.supr_induction.
@[simp]
theorem
submodule.span_singleton_le_iff_mem
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(m : M)
(p : submodule R M) :
submodule.span R {m} ≤ p ↔ m ∈ p
theorem
submodule.singleton_span_is_compact_element
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
theorem
submodule.finset_span_is_compact_element
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(S : finset M) :
The span of a finite subset is compact in the lattice of submodules.
theorem
submodule.finite_span_is_compact_element
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(S : set M)
(h : S.finite) :
The span of a finite subset is compact in the lattice of submodules.
@[protected, instance]
def
submodule.is_compactly_generated
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
submodule.submodule_eq_Sup_le_nonzero_spans
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M) :
p = has_Sup.Sup {T : submodule R M | ∃ (m : M) (hm : m ∈ p) (hz : m ≠ 0), T = submodule.span R {m}}
A submodule is equal to the supremum of the spans of the submodule's nonzero elements.
theorem
submodule.lt_sup_iff_not_mem
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{I : submodule R M}
{a : M} :
I < I ⊔ submodule.span R {a} ↔ a ∉ I
theorem
submodule.mem_span_finite_of_mem_span
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{S : set M}
{x : M}
(hx : x ∈ submodule.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.
def
submodule.prod
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
(p : submodule R M)
{M' : Type u_8}
[add_comm_monoid M']
[module R M']
(q₁ : submodule R M') :
The product of two submodules is a submodule.
theorem
submodule.span_prod_le
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type u_8}
[add_comm_monoid M']
[module R M']
(s : set M)
(t : set M') :
submodule.span R (s ×ˢ t) ≤ (submodule.span R s).prod (submodule.span R t)
@[simp]
theorem
submodule.prod_top
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type u_8}
[add_comm_monoid M']
[module R M'] :
@[simp]
theorem
submodule.prod_bot
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
{M' : Type u_8}
[add_comm_monoid M']
[module R M'] :
@[simp]
theorem
submodule.span_neg
{R : Type u_1}
{M : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set M) :
submodule.span R (-s) = submodule.span R s
theorem
submodule.mem_span_insert'
{R : Type u_1}
{M : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{x y : M}
{s : set M} :
x ∈ submodule.span R (has_insert.insert y s) ↔ ∃ (a : R), x + a • y ∈ submodule.span R s
@[protected, instance]
def
submodule.is_modular_lattice
{R : Type u_1}
{M : Type u_4}
[ring R]
[add_comm_group M]
[module R M] :
is_modular_lattice (submodule R M)
theorem
submodule.comap_map_eq
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring R₂]
[add_comm_group M]
[module R M]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{F : Type u_8}
[sc : semilinear_map_class F τ₁₂ M M₂]
(f : F)
(p : submodule R M) :
submodule.comap f (submodule.map f p) = p ⊔ linear_map.ker f
theorem
submodule.comap_map_eq_self
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring R₂]
[add_comm_group M]
[module R M]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{F : Type u_8}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
{p : submodule R M}
(h : linear_map.ker f ≤ p) :
submodule.comap f (submodule.map f p) = p
@[protected]
theorem
linear_map.map_le_map_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring R₂]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{F : Type u_8}
[sc : semilinear_map_class F τ₁₂ M M₂]
(f : F)
{p p' : submodule R M} :
submodule.map f p ≤ submodule.map f p' ↔ p ≤ p' ⊔ linear_map.ker f
theorem
linear_map.map_le_map_iff'
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring R₂]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{F : Type u_8}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
(hf : linear_map.ker f = ⊥)
{p p' : submodule R M} :
submodule.map f p ≤ submodule.map f p' ↔ p ≤ p'
theorem
linear_map.map_injective
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring R₂]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{F : Type u_8}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
(hf : linear_map.ker f = ⊥) :
theorem
linear_map.map_eq_top_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring R₂]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{F : Type u_8}
[sc : semilinear_map_class F τ₁₂ M M₂]
{f : F}
(hf : linear_map.range f = ⊤)
{p : submodule R M} :
submodule.map f p = ⊤ ↔ p ⊔ linear_map.ker f = ⊤
@[simp]
theorem
linear_map.to_span_singleton_apply
(R : Type u_1)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M)
(b : R) :
⇑(linear_map.to_span_singleton R M x) b = b • x
def
linear_map.to_span_singleton
(R : Type u_1)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
Given an element x of a module M over R, the natural map from
R to scalar multiples of x.
Equations
theorem
linear_map.span_singleton_eq_range
(R : Type u_1)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
submodule.span R {x} = linear_map.range (linear_map.to_span_singleton R M x)
The range of to_span_singleton x is the span of x.
@[simp]
theorem
linear_map.to_span_singleton_one
(R : Type u_1)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
⇑(linear_map.to_span_singleton R M x) 1 = x
@[simp]
theorem
linear_map.to_span_singleton_zero
(R : Type u_1)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M] :
linear_map.to_span_singleton R M 0 = 0
theorem
linear_map.eq_on_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{s : set M}
{f g : M →ₛₗ[σ₁₂] M₂}
(H : set.eq_on ⇑f ⇑g s)
⦃x : M⦄
(h : x ∈ submodule.span R s) :
If two linear maps are equal on a set s, then they are equal on submodule.span s.
See also linear_map.eq_on_span' for a version using set.eq_on.
theorem
linear_map.eq_on_span'
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{s : set M}
{f g : M →ₛₗ[σ₁₂] M₂}
(H : set.eq_on ⇑f ⇑g s) :
set.eq_on ⇑f ⇑g ↑(submodule.span R s)
If two linear maps are equal on a set s, then they are equal on submodule.span s.
This version uses set.eq_on, and the hidden argument will expand to h : x ∈ (span R s : set M).
See linear_map.eq_on_span for a version that takes h : x ∈ span R s as an argument.
theorem
linear_map.ext_on
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{s : set M}
{f g : M →ₛₗ[σ₁₂] M₂}
(hv : submodule.span R s = ⊤)
(h : set.eq_on ⇑f ⇑g s) :
f = g
If s generates the whole module and linear maps f, g are equal on s, then they are
equal.
theorem
linear_map.ext_on_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{ι : Type u_3}
{v : ι → M}
{f g : M →ₛₗ[σ₁₂] M₂}
(hv : submodule.span R (set.range v) = ⊤)
(h : ∀ (i : ι), ⇑f (v i) = ⇑g (v i)) :
f = g
If the range of v : ι → M generates the whole module and linear maps f, g are equal at
each v i, then they are equal.
theorem
linear_map.ker_to_span_singleton
(R : Type u_1)
(M : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
{x : M}
(h : x ≠ 0) :
linear_map.ker (linear_map.to_span_singleton R M x) = ⊥
theorem
linear_map.span_singleton_sup_ker_eq_top
{K : Type u_3}
{V : Type u_6}
[field K]
[add_comm_group V]
[module K V]
(f : V →ₗ[K] K)
{x : V}
(hx : ⇑f x ≠ 0) :
submodule.span K {x} ⊔ linear_map.ker f = ⊤
noncomputable
def
linear_equiv.to_span_nonzero_singleton
(R : Type u_1)
(M : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(x : M)
(h : x ≠ 0) :
R ≃ₗ[R] ↥(submodule.span R {x})
Given a nonzero element x of a torsion-free module M over a ring R, the natural
isomorphism from R to the span of x given by $r \mapsto r \cdot x$.
Equations
- linear_equiv.to_span_nonzero_singleton R M x h = (linear_equiv.of_injective (linear_map.to_span_singleton R M x) _).trans (linear_equiv.of_eq (linear_map.range (linear_map.to_span_singleton R M x)) (submodule.span R {x}) _)
theorem
linear_equiv.to_span_nonzero_singleton_one
(R : Type u_1)
(M : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(x : M)
(h : x ≠ 0) :
⇑(linear_equiv.to_span_nonzero_singleton R M x h) 1 = ⟨x, _⟩
@[reducible]
noncomputable
def
linear_equiv.coord
(R : Type u_1)
(M : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(x : M)
(h : x ≠ 0) :
↥(submodule.span R {x}) ≃ₗ[R] R
Given a nonzero element x of a torsion-free module M over a ring R, the natural
isomorphism from the span of x to R given by $r \cdot x \mapsto r$.
theorem
linear_equiv.coord_self
(R : Type u_1)
(M : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(x : M)
(h : x ≠ 0) :
⇑(linear_equiv.coord R M x h) ⟨x, _⟩ = 1
theorem
linear_equiv.coord_apply_smul
(R : Type u_1)
(M : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(x : M)
(h : x ≠ 0)
(y : ↥(submodule.span R {x})) :
⇑(linear_equiv.coord R M x h) y • x = ↑y