The span of a set of vectors, as a submodule

• Submodule.span s is defined to be the smallest submodule containing the set s.

Notations

• We introduce the notation R ∙ v for 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] [AddCommMonoid 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 = sInf {p : Submodule R M | s ⊆ ↑p}

theorem Submodule.isPrincipal_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) : Submodule.IsPrincipal S ↔ ∃ (a : M), S = Submodule.span R {a}

class Submodule.IsPrincipal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) : Prop

An R-submodule of M is principal if it is generated by one element.

• principal' : ∃ (a : M), S = Submodule.span R {a}

Instances

• IsBezout.span_pair_isPrincipal
• IsSimpleModule.instIsPrincipalToSemiringToAddCommMonoid
• bot_isPrincipal
• top_isPrincipal

theorem Submodule.IsPrincipal.principal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] : ∃ (a : M), S = Submodule.span R {a}

theorem Submodule.mem_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} : x ∈ Submodule.span R s ↔ ∀ (p : Submodule R M), s ⊆ ↑p → x ∈ p

theorem Submodule.subset_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid 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] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] {s : Set M} {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] [AddCommMonoid M] [Module R M] : Monotone (Submodule.span R)

theorem Submodule.span_eq_of_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid 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] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] {s : Set M} {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_restrictScalars {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Submodule.span S ↑p = Submodule.restrictScalars S p

A version of Submodule.span_eq for when the span is by a smaller ring.

theorem Submodule.image_span_subset {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) : ⇑f '' ↑(Submodule.span R s) ⊆ ↑N ↔ ∀ m ∈ s, f m ∈ N

A version of Submodule.map_span_le that does not require the RingHomSurjective assumption.

theorem Submodule.image_span_subset_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M) : ⇑f '' ↑(Submodule.span R s) ⊆ ↑(Submodule.span R₂ (⇑f '' s))

theorem Submodule.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) : Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)

theorem LinearMap.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (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] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) : Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N

theorem LinearMap.map_span_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) : Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ 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] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R (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] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M₂) : Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)

theorem LinearMap.span_preimage_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (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] [AddCommMonoid M] [Module R M] {s : Set M} : ↑(AddSubmonoid.closure s) ⊆ ↑(Submodule.span R s)

theorem Submodule.closure_le_toAddSubmonoid_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : AddSubmonoid.closure s ≤ (Submodule.span R s).toAddSubmonoid

@[simp]

