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 \span, 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) : S.IsPrincipal ↔ ∃ (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}

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

theorem Submodule.IsPrincipal.principal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) [S.IsPrincipal] : ∃ (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

theorem Submodule.coe_span_eq_self {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) : ↑(Submodule.span R ↑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.

@[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] {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 y : M) (hx : x ∈ Submodule.span R s) (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

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.

@[deprecated Submodule.span_induction]

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 y : M) (hx : x ∈ Submodule.span R s) (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

Alias of Submodule.span_induction.

---

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 : (x y : M) → x ∈ Submodule.span R s → y ∈ Submodule.span R s → Prop} (mem_mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (y : M) (hy : y ∈ Submodule.span R s), p 0 y ⋯ hy) (zero_right : ∀ (x : M) (hx : x ∈ Submodule.span R s), p x 0 hx ⋯) (add_left : ∀ (x y z : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s) (hz : z ∈ Submodule.span R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s) (hz : z ∈ Submodule.span R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (smul_left : ∀ (r : R) (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x y hx hy → p (r • x) y ⋯ hy) (smul_right : ∀ (r : R) (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x y hx hy → p x (r • y) hx ⋯) {a : M} {b : M} (ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R s) : 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_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] {s : Set M} {p : (x : M) → x ∈ Submodule.span R s → Prop} (zero : p 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ Submodule.span R s) (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 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.

@[deprecated Submodule.closure_induction]

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 y : M) (hx : x ∈ Submodule.span R s) (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

Alias of Submodule.closure_induction.

---

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_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.span ℤ s).toAddSubgroup = AddSubgroup.closure s

@[simp]

theorem Submodule.span_int_eq {M : Type u_9} [AddCommGroup M] (s : AddSubgroup M) : (Submodule.span ℤ ↑s).toAddSubgroup = 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 ↑(s.attach.biUnion 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] {ι : Sort 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 (x1 x2 : Submodule R M) => x1 ≤ x2) 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 (x1 x2 : Submodule R M) => x1 ≤ x2) 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 : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Submodule R M) => x1 ≤ x2) 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.ωScottContinuous 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) : (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

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 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] [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 : S.Finite) : CompleteLattice.IsCompactElement (Submodule.span R S)

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

instance Submodule.instIsCompactlyGenerated {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

• p.prod q₁ = { carrier := ↑p ×ˢ ↑q₁, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[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') : ↑(p.prod 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 ∈ p.prod 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.span R s).prod (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'] : ⊤.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'] : ⊥.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' → p.prod q ≤ p'.prod 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') : p.prod q₁ ⊓ p'.prod q₁' = (p ⊓ p').prod (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') : p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (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.instIsModularLattice {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] : IsModularLattice (Submodule R M)

Equations

• ⋯ = ⋯

theorem Submodule.isCompl_comap_subtype_of_isCompl_of_le {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} {q : Submodule R M} {r : Submodule R M} (h₁ : IsCompl q r) (h₂ : q ≤ p) : IsCompl (Submodule.comap p.subtype q) (Submodule.comap p.subtype r)

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 (f.domRestrict 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 ⇑(f.domRestrict 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 (⨆ i ∈ s, p i).subtype (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 : s.Nonempty) (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 : s.Nonempty) (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.id.smulRight 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₂] {ι : Sort 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 = ⟨t • x, ⋯⟩

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 = ⟨x, ⋯⟩

@[reducible, inline]

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.toSpanNonzeroSingleton R M x h).symm

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) ⟨x, ⋯⟩ = 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