01.01.04 · foundations / linear-algebra

Subspace, basis, dimension

shipped3 tiersLean: partial

Anchor (Master): Halmos — Finite-Dimensional Vector Spaces §I.5–I.8; Hoffman-Kunze §2; Lang Algebra Ch. III §5

Intuition [Beginner]

A subspace is a piece of a vector space that is itself closed under the same operations. Pick any two arrows that live inside it and add them: the sum stays inside. Stretch one arrow by any number: the result stays inside. The piece carries its own self-contained algebra.

In the everyday picture of three-dimensional space, the subspaces are the origin alone, every line through the origin, every plane through the origin, and the whole space. A line that misses the origin is not a subspace because adding two of its arrows lands somewhere off the line.

A basis is a smallest list of arrows that can build every other arrow by combining and scaling. Dimension counts how many arrows the basis needs.

Visual [Beginner]

The blue parallelogram on the left is a plane through the origin sitting inside three-dimensional space. The red and blue arrows span that plane: every point in it is a combination of the two. The right panel shows three arrows that together span the whole surrounding space.

The plane is a 2-dimensional subspace inside the 3-dimensional space. Two arrows are enough to reach every point of the plane. Three arrows are needed to reach every point of the whole space.

Worked example [Beginner]

Work in the coordinate plane. Take the two arrows $(1, 0)$ and $(0, 1)$ .

Combining them with coefficients $3$ and $2$ produces

3 (1, 0) + 2 (0, 1) = (3, 0) + (0, 2) = (3, 2) .

Combining them with coefficients $- 1$ and $4$ produces

- 1 (1, 0) + 4 (0, 1) = (- 1, 0) + (0, 4) = (- 1, 4) .

Every point $(a, b)$ in the plane is reached as $a (1, 0) + b (0, 1)$ . The two arrows reach every point and neither one is a multiple of the other. The list ${(1, 0), (0, 1)}$ is a basis of the coordinate plane, and the dimension of the plane is $2$ .

What this tells us: a basis is a minimum-size kit that builds every other arrow.

Check your understanding [Beginner]

Formal definition [Intermediate+]

Let $V$ be a vector space over a field $K$ .

A subspace of $V$ is a subset $W \subseteq V$ that is non-empty, closed under addition, and closed under scalar multiplication. Equivalently, $W$ is non-empty and contains $a u + b v$ whenever $u, v \in W$ and $a, b \in K$ . A subspace inherits the vector-space structure of $V$ ^{[quantum-well Proof that the sum of subspaces is also a subspace.md]}.

A finite list $v_{1}, \dots, v_{n}$ of vectors in $V$ is linearly independent when

a_{1} v_{1} + \dots + a_{n} v_{n} = 0 ⟹ a_{1} = \dots = a_{n} = 0,

with $a_{1}, \dots, a_{n} \in K$ . The list spans $V$ , written $V = span {v_{1}, \dots, v_{n}}$ , when every vector in $V$ is a linear combination of the listed vectors.

A basis of $V$ is a list of vectors that is both linearly independent and spanning. Equivalent phrasings: a basis is a maximal linearly independent list, or a minimal spanning list. The vector space $V$ is finite-dimensional when it has a finite basis.

The dimension of a finite-dimensional vector space, written $dim V$ , is the number of vectors in any basis. Well-definedness — that every basis has the same number of elements — is the content of the key theorem below ^{[textbooks-extra Calculus Vol.2 - Multi-Variable Calculus and Linear Algebra with Applications (Tom Apostol).pdf]}.

Examples. The coordinate space $K^{n}$ has dimension $n$ with the standard basis $e_{1}, \dots, e_{n}$ where $e_{i}$ has a $1$ in position $i$ and zeroes elsewhere. The space of polynomials of degree at most $n$ has dimension $n + 1$ with basis $1, x, x^{2}, \dots, x^{n}$ . The zero space ${0}$ has dimension $0$ with the empty basis.

