Basic results on bases

The main goal of this file is to show the equivalence between bases and families of vectors that are linearly independent and whose span is the whole space.

There are also various lemmas on bases on specific spaces (such as empty or singletons).

Main results

• Basis.linearIndependent: the basis vectors are linear independent.
• Basis.span_eq: the basis vectors span the whole space.
• Basis.mk: construct a basis out of v : ι → M such that LinearIndependent v and span (range v) = ⊤.

theorem Module.Basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : LinearMap.range ↑b.repr = Finsupp.supported R R Set.univ

theorem Module.Basis.mem_span_repr_support {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (m : M) : m ∈ Submodule.span R (⇑b '' ↑(b.repr m).support)

theorem Module.Basis.repr_support_subset_of_mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (s : Set ι) {m : M} (hm : m ∈ Submodule.span R (⇑b '' s)) : ↑(b.repr m).support ⊆ s

theorem Module.Basis.mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {m : M} {s : Set ι} : m ∈ Submodule.span R (⇑b '' s) ↔ ↑(b.repr m).support ⊆ s

@[simp]

theorem Module.Basis.self_mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] {i : ι} {s : Set ι} : b i ∈ Submodule.span R (⇑b '' s) ↔ i ∈ s

theorem Module.Basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) : x ∈ Submodule.span R (Set.range ⇑b)

@[simp]

theorem Module.Basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Submodule.span R (Set.range ⇑b) = ⊤

theorem Submodule.eq_top_iff_forall_basis_mem {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) {p : Submodule R M} : p = ⊤ ↔ ∀ (i : ι), b i ∈ p

theorem Module.Basis.index_nonempty {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial M] : Nonempty ι

theorem Module.Basis.linearIndependent {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : LinearIndependent R ⇑b

theorem Module.Basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] (i : ι) : b i ≠ 0

noncomputable def Module.Basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) : Basis ι R M

A linear independent family of vectors spanning the whole module is a basis.

@[simp]

theorem Module.Basis.mk_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {x : M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) : (Basis.mk hli hsp).repr x = hli.repr ⟨x, ⋯⟩

theorem Module.Basis.mk_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) (i : ι) : (Basis.mk hli hsp) i = v i

@[simp]

theorem Module.Basis.coe_mk {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) : ⇑(Basis.mk hli hsp) = v

theorem Module.Basis.mk_coord_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} (i : ι) : ((Basis.mk hli hsp).coord i) (v i) = 1

Given a basis, the ith element of the dual basis evaluates to 1 on the ith element of the basis.

theorem Module.Basis.mk_coord_apply_ne {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} {i j : ι} (h : j ≠ i) : ((Basis.mk hli hsp).coord i) (v j) = 0

Given a basis, the ith element of the dual basis evaluates to 0 on the jth element of the basis if j ≠ i.

theorem Module.Basis.mk_coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} [DecidableEq ι] {i j : ι} : ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Given a basis, the ith element of the dual basis evaluates to the Kronecker delta on the jth element of the basis.

noncomputable def Module.Basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hli : LinearIndependent R v) : Basis ι R ↥(Submodule.span R (Set.range v))

A linear independent family of vectors is a basis for their span.

theorem Module.Basis.span_apply {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hli : LinearIndependent R v) (i : ι) : ↑((Basis.span hli) i) = v i

theorem Module.Basis.maximal {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (b : Basis ι R M) : ⋯.Maximal

Any basis is a maximal linear independent set.

instance Module.Basis.uniqueBasis {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] : Unique (Basis ι R M)

def Module.Basis.singleton (ι : Type u_7) (R : Type u_8) [Unique ι] [Semiring R] : Basis ι R R

Basis.singleton ι R is the basis sending the unique element of ι to 1 : R.

@[simp]

theorem Module.Basis.singleton_apply (ι : Type u_7) (R : Type u_8) [Unique ι] [Semiring R] (i : ι) : (Basis.singleton ι R) i = 1

@[simp]

theorem Module.Basis.singleton_repr (ι : Type u_7) (R : Type u_8) [Unique ι] [Semiring R] (x : R) (i : ι) : ((Basis.singleton ι R).repr x) i = x

def Module.Basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] [IsEmpty ι] : Basis ι R M

If M is a subsingleton and ι is empty, this is the unique ι-indexed basis for M.

instance Module.Basis.emptyUnique {ι : Type u_1} {R : Type u_3} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] [IsEmpty ι] : Unique (Basis ι R M)

theorem Module.Basis.noZeroSMulDivisors {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) : NoZeroSMulDivisors R M

theorem Module.Basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

theorem Module.Basis.basis_singleton_iff {R : Type u_7} {M : Type u_8} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (ι : Type u_9) [Unique ι] : Nonempty (Basis ι R M) ↔ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y