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 is independent when forces every , and a subset is independent when every injective finite list into 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 , 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 as the smallest linear subspace containing
is exactly the set of linear combinations of finite lists of elements of , and
Linear subspace of a vector space
The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity
Vector space over a field
Field
The natural numbers (von Neumann)
On the order is membership:
Injection, surjection, bijection