Non-examples. The set ${(x, y) \in R^{2} : x \geq 0}$ is closed under addition and under non-negative scalar multiplication but not under multiplication by $- 1$ , so it fails to be a subspace. The set ${(x, y) \in R^{2} : x + y = 1}$ misses the origin and fails closure under addition. The list $(1, 0), (2, 0), (0, 1)$ in $R^{2}$ spans but is not linearly independent because $(2, 0) = 2 (1, 0)$ , so it is not a basis.

Key theorem with proof [Intermediate+]

Theorem (Steinitz replacement). Let $V$ be a vector space over $K$ . Suppose ${v_{1}, \dots, v_{n}}$ spans $V$ and ${w_{1}, \dots, w_{m}}$ is linearly independent. Then $m \leq n$ , and there is a relabelling of the $v_{i}$ so that ${w_{1}, \dots, w_{m}, v_{m + 1}, \dots, v_{n}}$ also spans $V$ ^{[Steinitz, E. — Bedingt konvergente Reihen und konvexe Systeme]}.

Proof. Argue by induction on $m$ .

Base case $m = 1$ . Since ${w_{1}}$ is linearly independent, $w_{1} \neq = 0$ . The spanning hypothesis writes $w_{1} = a_{1} v_{1} + \dots + a_{n} v_{n}$ for scalars $a_{i} \in K$ , and at least one $a_{i}$ is non-zero because $w_{1} \neq = 0$ . Relabel so that $a_{1} \neq = 0$ . Solving for $v_{1}$ gives

v_{1} = a_{1}^{- 1} w_{1} - a_{1}^{- 1} a_{2} v_{2} - \dots - a_{1}^{- 1} a_{n} v_{n} .

Every linear combination of $v_{1}, \dots, v_{n}$ is therefore also a linear combination of $w_{1}, v_{2}, \dots, v_{n}$ . Hence ${w_{1}, v_{2}, \dots, v_{n}}$ spans $V$ , and $1 \leq n$ holds because $V$ contains the non-zero vector $w_{1}$ , so $n \geq 1$ .

Inductive step. Assume the result for $m - 1$ . Apply it to the spanning set ${v_{1}, \dots, v_{n}}$ and the linearly independent set ${w_{1}, \dots, w_{m - 1}}$ . The conclusion gives $m - 1 \leq n$ and a relabelling so that ${w_{1}, \dots, w_{m - 1}, v_{m}, \dots, v_{n}}$ spans $V$ .

Express $w_{m}$ in this spanning set:

w_{m} = b_{1} w_{1} + \dots + b_{m - 1} w_{m - 1} + c_{m} v_{m} + \dots + c_{n} v_{n},

with $b_{j}, c_{k} \in K$ . At least one $c_{k}$ is non-zero. Otherwise $w_{m} = b_{1} w_{1} + \dots + b_{m - 1} w_{m - 1}$ , which rearranges to

b_{1} w_{1} + \dots + b_{m - 1} w_{m - 1} + (- 1) w_{m} = 0.

The coefficient $- 1$ on $w_{m}$ is non-zero, contradicting the linear independence of ${w_{1}, \dots, w_{m}}$ .

Therefore some $c_{k} \neq = 0$ . The list ${v_{m}, \dots, v_{n}}$ is non-empty, so $n \geq m$ . Relabel so that $c_{m} \neq = 0$ . Solving for $v_{m}$ gives

v_{m} = c_{m}^{- 1} w_{m} - c_{m}^{- 1} b_{1} w_{1} - \dots - c_{m}^{- 1} b_{m - 1} w_{m - 1} - c_{m}^{- 1} c_{m + 1} v_{m + 1} - \dots - c_{m}^{- 1} c_{n} v_{n} .

Every linear combination of $w_{1}, \dots, w_{m - 1}, v_{m}, \dots, v_{n}$ is therefore also a linear combination of $w_{1}, \dots, w_{m}, v_{m + 1}, \dots, v_{n}$ . Hence ${w_{1}, \dots, w_{m}, v_{m + 1}, \dots, v_{n}}$ spans $V$ . The induction is complete. $□$

