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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Basis.singleton_apply (ι : Type u_7) (R : Type u_8) [Unique ι] [Semiring R] (i : ι) : (Basis.singleton ι R) i = 1

@[simp]

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

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