Basis and dimension

In the plane, two vectors can point in different directions; three cannot, whatever you choose. The exchange lemma is that observation made into a theorem about every vector space: a list that reaches everything is never shorter than a list in which nothing is redundant. Its proof swaps the vectors of the second list in for the first, one at a time, and watches the first list run out.

Proposition 4: if x_i = 0, then 1·x_i plus 0 times each of the others is a combination, not all coefficients zero, equal to 0, so the list is dependent.

Lemma 1. Claim: for each m with m ≤ j and m ≤ n, after renumbering the x’s, the list y₁, …, y_m, x_m+1, …, x_n still spans V. For m = 0 this is the hypothesis. Suppose it holds for m and that m + 1 ≤ j and m + 1 ≤ n. Write y_m+1 = a₁y₁ + … + a_my_m + b_m+1x_m+1 + … + b_nx_n. If every b were zero, y_m+1 would be a combination of y₁, …, y_m, contradicting independence. So some b_i ≠ 0; renumber it as b_m+1. Solving for x_m+1 expresses it through y₁, …, y_m+1 and x_m+2, …, x_n, so the new list spans whatever the old one did, namely V. That proves the claim.

Now suppose j > n. Take m = n: the list y₁, …, y_n spans V. Then y_n+1 is a combination of y₁, …, y_n, which contradicts independence. So j ≤ n. □

Lax Exercise 10, Lemma 1 (p.5). He states it with sets and sketches the replacement; the invariant above, and the case where the x’s run out, are written out here. Lean: indep_ne_zero and lemma1. What the Lean proof is. lemma1 is proved by Mathlib’s counting lemma for spanning finsets (linearIndependent_le_span_finset), not by the replacement argument; it checks that the sentence above is true over every field, not that this proof is right. single_vector_not_span_plane applies it: one vector never spans the rational plane. control_dependent_family is the control: three vectors in a plane exist (the zero family) but are not independent, so independence is doing real work. [OPEN] none of it has been compiled.

The script checks Lemma 1 on every list of length up to n + 1 (up to n for F₃³) in F₂², F₃², F₂³ and F₃³: the longest independent list is exactly as long as the shortest spanning list, which is n.

A basis is a spanning list with nothing redundant. Lemma 1 says that any spanning list is at least as long as any independent list, so two bases are each at least as long as the other. The common length is the dimension. In the plate above, any two independent vectors in F₃² form a basis, and there are 48 ordered pairs of them.

Lemma 2: if the x’s are dependent, some x_i is a combination of the others, and dropping it does not change the span. Repeat; the list gets shorter each time, so it stops, at a list that still spans and has no dependence. That is a basis.

Theorem 3: let x₁, …, x_n and y₁, …, y_m be two bases. The x’s span and the y’s are independent, so m ≤ n by Lemma 1; the y’s span and the x’s are independent, so n ≤ m. Hence m = n.

Theorem 4: let n = dim V. If the y’s do not span V, some vector x is not a combination of them. Adjoin it. The longer list is still independent: in a relation k₁y₁ + … + k_jy_j + cx = 0, c must be 0 (otherwise x would be a combination of the y’s), and then every k_i is 0 because the y’s are independent. Repeat. By Lemma 1 an independent list in V has at most n vectors, so this stops after at most n − j steps, at an independent list that spans: a basis. □

Lax pp.5–6. Lean: lemma2 and theorem3. theorem3 is Lax’s argument as written: two uses of lemma1, one in each direction. lemma2 builds the basis from Mathlib’s finBasis rather than by dropping vectors. Lean states the bases as families indexed by Fin m and Fin n, where Lax speaks of sets of vectors. Not in Lean: Theorem 4. [OPEN]

The script checks, in all four spaces: no independent list contains a zero vector; every basis has length n; the number of ordered bases is (pⁿ − 1)(pⁿ − p) … (pⁿ − pⁿ⁻¹), which is 6 in F₂², 48 in F₃², 168 in F₂³ and 11,232 in F₃³; and that every independent list of length at most n completes to a basis by adjoining vectors (Theorem 4). The counts are consistent with the theorem; they are not a proof of it.

Cut a subspace Y out of V. Is there a second subspace Z such that every vector splits as a piece in Y plus a piece in Z, and in only one way? Yes, always, but there is no canonical choice of Z. In F_p², a line Y through the origin has p other lines through the origin, and each is a complement.

(a) Choose y₁ ≠ 0 in Y if Y ≠ {0}, then y₂ not in the span of y₁, and so on, always adding a vector outside the span so far. Each list stays independent, and by Lemma 1 it cannot exceed n = dim V, so the process stops, at a list that spans Y: a basis of Y.

(b) Complete that basis y₁, …, y_j to a basis y₁, …, y_j, z_j+1, …, z_n of V by Theorem 4, and let Z be the span of the z’s. Every x is a combination of the basis, which splits as a piece in Y plus a piece in Z. Uniqueness: if y + z = y′ + z′, then y − y′ = z′ − z lies in Y and in Z. Writing it in both bases and using that the whole list is independent, every coefficient is zero. So y = y′ and z = z′. The basis of Z has n − j vectors, so dim V = n = j + (n − j) = dim Y + dim Z.

Exercise 12: a basis e₁, …, e_n of V gives the map that sends k₁e₁ + … + k_ne_n to (k₁, …, k_n). It is linear, and it is bijective because each vector has exactly one such expression. Different bases give different maps, and for n > 1 there are several bases. □

Lax pp.6–7. Lean: theorem5a, theorem5b and exercise12. theorem5b states Lax’s sentence (existence and uniqueness of the splitting, plus the dimension formula); the complement is obtained from Mathlib’s exists_isCompl, and the uniqueness is derived from it in the file. exercise12 proves that an isomorphism exists; the non-uniqueness half is not in Lean. [OPEN]