Corollary (well-definedness of dimension). Any two bases of a finite-dimensional vector space have the same number of elements.

Proof. Let $B = {v_{1}, \dots, v_{n}}$ and $B^{'} = {w_{1}, \dots, w_{m}}$ be bases. Apply the replacement theorem with $B$ as the spanning set and $B^{'}$ as the linearly independent set: $m \leq n$ . Apply it again with the roles reversed: $n \leq m$ . Hence $m = n$ . $□$

Bridge. The replacement theorem builds toward rank-nullity, where dimension counts solutions and image vectors against each other inside a single linear map. The dimension function appears again in tensor algebra, where $dim (V \otimes W) = dim V \cdot dim W$ packages the multilinear structure into a single integer. The same dimension count organises differential forms, where the rank of $Λ^{k} V^{*}$ records how many independent $k$ -fold wedge products fit inside an $n$ -dimensional space. The same invariant feeds vector-bundle theory, where the rank of a bundle is the dimension of every fibre. Putting these together, dimension is the foundational invariant of finite-dimensional linear algebra: it classifies finite-dimensional vector spaces over a fixed field up to isomorphism, and it is the integer the rest of the strand reads off whenever a multilinear, exterior, or fibrewise construction is performed.

Exercises [Intermediate+]

Exercise 6 (hard, proof).

Prove the dimension formula

dim (W_{1} + W_{2}) + dim (W_{1} \cap W_{2}) = dim W_{1} + dim W_{2}

for finite-dimensional subspaces $W_{1}, W_{2}$ of a vector space $V$ .

Hint

Start with a basis of $W_{1} \cap W_{2}$ and extend separately to bases of $W_{1}$ and of $W_{2}$ .

Answer

Let ${u_{1}, \dots, u_{k}}$ be a basis of $W_{1} \cap W_{2}$ . Extend to a basis ${u_{1}, \dots, u_{k}, v_{1}, \dots, v_{p}}$ of $W_{1}$ and to a basis ${u_{1}, \dots, u_{k}, w_{1}, \dots, w_{q}}$ of $W_{2}$ . The combined list ${u_{1}, \dots, u_{k}, v_{1}, \dots, v_{p}, w_{1}, \dots, w_{q}}$ spans $W_{1} + W_{2}$ . To see independence, suppose $\sum a_{i} u_{i} + \sum b_{j} v_{j} + \sum c_{l} w_{l} = 0$ . Then $\sum c_{l} w_{l} = - \sum a_{i} u_{i} - \sum b_{j} v_{j}$ lies in $W_{1} \cap W_{2}$ , so each $c_{l} = 0$ by independence of the $w_{l}$ modulo $W_{1} \cap W_{2}$ . The remaining relation reduces to a relation among the basis of $W_{1}$ , forcing all $a_{i} = b_{j} = 0$ . Therefore $dim (W_{1} + W_{2}) = k + p + q$ , while $dim W_{1} + dim W_{2} = (k + p) + (k + q)$ , and $dim (W_{1} \cap W_{2}) = k$ . The identity follows.

Lean formalization [Intermediate+]

Mathlib models a subspace as Submodule K V, a basis as Basis ι K V, and the dimension of a finite-dimensional space as Module.finrank K V. The companion file Codex.Foundations.LinearAlgebra.Basis records the statements used above and packages the cardinality coincidence of any two finite bases.

[object Promise]

This unit is marked lean_status: partial because Mathlib provides every named ingredient — Submodule, Basis, Module.Free.rank, FiniteDimensional, mk_eq_mk_of_basis — but does not package a single self-contained Steinitz-replacement theorem proof in the modern Mathlib idiom; the corresponding statement in the companion module is left as a sorry-gated theorem awaiting the Mathlib-style derivation.

Advanced results [Master]

Subspace lattice. The subspaces of $V$ form a lattice under inclusion, with meet $W_{1} \cap W_{2}$ and join $W_{1} + W_{2} = {w_{1} + w_{2} : w_{1} \in W_{1}, w_{2} \in W_{2}}$ . The dimension formula

