How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
Definition
Let be a vector space over a field (Vector space over a field).
A subset is a basis of when
- (B1) is linearly independent (Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent), and
- (B2) spans , that is (Linear combination of a finite list, and the span as the smallest linear subspace containing , which is where the words spans and spanning set are fixed; they are not redefined here).
The empty set is a basis of the zero space, and of nothing else. is linearly independent (Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent) and ( is exactly the set of linear combinations of finite lists of elements of , and ), so is a basis of exactly when . This is the case from which every induction on this page starts, and it is a genuine case rather than a convention.
Ordered bases
An ordered basis of is a finite list , with and the von Neumann natural (The natural numbers (von Neumann), On the order is membership: ), such that is injective (Injection, surjection, bijection) and its image is a basis of .
By claim 6 of Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never , its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent, a list is linearly independent exactly when it is injective with linearly independent image, so an ordered basis is equally described as a linearly independent list with : the injectivity does not have to be imposed separately. The empty list is the ordered basis of the zero space.
An ordered basis is a list, so it carries an order; a basis is a set, so it does not. Reordering an ordered basis gives a different ordered basis with the same image, and the coordinates of A finite list is an ordered basis if and only if every equals for exactly one ; those scalars are the coordinates of in that ordered basis are attached to the list, not to the set.
Bases of a linear subspace
Let be a linear subspace of (Linear subspace of a vector space), which is itself a vector space over , with the addition, the zero vector and the scalar multiplication of restricted to . For the two readings of " is a basis" — computed inside , or computed inside — agree, so the phrase needs no disambiguation below.
- Independence agrees. The finite sums of a list are given by the same recursion in as in (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity), the base value and the operation being literally those of (Linear subspace of a vector space). So a list into has the same sums whichever space it is read in, and the vanishing condition of Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent is the same condition in both.
- The span agrees. A subset of is a linear subspace of exactly when it is a linear subspace of , conditions (W1), (W2), (W3) being the same conditions in either reading. Now , since is a linear subspace of containing and the span is contained in every such subspace; so is a linear subspace of containing , whence . Conversely is a linear subspace of containing , whence . The two are therefore equal, and we write for both.
Consequently is a basis of the vector space if and only if is linearly independent as a subset of and .
Remarks
-
The name is
def-linear-basis, and the bare word is not used here. The library already has a basis — a basis for a topology, defined in Basis and subbasis for a topology, and the topology generated by a family of sets ↗ and namespaced there with the aliasdef-basis-top. The two notions share the word and nothing else: one is a family of open sets closed under a refinement condition, the other an independent spanning subset of a vector space. This page therefore follows the convention of Linear subspace of a vector space, where the same collision with the topological subspace was resolved the same way, and says linear in the id. In prose, where the ambient vector space is named, "basis" alone is used. -
Nothing above asserts that a basis exists. Existence for an arbitrary vector space is Every vector space has a basis, and it is proved from Zorn's lemma; existence for the concrete spaces is The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension and needs no choice principle at all. The definition is stated first so that both statements have something to be about.
-
A basis need not be finite, and this definition does not assume it is. Condition (B1) quantifies over finite lists drawn from and (B2) is an equality of sets, so both make sense for an arbitrary . It is only Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis that restricts attention to spaces admitting a finite basis, and the companion page exhibits an explicit infinite basis, for the eventually zero families in .
Depends on
- Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i<n} \lambda_i v_i = 0_V$ forces every $\lambda_i = 0_F$, and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent
- Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never $0_V$, its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent
- Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$
- $\operatorname{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$, and $\operatorname{span}(\varnothing) = \{0_V\}$
- Linear subspace of a vector space
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- Vector space over a field
- Field
- The natural numbers $\mathbb{N}$ (von Neumann)
- On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$
- Injection, surjection, bijection
Used by
- Every linear subspace U of a vector space V has a complement: a linear subspace W with V = U ⊕ W Corollary
- Every spanning subset of a vector space contains a basis Corollary
- Every vector space has a basis Corollary
- If V = bigoplus_i<n Uᵢ with every Uᵢ finite-dimensional, then V is finite-dimensional and dim_F V = ∑_i<n dim_F Uᵢ; in particular dim_F(U ⊕ W) = dim_F U + dim_F W Corollary
- {(1,0), (0,1), (1,1)} spans F² and is linearly dependent, so a spanning set need not be a basis; each of its three two-element subsets is a basis Counterexample
- Inside the space of eventually zero families, the linear subspace spanned by { eᵢ : i ≥ 1 } is proper and has a basis equinumerous with a basis of the whole space, so "equal dimension forces equality" fails without finite dimension Counterexample
- The standard unit families { eᵢ : i ∈ ℕ } are linearly independent in F^ℕ but do not span it: the constant family 1_F is not a finite linear combination of them Counterexample
- Three distinct lines U₀, U₁, U₂ in F² have dim_F(U₀+U₁+U₂) = 2 while the inclusion-exclusion analogue of the dimension formula predicts 3, so the two-subspace formula does not extend Counterexample
- Coordinate columns [v]_mathcal B and matrices [T]_mathcal B^mathcal C of linear maps relative to ordered bases Definition
- Finite-dimensional vector space, and its dimension dim_F V; infinite-dimensional means having no finite basis Definition
- Row space, column space, nullspace, row rank, column rank and matrix rank Definition
- ℝ as a vector space over ℚ has a basis, and every such basis is infinite; the existence proof exhibits none Example
- The standard unit families eₖ ∈ F^ℕ form a basis of the linear subspace of eventually zero families: an explicit infinite basis, built with no choice principle Example
- The vector (1,2) ∈ ℝ² has coordinate list (1,2) in the standard ordered basis, (2,1) in its reversal, and (2,-1) in the ordered basis ((1,1),(1,0)) Example
- FALSE: all norms on a real vector space are equivalent False statement
- FALSE: the union of two linearly independent subsets of a vector space is linearly independent False statement
- Assuming the Axiom of Choice, ℝ has a Hamel basis over ℚ: there is B ⊆ ℝ such that every real is a finite ℚ-linear combination of elements of B in exactly one way, and each basis vector carries a well-defined ℚ-linear coefficient map Lemma
- Extending a basis of the kernel to a basis of the domain gives a basis of the image Lemma
- For B ⊆ V the following are equivalent: B is a basis; B is a maximal linearly independent subset of V; B is a minimal spanning subset of V — maximality and minimality being in the inclusion order Lemma
- The nonzero rows of a row echelon form form a basis of the original row space Lemma
- The standard list e : n → Fⁿ with eᵢ(i) = 1_F and eᵢ(j) = 0_F for j ≠ i is an ordered basis of Fⁿ; hence dim_F Fⁿ = n, and F⁰ is the zero space with basis ∅ and dimension 0 Lemma
- A finite list v : n → V is an ordered basis if and only if every x ∈ V equals ∑_i<n λᵢ vᵢ for exactly one λ : n → F; those scalars are the coordinates of x in that ordered basis Theorem
- If dim_F V = n and U is a linear subspace of V, then U is finite-dimensional, dim_F U ≤ n, and dim_F U = n if and only if U = V Theorem
- If V has a basis with n elements and a basis with m elements then n = m; and if V has one finite basis then every basis of V is finite Theorem
- Similarity is an equivalence relation, and two matrices represent the same endomorphism in two bases exactly when they are similar Theorem
- The columns of the original matrix indexed by pivot columns form a basis of its column space Theorem
- The dimension formula: for finite-dimensional linear subspaces U and W of V, the subspaces U + W and U ∩ W are finite-dimensional and dim_F(U+W) + dim_F(U ∩ W) = dim_F U + dim_F W Theorem
- Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if L ⊆ S ⊆ V with L independent and span(S) = V, there is a basis B of V with L ⊆ B ⊆ S Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 64 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Basis (linear algebra) (Wikipedia) (standard reference, not scraped)
- S. Axler, Linear Algebra Done Right, 4th ed., Ch. 2 (standard reference, not scraped)
- Cambridge University Press excerpt: Vector spaces and bases (standard reference, not scraped)