The script lists every subspace of F₂², F₃², F₂³ and F₃³ (5, 6, 16 and 28 of them) and checks that each has complements, that each complement adds dimensions, and that a j-dimensional subspace of an n-dimensional space has exactly p^j(n−j) of them, so never just one when 0 < j < n. It counts isomorphisms F_pⁿ → F_pⁿ as (pⁿ − 1) … (pⁿ − pⁿ⁻¹) (6, 48, 168, 11,232). Over F₃ even n = 1 has two isomorphisms (multiplication by 1 and by 2), so “not unique” is only a statement about n > 1 for F₂.

Not done here. Lax’s Exercise 11 (dimension of a direct sum of m subspaces) is left as an exercise.

Chapter 3 formed V/Y by forgetting what Y contributes. Theorem 6 says what is left: whatever dimension Y has, the rest is the quotient. The proof shows which vectors carry it: complete a basis of Y by new vectors x_k, and the classes of the x_k alone are a basis of V/Y.

Let y₁, …, y_j be a basis of Y, j = dim Y, completed by x_j+1, …, x_n to a basis of V, n = dim V (Theorem 4). Claim: the classes {x_j+1}, …, {x_n} are a basis of V/Y.

They span: every x is a combination ∑a_iy_i + ∑b_kx_k, and the y’s lie in Y, so {x} = ∑b_k{x_k}. They are independent: if ∑c_k{x_k} = {0}, then ∑c_kx_k lies in Y, so equals ∑d_iy_i for some d_i; moving it across gives a relation among basis vectors of V, so all c_k and d_i are zero. So dim(V/Y) = n − j, and dim Y + dim(V/Y) = j + (n − j) = n.

Corollary 6′: if dim Y = dim V then dim(V/Y) = 0, so V/Y has the empty list as a basis and its only element is the class of 0. Every x then satisfies {x} = {0}, which means x − 0 lies in Y. So Y = V. □

Lax pp.8–10 (Theorem 6, Corollary 6′; Exercise 17 is the proof of the corollary). Lean: theorem6, corollary6. Both are calls to Mathlib’s theorems about finrank of a quotient and of a subspace of full dimension, stated in Lax’s words; the basis argument above is not re-done in Lean. [OPEN]

The script checks, for every subspace of all four spaces, that the number of classes is p^n−j, that the classes of the added vectors span V/Y and are independent (the claim in the proof, tested on one completion per subspace), and that a subspace of dimension n is everything. Lax Exercise 16 (polynomials of degree below n vanishing at j points) is in the exercises; the script checks it over F₃ with n = 3 and every choice of j distinct points in F₃.

Two planes through the origin in 3-space meet in a line, and together they fill the space: 2 + 2 − 1 = 3. Theorem 7 is that count in every dimension. The overlap is counted twice by the dimensions, so it is subtracted once. The proof reduces the general case to a sum that has no overlap, by collapsing the overlap W to a point.

Theorem 7. If W = {0}, this is Theorem 5. In general, W lies in U and in U′. Let U₀ be the set of classes {u} in V/W with u in U, and U′₀ likewise. The map u → {u} from U to V/W is linear with kernel U ∩ W = W, so U₀ is isomorphic to U/W and dim U₀ = dim U − dim W by Theorem 6. Similarly dim U′₀ = dim U′ − dim W.

U₀ and U′₀ meet only in {0}: if {u} = {u′} with u in U, u′ in U′, then u = u′ + w with w in W, and W lies in U′, so u lies in U′, hence in U ∩ U′ = W, so {u} = {0}. And U₀ + U′₀ is all of V/W, since V = U + U′. By the case W = {0}, dim(V/W) = dim U₀ + dim U′₀. By Theorem 6, dim(V/W) = dim V − dim W. So dim V − dim W = (dim U − dim W) + (dim U′ − dim W), which is the formula. □

Exercise 18: the pairs (b_i, 0) and (0, c_k), for bases of V₁ and V₂, form a basis of the Cartesian sum. Exercise 19: choose a complement Z of Y (Theorem 5). Each class of V/Y meets Z in exactly one point, because x and x′ in the same class and both in Z give x − x′ in Y ∩ Z = {0}; and every class meets Z, since x = y + z puts z in the class of x. Send (y, class) to y + (that point of Z). This is linear and bijective, so Y ⊕ V/Y ≅ V. The isomorphism depends on the choice of Z. □

Lax pp.10–11. Lean: theorem7, exercise18, exercise19; each is a short call to Mathlib’s finrank theorems for sums, products and quotients. theorem7 is stated additively (dim V + dim W = dim U + dim U′) to avoid subtraction in the natural numbers. [OPEN]

The script checks Theorem 7 on every pair of subspaces with U + U′ = V in the four spaces (15, 23, 129 and 445 pairs), and the identity without that hypothesis (dim(U + U′) + dim(U ∩ U′) = dim U + dim U′) on every pair. It also checks each step of the proof: |U₀| = |U|/|W|, U₀ ∩ U′₀ = {0}, U₀ + U′₀ = V/W. For Exercise 19 it builds the explicit map above for every subspace of all four spaces and confirms it is a bijection that respects addition. Exercise 18 is checked only by counting elements (p^n₁+n₂).

Lax works over the reals or complex numbers. Nothing above uses that: only that K is a field, so every statement and proof holds over F_p, which is where the plate and the script live, and the Lean file is over an arbitrary field. The field axiom is used where the proof of Lemma 1 divides by the nonzero coefficient b to solve for x_m+1. Over a ring that is not a field that step is unavailable, and I have not checked here what happens to the lemma there.