dim (W_{1} + W_{2}) + dim (W_{1} \cap W_{2}) = dim W_{1} + dim W_{2}

is the modular identity that characterises this lattice ^{[Hoffman-Kunze — Linear Algebra]}. The lattice is modular but generally not distributive: in $R^{2}$ , three distinct lines through the origin produce a sublattice on which the distributive law fails.

Quotient and direct sum. For a subspace $W \subseteq V$ , the quotient space $V / W$ has dimension $dim V - dim W$ . A choice of complement $W^{'}$ realises the internal direct-sum decomposition $V = W \oplus W^{'}$ and identifies $V / W$ with $W^{'}$ . The dimension count $dim (W \oplus W^{'}) = dim W + dim W^{'}$ holds by concatenating bases.

Infinite-dimensional case. Every vector space has a basis (a Hamel basis), assuming the axiom of choice; existence is proved by Zorn's lemma applied to the partially ordered set of linearly independent subsets ^{[quantum-well Finite dimensional vector spaces.md]}. Any two Hamel bases of $V$ have the same cardinality, and that cardinal is $dim V$ . In an infinite-dimensional Banach space, a Hamel basis is uncountable, and the more useful objects are Schauder bases (allowing convergent infinite sums) or, in Hilbert spaces, orthonormal bases. These are categorically different objects: a Schauder basis depends on the topology and on a choice of summation order, while a Hamel basis is purely algebraic.

Dimension as a categorical invariant. The category $K -Vect^{fd}$ of finite-dimensional vector spaces over $K$ is equivalent to the skeleton consisting of objects $K^{n}$ for $n \geq 0$ , with morphisms $K^{m} \to K^{n}$ given by $n \times m$ matrices. Under this equivalence, isomorphism class corresponds to the natural number $dim$ , so $π_{0}$ of the underlying groupoid is $N$ . The Grothendieck group of the symmetric monoidal category $(K -Vect^{fd}, \oplus)$ is $K_{0} (K -Vect^{fd}) = Z$ , generated by the class $[K]$ , and the dimension homomorphism $dim : K_{0} \to Z$ is an isomorphism.

Module-theoretic generalisation. Over a principal ideal domain, a finitely generated free module has a well-defined rank that plays the role of dimension; the structure theorem decomposes any finitely generated module into a free part and torsion. Over a general commutative ring, dimension fragments into multiple invariants — minimal generator count, Krull dimension, projective dimension — none of which agree in full generality. The clean coincidence available over a field is the algebraic content of "vector space".

Synthesis. This construction generalises the pattern fixed in the vector space unit, with the choice of basis selecting a coordinate system inside an otherwise unstructured object. Read in the opposite direction, dimension is the object that records the structure independently of the coordinates: the same invariant survives every change of basis. The replacement-theorem skeleton appears again in matroid theory, where the same exchange axiom abstracts the linear-independence pattern away from vector spaces and into a combinatorial framework. Putting these together, the central insight is that finite-dimensional linear algebra is governed by a single integer, and that integer is the only invariant separating one finite-dimensional space from another over a fixed field. The same invariant feeds vector-bundle rank, tensor-product dimension counts, exterior-algebra rank, and the discrete data of every Lie-group representation.

Full proof set [Master]

Existence of a basis (finite-dimensional case). Suppose $V$ is spanned by a finite list $S = {v_{1}, \dots, v_{n}}$ . Iterate the following procedure: if some $v_{i}$ is a linear combination of the others, remove it; otherwise stop. The procedure terminates because the list shrinks at each step and stays a spanning set throughout. The final list is linearly independent and spans, hence a basis.

Extension of an independent list to a basis. Let $L = {u_{1}, \dots, u_{k}}$ be linearly independent in a finite-dimensional $V$ with basis $B = {v_{1}, \dots, v_{n}}$ . Apply Steinitz replacement with $B$ as the spanning set and $L$ as the independent list: $k \leq n$ , and the relabelling of $B$ produces ${u_{1}, \dots, u_{k}, v_{k + 1}, \dots, v_{n}}$ spanning $V$ . This list has $n$ elements and $dim V = n$ , so it is a basis ^{[textbooks-extra Calculus Vol.2 - Multi-Variable Calculus and Linear Algebra with Applications (Tom Apostol).pdf]}.

Coordinate isomorphism. A choice of ordered basis $(v_{1}, \dots, v_{n})$ defines

Φ : K^{n} \to V, (a_{1}, \dots, a_{n}) ⟼ a_{1} v_{1} + \dots + a_{n} v_{n} .

Spanning gives surjectivity. Linear independence gives $ker Φ = 0$ , hence injectivity. So $Φ$ is an isomorphism, and every $n$ -dimensional vector space over $K$ is isomorphic to $K^{n}$ .

Hamel basis existence (general case). Let $F$ be the family of linearly independent subsets of $V$ , partially ordered by inclusion. Every chain $C \subseteq F$ has the union $⋃ C$ as an upper bound, which is linearly independent because any finite linear-dependence relation involves only finitely many elements and hence lies inside one member of the chain. Zorn's lemma gives a maximal element $B$ . Maximality forces $span B = V$ : otherwise a vector $v \in / span B$ extends $B \cup {v}$ to a strictly larger independent set. Hence $B$ is a basis.

Equicardinality of Hamel bases. Standard transfinite combinatorics shows that two Hamel bases $B, B^{'}$ of an infinite-dimensional vector space satisfy $∣ B ∣ = ∣ B^{'} ∣$ . The proof reduces to a counting argument: each element of $B^{'}$ is a finite linear combination of elements of $B$ , the assignment is at-most countable-to-one, and cardinal arithmetic with infinite cardinals closes the comparison ^{[Halmos — Finite-Dimensional Vector Spaces]}.

Connections [Master]

Vector space 01.01.03 — supplies the underlying object on which the subspace lattice is built and the algebraic data the basis decomposes.
Bilinear and quadratic forms 01.01.15 — measurement on a vector space pulls back through a basis to a Gram matrix, and the rank of that matrix records the dimension of the radical complement.
Tensor algebra 03.01.04 — the dimension count $dim (V^{\otimes k}) = (dim V)^{k}$ is the multilinear shadow of the present unit, and a basis of $V$ generates a basis of every tensor power.
Vector bundle 03.05.02 — the rank of a bundle is the dimension of every fibre, and a local product chart pulls a basis of the fibre back to a frame on the base.
Differential forms 03.04.01 — the rank of $Λ^{k} V^{*}$ is $(k n)$ , where $n = dim V$ , so the dimension function fixes how many independent $k$ -forms exist on an $n$ -manifold's cotangent space.

Historical & philosophical context [Master]

Hermann Grassmann gave the first systematic account of linearly independent generators and dimension in Die lineale Ausdehnungslehre (1844), formulating the algebra of $n$ -dimensional extension long before the field-axiomatic vector-space concept stabilised ^{[Halmos — Finite-Dimensional Vector Spaces]}. Giuseppe Peano's Calcolo geometrico secondo l'Ausdehnungslehre di H. Grassmann (1888) gave the modern axiomatic definition of a real vector space, including the closure conditions on subspaces and the dimension axiom in essentially their current form.

Ernst Steinitz proved the replacement theorem in 1913 in his memoir Bedingt konvergente Reihen und konvexe Systeme (J. reine angew. Math. 143). The theorem established well-definedness of dimension as a corollary of an exchange procedure and is the algebraic ancestor of the matroid exchange axiom; van der Waerden adopted it as the standard route to dimension in Moderne Algebra (1930), and Hermann Weyl's Theorie der Gruppen und ihrer Darstellungen (1928) presented the linear-algebraic content axiomatically as the foundation for representation theory. Georg Hamel's 1905 paper Eine Basis aller Zahlen und die unstetigen Lösungen der Funktionalgleichung $f (x + y) = f (x) + f (y)$ used Zorn-style choice to construct what is now called a Hamel basis of $R$ over $Q$ , exhibiting an additive function on $R$ that is not linear and demonstrating the choice-dependence of bases in the infinite-dimensional setting.

Bibliography [Master]

Grassmann, H., Die lineale Ausdehnungslehre, ein neuer Zweig der Mathematik, Otto Wigand, Leipzig, 1844.
Peano, G., Calcolo geometrico secondo l'Ausdehnungslehre di H. Grassmann, Bocca, Torino, 1888.
Hamel, G., "Eine Basis aller Zahlen und die unstetigen Lösungen der Funktionalgleichung $f (x + y) = f (x) + f (y)$ ", Mathematische Annalen 60 (1905), 459–462.
Steinitz, E., "Bedingt konvergente Reihen und konvexe Systeme", Journal für die reine und angewandte Mathematik 143 (1913), 128–176.
Weyl, H., Theorie der Gruppen und ihrer Darstellungen, S. Hirzel, Leipzig, 1928.
van der Waerden, B. L., Moderne Algebra, Springer, 1930.
Halmos, P. R., Finite-Dimensional Vector Spaces, Princeton University Press, 1942. §I.5–I.8.
Hoffman, K. & Kunze, R., Linear Algebra, Prentice-Hall, 2nd ed., 1971. §2.
Apostol, T. M., Calculus, Vol. 2: Multi-Variable Calculus and Linear Algebra with Applications, 2nd ed., Wiley, 1969. Ch. 1 §1.7–§1.13.

Autonomous production unit. Pulled-prerequisite for rank-nullity, tensor-algebra dimension counts, and vector-bundle rank.

Prerequisites

01.01.03

Tier anchors

beginner: 3Blue1Brown — Essence of Linear Algebra Ch. 2 (linear combinations, span, basis)
intermediate: Axler — Linear Algebra Done Right §2; Apostol Calculus Vol. 2 Ch. 1 §1.7–§1.13
master: Halmos — Finite-Dimensional Vector Spaces §I.5–I.8; Hoffman-Kunze §2; Lang Algebra Ch. III §5

References

quantum-well
md/Mathematical foundations/Algebra/Linear Algebra and Matrix Theory/Vector space dimension.md · vector space dimension entry
quantum-well
md/Mathematical foundations/Algebra/Linear Algebra and Matrix Theory/Finite dimensional vector spaces.md · finite-dimensional vector spaces entry
quantum-well
md/Mathematical foundations/Algebra/Linear Algebra and Matrix Theory/Proofs and examples/Proof that the sum of subspaces is also a subspace.md · proof that the sum of two subspaces is a subspace
textbooks-extra
Calculus Vol.2 - Multi-Variable Calculus and Linear Algebra with Applications (Tom Apostol).pdf · Ch. 1 §1.7–§1.13, subspaces, linear independence, bases, dimension
TODO_REF
Halmos — Finite-Dimensional Vector Spaces · §I.5–I.8, subspaces, bases, dimension; Steinitz replacement
TODO_REF
Hoffman-Kunze — Linear Algebra · §2, subspaces and bases
TODO_REF
Steinitz, E. — Bedingt konvergente Reihen und konvexe Systeme · J. reine angew. Math. 143 (1913), replacement theorem

Lean module

Codex.Foundations.LinearAlgebra.Basis

Mathlib gap

Mathlib already provides Submodule, Basis, Module.Free.rank, FiniteDimensional, and the cardinality coincidence of any two bases via mk_eq_mk_of_basis. What it lacks in unified form is a single self-contained Steinitz replacement theorem proof in the modern Mathlib idiom — the statement that a linearly independent family is no larger than any spanning family, with an explicit replacement procedure — and the categorical Grothendieck-group identification K_0(K-Vect^fd) = Z generated by the class of K. Both are derivable from existing Mathlib lemmas; they are not packaged as named results.

Reviewer

TBD

Estimated time

beginner: 18m
intermediate: 40m
master: 70m