Vector space

Intuition [Beginner]

A vector space is a place where adding arrows and stretching arrows always makes sense. If two arrows live in the same vector space, their sum lives there too. If an arrow is stretched by a number, the result also lives there.

The idea matters because it separates the rules from the picture. Arrows in the plane are vector-space examples, but so are lists of numbers, polynomials, signals, and solutions to many equations. Once the rules are shared, the same algebra works in all of these settings.

Think of a vector space as a workshop with two reliable tools: combine and scale.

Visual [Beginner]

The blue and red arrows combine to make the green arrow. The purple arrow is stretched but stays in the same plane.

The picture shows the two operations, not the full definition. A vector space is any collection where these operations obey the same basic rules.

Worked example [Beginner]

Work in the usual coordinate plane. Take the arrow $(3,1)$ and the arrow $(-1,4)$.

Adding them means adding matching coordinates:

$$(3,1)+(-1,4)=(2,5).$$

Stretching the first arrow by $2$ gives

$$2(3,1)=(6,2).$$

Both results are still arrows in the coordinate plane.

What this tells us: the coordinate plane is closed under the two vector-space operations, addition and scaling.

Check your understanding [Beginner]

Formal definition [Intermediate+]

Let $K$ be a field. A vector space over $K$ is an abelian group $(V,+,0)$ together with a scalar multiplication map

$$K\times V⟶V,(a,v)⟼av,$$

such that, for all $a,b\in K$ and all $u,v\in V$,

$$a(u+v)=au+av,(a+b)v=av+bv,$$ $$(ab)v=a(bv),1v=v.$$

The elements of $V$ are vectors; the elements of $K$ are scalars. This is Mathlib's Module K V structure when K is a field ^{[quantum-well Vector spaces.md]}.

Standard examples include $K^n$, polynomial spaces $K[x]$, function spaces $X\to K$, and solution spaces of homogeneous linear equations. The one-element vector space exists over every field and contains only the zero vector.

Key theorem with proof [Intermediate+]

Theorem (elementary consequences of the axioms). Let $V$ be a vector space over a field $K$. For every $v\in V$ and every $a\in K$,

$$0v=0,a0=0,(-1)v=-v.$$

Proof. For the first identity, use distributivity over scalar addition:

$$0v=(0+0)v=0v+0v.$$

Add the additive inverse of $0v$ to both sides. The result is $0=0v$, so $0v=0$.

For the second identity, use distributivity over vector addition:

$$a0=a(0+0)=a0+a0.$$

The same cancellation gives $a0=0$.

For the third identity,

$$v+(-1)v=1v+(-1)v=(1+(-1))v=0v=0.$$

Thus $(-1)v$ is an additive inverse of $v$. The additive inverse is unique in the abelian group $(V,+,0)$, so $(-1)v=-v$. $\square$

Bridge. The construction here builds toward 01.01.15 (bilinear form / quadratic form), where the same data is upgraded, and the symmetry side is taken up in 03.01.04 (tensor algebra). The defining pattern appears again in those units in a sharpened form, where the local data is glued or quotiented. Putting these together, the foundational insight is that the data of this unit gives the structural signature that the rest of the strand reads off.

Exercises [Intermediate+]

Lean formalization [Intermediate+]

Mathlib models vector spaces as modules over a field. The companion file Codex.Foundations.LinearAlgebra.VectorSpace records the distributive laws and elementary zero-scalar consequences used above.

[object Promise]

This unit is marked lean_status: full because its formal content is within Mathlib's standard algebraic hierarchy.

Advanced results [Master]

Every vector space has a basis, assuming the usual choice principle. For finite-dimensional spaces, a basis is a finite list of linearly independent vectors that spans the space; every vector has a unique coordinate expression in that basis. For arbitrary vector spaces, the same statement is proved by Zorn's lemma ^{[Halmos Ch. 1]}.

If $V$ has a basis indexed by $I$, then $V$ is isomorphic to the direct sum

$$K^{(I)}=\{(a_i{)}_{i\in I}:a_i=0\text{ for all but finitely many }i\}.$$