theorem Submodule.span_closure {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R ↑(AddSubmonoid.closure s) = Submodule.span R s

theorem Submodule.span_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {p : M → Prop} (h : x ∈ Submodule.span R s) (mem : ∀ x ∈ s, p x) (zero : p 0) (add : ∀ (x y : M), p x → p y → p (x + y)) (smul : ∀ (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] [AddCommMonoid M] [Module R M] {s : Set M} {p : M → M → Prop} {a : M} {b : M} (ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R s) (mem_mem : ∀ x ∈ s, ∀ y ∈ s, p x y) (zero_left : ∀ (y : M), p 0 y) (zero_right : ∀ (x : M), p x 0) (add_left : ∀ (x₁ x₂ y : M), p x₁ y → p x₂ y → p (x₁ + x₂) y) (add_right : ∀ (x y₁ y₂ : M), p x y₁ → p x y₂ → p x (y₁ + y₂)) (smul_left : ∀ (r : R) (x y : M), p x y → p (r • x) y) (smul_right : ∀ (r : R) (x y : M), p x y → p x (r • y)) : p a b

An induction principle for span membership. This is a version of Submodule.span_induction for binary predicates.

theorem Submodule.span_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (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) ⋯) (smul : ∀ (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.

theorem Submodule.span_eq_closure {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : (Submodule.span R s).toAddSubmonoid = AddSubmonoid.closure (Set.univ • s)

theorem Submodule.closure_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {p : M → Prop} (h : x ∈ Submodule.span R s) (zero : p 0) (add : ∀ (x y : M), p x → p y → p (x + y)) (smul_mem : ∀ (r : R), ∀ x ∈ s, p (r • x)) : p x

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.

theorem Submodule.closure_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (zero : p 0 ⋯) (add : ∀ (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) ⋯) (smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯) {x : M} (hx : x ∈ Submodule.span R s) : p x hx

A dependent version of Submodule.closure_induction.

@[simp]

theorem Submodule.span_span_coe_preimage {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R (Subtype.val ⁻¹' s) = ⊤

@[simp]

theorem Submodule.span_setOf_mem_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R {x : ↥(Submodule.span R s) | ↑x ∈ s} = ⊤

theorem Submodule.span_nat_eq_addSubmonoid_closure {M : Type u_4} [AddCommMonoid M] (s : Set M) : (Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

@[simp]

theorem Submodule.span_nat_eq {M : Type u_4} [AddCommMonoid M] (s : AddSubmonoid M) : (Submodule.span ℕ ↑s).toAddSubmonoid = s

theorem Submodule.span_int_eq_addSubgroup_closure {M : Type u_9} [AddCommGroup M] (s : Set M) : Submodule.toAddSubgroup (Submodule.span ℤ s) = AddSubgroup.closure s

@[simp]

theorem Submodule.span_int_eq {M : Type u_9} [AddCommGroup M] (s : AddSubgroup M) : Submodule.toAddSubgroup (Submodule.span ℤ ↑s) = s

def Submodule.gi (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : GaloisInsertion (Submodule.span R) SetLike.coe

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 := ⋯ }

@[simp]

theorem Submodule.span_empty {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : Submodule.span R ∅ = ⊥

@[simp]

theorem Submodule.span_univ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : Submodule.span R Set.univ = ⊤

theorem Submodule.span_union {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (t : Set M) : Submodule.span R (s ∪ t) = Submodule.span R s ⊔ Submodule.span R t

theorem Submodule.span_iUnion {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (s : ι → Set M) : Submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), Submodule.span R (s i)

theorem Submodule.span_iUnion₂ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_10} {κ : ι → Sort u_9} (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_biUnion {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq M] {α : Type u_9} (s : Finset α) (f : { x : α // x ∈ s } → Finset M) : Submodule.span R ↑(Finset.biUnion (Finset.attach s) f) = ⨆ (x : { x : α // x ∈ s }), Submodule.span R ↑(f x)

theorem Submodule.sup_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} : Submodule.span R s ⊔ p = Submodule.span R (s ∪ ↑p)

def Submodule.«term_∙_» : Lean.TrailingParserDescr

Equations

• Submodule.«term_∙_» = Lean.ParserDescr.trailingNode `Submodule.term_∙_ 1000 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 0))

theorem Submodule.span_eq_iSup_of_singleton_spans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule.span R s = ⨆ x ∈ s, Submodule.span R {x}

theorem Submodule.span_range_eq_iSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_9} {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] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] {U : Set M} {V : Set M} {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_isUnit {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) (hr : IsUnit r) : Submodule.span R (r • s) = Submodule.span R s

See Submodule.span_smul_eq (in RingTheory.Ideal.Operations) for span R (r • s) = r • span R s that holds for arbitrary r in a CommSemiring.

@[simp]

theorem Submodule.coe_iSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (fun (x x_1 : Submodule R M) => x ≤ x_1) S) : ↑(iSup S) = ⋃ (i : ι), ↑(S i)

@[simp]

theorem Submodule.mem_iSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (fun (x x_1 : Submodule R M) => x ≤ x_1) S) {x : M} : x ∈ iSup S ↔ ∃ (i : ι), x ∈ S i

theorem Submodule.mem_sSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Submodule R M)} {z : M} (hs : Set.Nonempty s) (hdir : DirectedOn (fun (x x_1 : Submodule R M) => x ≤ x_1) s) : z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

@[simp]

theorem Submodule.coe_iSup_of_chain {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (a : ℕ →o Submodule R M) : ↑(⨆ (k : ℕ), a k) = ⋃ (k : ℕ), ↑(a k)

theorem Submodule.coe_scott_continuous {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : OmegaCompletePartialOrder.Continuous' SetLike.coe

We can regard coe_iSup_of_chain as the statement that (↑) : (Submodule R M) → Set M is Scott continuous for the ω-complete partial order induced by the complete lattice structures.

@[simp]

theorem Submodule.mem_iSup_of_chain {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (a : ℕ →o Submodule R M) (m : M) : m ∈ ⨆ (k : ℕ), a k ↔ ∃ (k : ℕ), m ∈ a k

theorem Submodule.mem_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {p : Submodule R M} {p' : Submodule R M} : x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x

theorem Submodule.mem_sup' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {p : Submodule R M} {p' : Submodule R M} : x ∈ p ⊔ p' ↔ ∃ (y : ↥p) (z : ↥p'), ↑y + ↑z = x

theorem Submodule.exists_add_eq_of_codisjoint {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : Codisjoint p p') (x : M) : ∃ y ∈ p, ∃ z ∈ p', y + z = x

theorem Submodule.coe_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : ↑(p ⊔ p') = ↑p + ↑p'

theorem Submodule.sup_toAddSubmonoid {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid

theorem Submodule.sup_toAddSubgroup {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : Submodule.toAddSubgroup (p ⊔ p') = Submodule.toAddSubgroup p ⊔ Submodule.toAddSubgroup p'

theorem Submodule.mem_span_singleton_self {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid 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] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] {x : M} {y : M} : x ∈ Submodule.span R {y} ↔ ∃ (a : R), a • y = x

theorem Submodule.le_span_singleton_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Submodule R M} {v₀ : M} : s ≤ Submodule.span R {v₀} ↔ ∀ v ∈ s, ∃ (r : R), r • v₀ = v

theorem Submodule.span_singleton_eq_top_iff (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : Submodule.span R {x} = ⊤ ↔ ∀ (v : M), ∃ (r : R), r • x = v

@[simp]

theorem Submodule.span_zero_singleton (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : Submodule.span R {0} = ⊥

theorem Submodule.span_singleton_eq_range (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (y : M) : ↑(Submodule.span R {y}) = Set.range fun (x : R) => x • y

theorem Submodule.span_singleton_smul_le (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_9} [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower 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] [AddCommMonoid M] [Module R M] {G : Type u_9} [Group G] [SMul G R] [MulAction G M] [IsScalarTower 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] [AddCommMonoid M] [Module R M] {r : R} (hr : IsUnit r) (x : M) : Submodule.span R {r • x} = Submodule.span R {x}

theorem Submodule.disjoint_span_singleton {K : Type u_9} {E : Type u_10} [DivisionRing K] [AddCommGroup E] [Module K E] {s : Submodule K E} {x : E} : Disjoint s (Submodule.span K {x}) ↔ x ∈ s → x = 0

theorem Submodule.disjoint_span_singleton' {K : Type u_9} {E : Type u_10} [DivisionRing K] [AddCommGroup 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] [AddCommMonoid M] [Module R M] {x : M} {y : M} {z : M} (hxy : x ∈ Submodule.span R {y}) (hyz : y ∈ Submodule.span R {z}) : x ∈ Submodule.span R {z}

theorem Submodule.span_insert {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (s : Set M) : Submodule.span R (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] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} (h : x ∈ Submodule.span R s) : Submodule.span R (insert x s) = Submodule.span R s

theorem Submodule.span_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R ↑(Submodule.span R s) = Submodule.span R s

theorem Submodule.mem_span_insert {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {y : M} : x ∈ Submodule.span R (insert y s) ↔ ∃ (a : R), ∃ z ∈ Submodule.span R s, x = a • y + z

theorem Submodule.mem_span_pair {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {y : M} {z : M} : z ∈ Submodule.span R {x, y} ↔ ∃ (a : R) (b : R), a • x + b • y = z

theorem Submodule.span_le_restrictScalars (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] : Submodule.span R s ≤ Submodule.restrictScalars 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] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] : ↑(Submodule.span R s) ⊆ ↑(Submodule.span S s)

A version of Submodule.span_le_restrictScalars with coercions.

theorem Submodule.span_span_of_tower (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower 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.

theorem Submodule.span_eq_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R s = ⊥ ↔ ∀ x ∈ s, x = 0

@[simp]

theorem Submodule.span_singleton_eq_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] : Submodule.span R 0 = ⊥

@[simp]

theorem Submodule.span_singleton_le_iff_mem {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) (p : Submodule R M) : Submodule.span R {m} ≤ p ↔ m ∈ p

theorem Submodule.span_singleton_eq_span_singleton {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} {y : M} : Submodule.span R {x} = Submodule.span R {y} ↔ ∃ (z : Rˣ), z • x = y

theorem Submodule.span_image {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} [RingHomSurjective σ₁₂] (f : F) : Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)

@[simp]

theorem Submodule.span_image' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {s : Set M} [RingHomSurjective σ₁₂] (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] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M} (h : x ∈ Submodule.span R s) : f x ∈ Submodule.span R₂ (⇑f '' s)

theorem Submodule.apply_mem_span_image_iff_mem_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {x : M} {s : Set M} (hf : Function.Injective ⇑f) : f x ∈ Submodule.span R₂ (⇑f '' s) ↔ x ∈ Submodule.span R s

@[simp]

theorem Submodule.map_subtype_span_singleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (x : ↥p) : Submodule.map (Submodule.subtype p) (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] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) {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.iSup_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Set M) : ⨆ (i : ι), Submodule.span R (p i) = Submodule.span R (⋃ (i : ι), p i)

theorem Submodule.iSup_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) : ⨆ (i : ι), p i = Submodule.span R (⋃ (i : ι), ↑(p i))

theorem Submodule.iSup_toAddSubmonoid {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) : (⨆ (i : ι), p i).toAddSubmonoid = ⨆ (i : ι), (p i).toAddSubmonoid

theorem Submodule.iSup_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), p i) (hp : ∀ (i : ι), ∀ 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.iSup_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) {C : (x : M) → x ∈ ⨆ (i : ι), p i → Prop} (mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯) (zero : C 0 ⋯) (add : ∀ (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.iSup_induction.

theorem Submodule.singleton_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : CompleteLattice.IsCompactElement (Submodule.span R {x})

theorem Submodule.finset_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Finset M) : CompleteLattice.IsCompactElement (Submodule.span R ↑S)

The span of a finite subset is compact in the lattice of submodules.

theorem Submodule.finite_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Set M) (h : Set.Finite S) : CompleteLattice.IsCompactElement (Submodule.span R S)

The span of a finite subset is compact in the lattice of submodules.

instance Submodule.instIsCompactlyGeneratedSubmoduleCompleteLattice {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : IsCompactlyGenerated (Submodule R M)

Equations

• ⋯ = ⋯

theorem Submodule.submodule_eq_sSup_le_nonzero_spans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : p = sSup {T : Submodule R M | ∃ m ∈ p, 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] [AddCommMonoid M] [Module R M] {I : Submodule R M} {a : M} : I < I ⊔ Submodule.span R {a} ↔ a ∉ I

theorem Submodule.mem_iSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ι → Submodule R M) {m : M} : m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem Submodule.mem_sSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Submodule R M)} {m : M} : m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

theorem Submodule.mem_span_finite_of_mem_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set M} {x : M} (hx : x ∈ Submodule.span R S) : ∃ (T : Finset M), ↑T ⊆ S ∧ x ∈ Submodule.span R ↑T

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] [AddCommMonoid M] [Module R M] (p : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') : Submodule R (M × M')

The product of two submodules is a submodule.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Submodule.prod_coe {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') : ↑(Submodule.prod p q₁) = ↑p ×ˢ ↑q₁

@[simp]

theorem Submodule.mem_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {p : Submodule R M} {q : Submodule R M'} {x : M × M'} : x ∈ Submodule.prod p q ↔ x.1 ∈ p ∧ x.2 ∈ q

theorem Submodule.span_prod_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (s : Set M) (t : Set M') : Submodule.span R (s ×ˢ t) ≤ Submodule.prod (Submodule.span R s) (Submodule.span R t)

@[simp]

theorem Submodule.prod_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] : Submodule.prod ⊤ ⊤ = ⊤

@[simp]

theorem Submodule.prod_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] : Submodule.prod ⊥ ⊥ = ⊥

theorem Submodule.prod_mono {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {p : Submodule R M} {p' : Submodule R M} {q : Submodule R M'} {q' : Submodule R M'} : p ≤ p' → q ≤ q' → Submodule.prod p q ≤ Submodule.prod p' q'

@[simp]

theorem Submodule.prod_inf_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') (q₁' : Submodule R M') : Submodule.prod p q₁ ⊓ Submodule.prod p' q₁' = Submodule.prod (p ⊓ p') (q₁ ⊓ q₁')

@[simp]

theorem Submodule.prod_sup_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') (q₁' : Submodule R M') : Submodule.prod p q₁ ⊔ Submodule.prod p' q₁' = Submodule.prod (p ⊔ p') (q₁ ⊔ q₁')

@[simp]

theorem Submodule.span_neg {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup 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] [AddCommGroup M] [Module R M] {x : M} {y : M} {s : Set M} : x ∈ Submodule.span R (insert y s) ↔ ∃ (a : R), x + a • y ∈ Submodule.span R s

instance Submodule.instIsModularLatticeSubmoduleToSemiringToAddCommMonoidToLatticeToConditionallyCompleteLatticeCompleteLattice {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] : IsModularLattice (Submodule R M)

Equations

• ⋯ = ⋯

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₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (p : Submodule R M) : Submodule.comap f (Submodule.map f p) = p ⊔ LinearMap.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₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) : Submodule.comap f (Submodule.map f p) = p

theorem LinearMap.range_domRestrict_eq_range_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : LinearMap.range (LinearMap.domRestrict f S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤

@[simp]

theorem LinearMap.surjective_domRestrict_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(LinearMap.domRestrict f S) ↔ S ⊔ LinearMap.ker f = ⊤

@[simp]

theorem Submodule.biSup_comap_subtype_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommGroup M] [Module R M] {ι : Type u_9} (s : Set ι) (p : ι → Submodule R M) : ⨆ i ∈ s, Submodule.comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i) = ⊤

theorem Submodule.biSup_comap_eq_top_of_surjective {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {ι : Type u_9} (s : Set ι) (hs : Set.Nonempty s) (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤) (f : M →ₛₗ[τ₁₂] M₂) (hf : Function.Surjective ⇑f) : ⨆ i ∈ s, Submodule.comap f (p i) = ⊤

theorem Submodule.biSup_comap_eq_top_of_range_eq_biSup {M : Type u_4} {M₂ : Type u_5} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_9} {R₂ : Type u_10} [Ring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] [Module R M] [Module R₂ M₂] {ι : Type u_11} (s : Set ι) (hs : Set.Nonempty s) (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) : ⨆ i ∈ s, Submodule.comap f (p i) = ⊤

theorem Submodule.wcovBy_span_singleton_sup {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) (p : Submodule K V) : p ⩿ Submodule.span K {x} ⊔ p

There is no vector subspace between p and (K ∙ x) ⊔ p, WCovBy version.

theorem Submodule.covBy_span_singleton_sup {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {x : V} {p : Submodule K V} (h : x ∉ p) : p ⋖ Submodule.span K {x} ⊔ p

There is no vector subspace between p and (K ∙ x) ⊔ p, CovBy version.

theorem LinearMap.map_le_map_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) {p : Submodule R M} {p' : Submodule R M} : Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' ⊔ LinearMap.ker f

theorem LinearMap.map_le_map_iff' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.ker f = ⊥) {p : Submodule R M} {p' : Submodule R M} : Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p'

theorem LinearMap.map_injective {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.ker f = ⊥) : Function.Injective (Submodule.map f)

theorem LinearMap.map_eq_top_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.range f = ⊤) {p : Submodule R M} : Submodule.map f p = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤

@[simp]

theorem LinearMap.toSpanSingleton_apply (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (b : R) : (LinearMap.toSpanSingleton R M x) b = b • x

def LinearMap.toSpanSingleton (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : R →ₗ[R] M

Given an element x of a module M over R, the natural map from R to scalar multiples of x. See also LinearMap.ringLmapEquivSelf.

Equations

• LinearMap.toSpanSingleton R M x = LinearMap.smulRight LinearMap.id x

theorem LinearMap.span_singleton_eq_range (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : Submodule.span R {x} = LinearMap.range (LinearMap.toSpanSingleton R M x)

The range of toSpanSingleton x is the span of x.

theorem LinearMap.toSpanSingleton_one (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : (LinearMap.toSpanSingleton R M x) 1 = x

@[simp]

theorem LinearMap.toSpanSingleton_zero (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : LinearMap.toSpanSingleton R M 0 = 0

theorem LinearMap.toSpanSingleton_isIdempotentElem_iff {R : Type u_1} [Semiring R] {e : R} : IsIdempotentElem (LinearMap.toSpanSingleton R R e) ↔ IsIdempotentElem e

theorem LinearMap.isIdempotentElem_apply_one_iff {R : Type u_1} [Semiring R] {f : Module.End R R} : IsIdempotentElem (f 1) ↔ IsIdempotentElem f

theorem LinearMap.eqOn_span_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f : F} {g : F} : Set.EqOn ⇑f ⇑g ↑(Submodule.span R s) ↔ Set.EqOn (⇑f) (⇑g) s

Two linear maps are equal on Submodule.span s iff they are equal on s.

theorem LinearMap.eqOn_span' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f : F} {g : F} (H : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑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.EqOn, and the hidden argument will expand to h : x ∈ (span R s : Set M). See LinearMap.eqOn_span for a version that takes h : x ∈ span R s as an argument.

theorem LinearMap.eqOn_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f : F} {g : F} (H : Set.EqOn (⇑f) (⇑g) s) ⦃x : M⦄ (h : x ∈ Submodule.span R s) : f x = g x

If two linear maps are equal on a set s, then they are equal on Submodule.span s.

See also LinearMap.eqOn_span' for a version using Set.EqOn.

theorem LinearMap.ext_on {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f : F} {g : F} (hv : Submodule.span R s = ⊤) (h : Set.EqOn (⇑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 LinearMap.ext_on_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {ι : Type u_9} {v : ι → M} {f : F} {g : F} (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 LinearMap.ker_toSpanSingleton (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (h : x ≠ 0) : LinearMap.ker (LinearMap.toSpanSingleton R M x) = ⊥

theorem LinearMap.span_singleton_sup_ker_eq_top {K : Type u_3} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) : Submodule.span K {x} ⊔ LinearMap.ker f = ⊤

noncomputable def LinearEquiv.toSpanNonzeroSingleton (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.toSpanNonzeroSingleton_apply (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x ≠ 0) (t : R) : (LinearEquiv.toSpanNonzeroSingleton R M x h) t = { val := t • x, property := ⋯ }

theorem LinearEquiv.toSpanNonzeroSingleton_one (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x ≠ 0) : (LinearEquiv.toSpanNonzeroSingleton R M x h) 1 = { val := x, property := ⋯ }

@[inline, reducible]

noncomputable abbrev LinearEquiv.coord (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors 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$.

Equations

• LinearEquiv.coord R M x h = LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton R M x h)

theorem LinearEquiv.coord_self (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x ≠ 0) : (LinearEquiv.coord R M x h) { val := x, property := ⋯ } = 1

theorem LinearEquiv.coord_apply_smul (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x ≠ 0) (y : ↥(Submodule.span R {x})) : (LinearEquiv.coord R M x h) y • x = ↑y