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.

source

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 | s ⊆ ↑p}

Instances For

source

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

source

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)

source

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

source

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

source

theorem Submodule.span_monotone {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Monotone (Submodule.span R)

source

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

source

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

source

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

source

@[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.

source

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} [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) :

Submodule.map f (Submodule.span R s) = Submodule.span R₂ (↑f '' s)

source

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} [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.

source

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} [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :

Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ (m : M), m ∈ s → ↑f m ∈ N

source

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} [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (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.

source

@[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

source

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} [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M₂) :

Submodule.span R (↑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)

source

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} [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.

source

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)

source

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

source

@[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

source

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) (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.

source

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) (Hs : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → p x y) (H0_left : ∀ (y : M), p 0 y) (H0_right : ∀ (x : M), p x 0) (Hadd_left : ∀ (x₁ x₂ y : M), p x₁ y → p x₂ y → p (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : M), p x y₁ → p x y₂ → p x (y₁ + y₂)) (Hsmul_left : ∀ (r : R) (x y : M), p x y → p (r • x) y) (Hsmul_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.

source

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} (Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(Submodule.span R s))) (H0 : p 0 (_ : 0 ∈ Submodule.span R s)) (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) (_ : x + y ∈ Submodule.span R s)) (H2 : ∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) (_ : a • x ∈ Submodule.span R s)) {x : M} (hx : x ∈ Submodule.span R s) :

p x hx

A dependent version of Submodule.span_induction.

source

@[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) = ⊤

source

theorem Submodule.span_nat_eq_addSubmonoid_closure {M : Type u_4} [AddCommMonoid M] (s : Set M) :

(Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

source

@[simp]

theorem Submodule.span_nat_eq {M : Type u_4} [AddCommMonoid M] (s : AddSubmonoid M) :

(Submodule.span ℕ ↑s).toAddSubmonoid = s

source

theorem Submodule.span_int_eq_addSubgroup_closure {M : Type u_9} [AddCommGroup M] (s : Set M) :

Submodule.toAddSubgroup (Submodule.span ℤ s) = AddSubgroup.closure s

source

@[simp]

theorem Submodule.span_int_eq {M : Type u_9} [AddCommGroup M] (s : AddSubgroup M) :

Submodule.toAddSubgroup (Submodule.span ℤ ↑s) = s

source

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

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

Instances For

source

@[simp]

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

Submodule.span R ∅ = ⊥

source

@[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 = ⊤

source

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

source

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)

source

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, s i j) = ⨆ i, ⨆ j, Submodule.span R (s i j)

source

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, Submodule.span R ↑(f x)

source

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)

source

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)

source

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))

Instances For

source

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}

source

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}

source

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

source

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)

source

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.

source

@[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} [hι : Nonempty ι] (S : ι → Submodule R M) (H : Directed (fun x x_1 => x ≤ x_1) S) :

↑(iSup S) = ⋃ i, ↑(S i)

source

@[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 => x ≤ x_1) S) {x : M} :

x ∈ iSup S ↔ ∃ i, x ∈ S i

source

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 => x ≤ x_1) s) :

z ∈ sSup s ↔ ∃ y, y ∈ s ∧ z ∈ y

source

@[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)

source

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.

source

@[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

source

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, y ∈ p ∧ ∃ z, z ∈ p' ∧ y + z = x

source

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 z, ↑y + ↑z = x

source

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, y ∈ p ∧ ∃ z, z ∈ p' ∧ y + z = x

source

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'

source

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

source

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'

source

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}

source

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 { x_1 // x_1 ∈ Submodule.span R {x} }

source

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, a • y = x

source

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 : M), v ∈ s → ∃ r, r • v₀ = v

source

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 • x = v

source

@[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} = ⊥

source

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 => x • y

source

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}

source

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}

source

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}

source

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

source

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

source

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}

source

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

source

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

source

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

source

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 z, z ∈ Submodule.span R s ∧ x = a • y + z

source

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 b, a • x + b • y = z

source

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.

source

@[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.

source

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.

source

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 : M), x ∈ s → x = 0

source

@[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

source

@[simp]

theorem Submodule.span_zero {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :

Submodule.span R 0 = ⊥

source

@[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

source

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, z • x = y

source

@[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₂] {F : Type u_8} [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} [RingHomSurjective σ₁₂] (f : F) :

Submodule.span R₂ (↑f '' s) = Submodule.map f (Submodule.span R s)

source

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} [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)

source

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} [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

source

@[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 : { x // x ∈ p }) :

Submodule.map (Submodule.subtype p) (Submodule.span R {x}) = Submodule.span R {↑x}

source

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} [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.

source

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)

source

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))

source

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

source

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 : 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.

source

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} (hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ i, p i)) (h0 : C 0 (_ : 0 ∈ ⨆ i, p i)) (hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ i, p i)) {x : M} (hx : x ∈ ⨆ i, p i) :

C x hx

A dependent version of submodule.iSup_induction.

source

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})

source

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.

source

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.

source

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

IsCompactlyGenerated (Submodule R M)

Equations

@Submodule.instIsCompactlyGeneratedSubmoduleCompleteLattice = @Submodule.instIsCompactlyGeneratedSubmoduleCompleteLattice.proof_1

source

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 | ∃ m x x, T = Submodule.span R {m}}

A submodule is equal to the supremum of the spans of the submodule's nonzero elements.

source

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

source

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

source

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 : Submodule R M), p ∈ s → p ≤ N) → m ∈ N

source

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, ↑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.

source

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.

Instances For

source

@[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₁

source

@[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

source

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)

source

@[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 ⊤ ⊤ = ⊤

source

@[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 ⊥ ⊥ = ⊥

source

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'

source

@[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₁')

source

@[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₁')

source

@[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

source

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, x + a • y ∈ Submodule.span R s

source

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

IsModularLattice (Submodule R M)

Equations

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

source

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} [sc : SemilinearMapClass F τ₁₂ M M₂] (f : F) (p : Submodule R M) :

Submodule.comap f (Submodule.map f p) = p ⊔ LinearMap.ker f

source

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} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) :

Submodule.comap f (Submodule.map f p) = p

source

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 = ⊤

source

@[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 = ⊤

source

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.

source

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.

source

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} [sc : 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

source

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} [sc : 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'

source

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} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.ker f = ⊥) :

Function.Injective (Submodule.map f)

source

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} [sc : SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.range f = ⊤) {p : Submodule R M} :

Submodule.map f p = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤

source

@[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

source

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.

Equations

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

Instances For

source

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.

source

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

source

@[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

source

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₂} [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.

source

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₂} [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.

source

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₂} [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.

source

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₂} [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.

source

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₂} [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.

source

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) = ⊥

source

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 = ⊤

source

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] { x_1 // x_1 ∈ 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.

Instances For

source

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 := (_ : x ∈ Submodule.span R {x}) }

source

@[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) :

{ x_1 // x_1 ∈ 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)

Instances For

source

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 := (_ : x ∈ Submodule.span R {x}) } = 1

source

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 : { x_1 // x_1 ∈ Submodule.span R {x} }) :

↑(LinearEquiv.coord R M x h) y • x = ↑y