This identifies vector spaces over a fixed field by dimension: two vector spaces over $K$ are isomorphic exactly when their bases have the same cardinality.

The categorical form is also important. A vector space over $K$ is a module over the field $K$, and the category ${\mathrm{Vect}}_K$ is an abelian category with kernels, cokernels, direct sums, and exact sequences. The finite-dimensional subcategory is rigid monoidal under tensor product and duals.

Synthesis. This construction generalises the pattern fixed in 00.02.05 (function), with the symmetric data replaced by its skew or twisted analogue. Read in the opposite direction, the construction is dual to the metric story: complements and orthogonality are taken with respect to the bilinear datum of this unit, not a metric, and the resulting category of subobjects is the one the rest of the strand classifies. The central insight is that this datum identifies algebra with geometry: functions become vector fields, subspaces become quotients, and invariants become cohomology classes — and that identification is the engine driving every theorem downstream.

Full proof set [Master]

Basis classification in finite dimension. Let $V$ be finite-dimensional. Any spanning list can be shortened to a basis by deleting vectors that are linear combinations of earlier vectors. Any linearly independent list can be extended to a basis by adding vectors from a fixed spanning list until the span is all of $V$. The exchange lemma proves that any two bases have the same number of elements, so dimension is well-defined ^{[Hoffman-Kunze §1]}.

Coordinate isomorphism. If $(v_1,\dots ,v_n)$ is a basis of $V$, define

$$\Phi :K^n\to V,(a_1,\dots ,a_n)\mapsto a_1{v}_1+\cdots +a_n{v}_n.$$

Spanning makes $\Phi$ surjective. Linear independence makes $\ker \Phi =0$, so $\Phi$ is injective. Therefore $\Phi$ is a vector-space isomorphism.

Subspace criterion. A nonempty subset $S\subseteq V$ is a subspace exactly when it is closed under linear combinations $au+bv$. If $S$ is a subspace, closure is inherited from scalar multiplication and addition. Conversely, closure under $au+bv$ gives $0\in S$ by choosing $a=0$, gives additive inverses by choosing $a=-1$, and gives closure under addition and scalar multiplication by choosing the other coefficients appropriately.

Connections [Master]

• Bilinear forms 01.01.15 — require vector spaces before one can evaluate two vector inputs.

• Tensor algebra 03.01.04 — starts from a vector space and builds the free associative algebra generated by it.

• Clifford algebra 03.09.02 — is a quotient of the tensor algebra of a vector space by quadratic relations.

• Fredholm operators 03.09.06 — act on infinite-dimensional vector spaces with topology added.

• Vector bundle 03.05.02 — places one vector space over each point of a base space.

Historical & philosophical context [Master]

The abstract vector-space concept emerged from nineteenth-century linear equations, determinants, and geometry, then stabilized through early twentieth-century algebra. The modern axiomatic presentation treats vectors as elements of any set with addition and scalar multiplication satisfying structural laws, not as coordinate tuples alone ^{[Halmos Ch. 1]}.

Halmos's Finite-Dimensional Vector Spaces helped set the mid-century American style for coordinate-free linear algebra. Axler later emphasized linear maps and invariant subspaces while delaying determinants, a choice reflected in the modern definition-first route through vector spaces ^{[quantum-well Axler S., Gerhing F.W., Ribet K.A. Linear Algebra Done Right, Springer, 2nd edition, 1997.md]}.

Bibliography [Master]

• Halmos, P. R., Finite-Dimensional Vector Spaces, Princeton University Press, 1942.
• Axler, S., Linear Algebra Done Right, Springer, 1997. §1.A.
• Hoffman, K. & Kunze, R., Linear Algebra, Prentice-Hall, 2nd ed., 1971. §1.
• Bourbaki, N., Algebra I, Chapters 1-3, Springer, 1989.

---

Wave 2 Phase 2.1 unit #1. Produced as a foundational pulled prerequisite for Clifford algebra, Fredholm operators, and characteristic-class units.