Alphabeta MathHow 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.
Every vector space has a basis
Statement
Assume the Axiom of Choice, through Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if with independent and , there is a basis of with . Then every vector space over a field (Vector space over a field) has a basis (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
In particular the zero space has a basis, namely .
Facts & Assumptions
Given: A field and a vector space over .
if and only if is a linear subspace of , and is a linear subspace of itself (The span is monotone and idempotent, exactly when is a linear subspace, and , claim 4, Linear subspace of a vector space, Linear combination of a finite list, and the span as the smallest linear subspace containing ).
If with linearly independent and , there is a basis of with (Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if with independent and , there is a basis of with ).
Proof
is a linear subspace of itself, so : the whole space satisfies the three closure conditions trivially, and the span of a linear subspace is that subspace.
The empty set is linearly independent and .
By steps 1.1 and 1.2 the extension theorem applies with and , and yields a basis of with ; so has a basis. When the basis produced is , the only linearly independent subset of that space.
Remarks
-
The converse is a theorem of Blass, and it is not proved here. The implication proved above runs from the Axiom of Choice, through Zorn's lemma, to the existence of bases. The opposite implication also holds: the statement that every vector space over every field has a basis implies the Axiom of Choice. That is a hard result of Andreas Blass, published in 1984 as "Existence of bases implies the axiom of choice"; this library does not prove it, does not use it, and nothing here rests on it. It is recorded because it fixes the exact strength of the statement above: existence of bases is not merely a consequence of choice, it is equivalent to it over ZF. The reference is listed in the sources of this item.
-
Where the choice is spent. In Zorn's lemma, once, and nowhere else on this page. Every other existence statement here is explicit: the standard basis of (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ) is written down, and so is the infinite basis of the eventually zero families on the companion page. The contrast between those and the present corollary — which produces a basis of over while exhibiting none, as the companion page records — is the point of keeping them on the same page.
-
This says nothing about the size of the basis. For a space with no finite basis, Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis assigns no dimension at all, and the corollary correspondingly asserts only existence.
Depends on
- Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L \subseteq S \subseteq V$ with $L$ independent and $\operatorname{span}(S) = V$, there is a basis $B$ of $V$ with $L \subseteq B \subseteq S$
- Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
- 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
- Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$
- The span is monotone and idempotent, $\operatorname{span}(S) = S$ exactly when $S$ is a linear subspace, and $\operatorname{span}(S \cup \{0_V\}) = \operatorname{span}(S)$
- Linear subspace of a vector space
- Vector space over a field
- Field
- The Axiom of Choice
Used by
- Every linear subspace U of a vector space V has a complement: a linear subspace W with V = U ⊕ W Corollary
- Field Kunneth isomorphism for homology of products Corollary
- A module is relatively H-projective when it is a direct summand of one induced from H Definition
- ℝ as a vector space over ℚ has a basis, and every such basis is infinite; the existence proof exhibits none Example
- The one-dimensional vertex operator algebra is rational assuming Choice Example
- Weak and global dimension for a field and the integers Example
- An augmented coideal ideal of an enveloping algebra is generated by its primitive part Lemma
- 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
- Double bar comparison for cyclic bimodule tensor products Lemma
- External evaluation detects tensor-square operations Lemma
- Finite cell local system cohomology is finite and commutes with field extension Lemma
- Finite-type field extensions with zero Ω Lemma
- Lie algebras of subspace stabilizers and Lie-stable subspaces Lemma
- Linearity and conjugation invariance of the finite potent trace Lemma
- Representations of diagonalizable groups split into character eigenspaces Lemma
- Tensor products of primitive vectors Lemma
- The trace of a finite potent endomorphism exists and is unique Lemma
- Chevalley–Eilenberg cohomology computes Ext of the trivial module Proposition
- Compact Lie groups admit bi-invariant metrics Proposition
- Integrable weight sets and multiplicities are weyl invariant Proposition
- Modules over a field are projective, flat, and injective Proposition
- The proved choice ledger: hypotheses, equivalences, and upper bounds Remark
- A connected graded module coalgebra with injective unit orbit is free Theorem
- A transgressive simple fiber system gives a polynomial base Theorem
- Assuming choice, J_V:V→ V^** is surjective if and only if V is finite-dimensional Theorem
- Derived cyclicity of Hochschild hyperhomology Theorem
- Finite-dimensional compact-group representations are unitarizable Theorem
- Functoriality and coefficient long exact sequences for Hochschild homology Theorem
- Point blowups of regular surfaces stay regular, with rational exceptional fibre over the residue field Theorem
- The admissible square algebra is a connected bialgebra Theorem
- The two-sided bar complex is a projective Aᵉ-resolution Theorem
- Universal property of the free Lie algebra Theorem
Dependency tree · two levels
33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Basis (linear algebra) (Wikipedia) — where A. Blass, Existence of bases implies the axiom of choice, Contemporary Mathematics 31 (1984), 31-33, is recorded (standard reference, not scraped)
- Axiom of choice (Wikipedia) (standard reference, not scraped)
- Cambridge University Press excerpt: Vector spaces and bases (standard reference, not scraped)