A vector space is what you may do with vectors once you stop looking at their components: add them and scale them. This chapter fixes the axioms, the subspaces, and the one construction that throws information away on purpose, the quotient.
The object. The grid of points of Fp² (pairs of numbers mod p), a chosen direction d, and the classes you get by sliding along d. Points of one colour are congruent modulo the line spanned by d. Change p or d and watch the classes regroup.
A vector space over a field K is a set with two operations: add two vectors, multiply a vector by a number from K. Nothing else is assumed. Lax’s reason for working this abstractly (p.1) is that many spaces do not come as arrays: the solutions of a linear differential equation, or the vectors whose components add to zero. The plate above is the other extreme, the smallest possible example, where every vector can be listed.
(a) Taking x = 0 gives 0 + z = 0, and 0 + z = z because 0 is neutral. So z = 0. (b) 0x + 0x = (0 + 0)x = 0x = 0x + 0, and cancelling 0x from both sides gives 0x = 0. (c) x + (−1)x = 1x + (−1)x = (1 + (−1))x = 0x = 0, so (−1)x is an additive inverse of x, and inverses in a group are unique, so it equals −x. □
(a) is Lax’s Exercise 1 (p.2); (b) and (c) are his deductions on pp.2–3. In VectorSpace.lean they are zero_unique, zero_smul_axioms and neg_one_smul_eq_neg, stated for Mathlib’s Module K V over any field. The script checks the axioms and all three consequences exhaustively on F2² and F3²; that is a check of two examples, not a proof. The author compiled the Lean file: no errors, no warnings, and the axiom report shows no sorryAx.
A subspace is a subset you cannot leave by adding or scaling. In the plane over the reals: the origin, any line through it, the whole plane. A line that misses the origin is not one; neither is the first quadrant.
{0}: 0 + 0 = 0 and k0 = 0. Y ∩ Z: each condition holds in Y and in Z, hence in both. Y + Z: 0 = 0 + 0; (y + z) + (y′ + z′) = (y + y′) + (z + z′); k(y + z) = ky + kz. □
Lax Exercises 6, 7, 8 (p.4). Lean: trivial_isSub, inter_isSub, sum_isSub, with a subspace defined by exactly the three conditions above, not by Mathlib’s Submodule, so the statement reads against the book. Exhaustive check in F3³ for Y = span(e1, e2) and Z = span(e2, e3): Y ∩ Z has 3 elements and Y + Z has 27.
Fix a subspace Y. Call two vectors the same if they differ by something in Y. The plate shows it: with p = 3 and d = (1, 0), the points of one row share a colour, and a row is a coset of the line. Lax’s own example (p.8): in the space of vectors with n components, take Y to be those whose first two components are zero. Then two vectors are congruent exactly when their first two components agree, and forming the quotient “throws away” the other components.
(a) x − x = 0 ∈ Y. If x − y ∈ Y then y − x = (−1)(x − y) ∈ Y by Proposition 1(c). If x − y and y − w are in Y, so is their sum x − w. (b) (x1 + z1) − (x2 + z2) = (x1 − x2) + (z1 − z2) ∈ Y, and kx1 − kx2 = k(x1 − x2) ∈ Y. □
Lax Exercises 13 and 15 (pp.7–8). Lean: cong_refl, cong_symm, cong_trans, cong_add, cong_smul. The control matters: for Y = {0, 1} in the rationals, which is not a subspace, 2 ≡ 1 and 1 ≡ 0 but 2 ≬ 0, so transitivity fails (control_cong_not_trans; the script checks it, and also a non-subspace of F3²). The script checks (a) and (b) on every triple and every quadruple of F3³ for a line and for a plane, and the button on the plate does the same for the grid you chose.
Not done here. That the set of classes V/Y with these operations satisfies the nine axioms follows by computing on representatives; I have not written it out and it is not in the Lean file. The dimension count dim Y + dim(V/Y) = dim V is Lax’s Theorem 6 (p.8) and is proved in Chapter 4; the script only notes that the class counts in F3³ (9 for a line, 3 for a plane) are consistent with it. [OPEN]
A link back to Chapter 2. The solutions of x′ = Ax + b, when there is one solution u, are exactly u + S where S is the solution space of x′ = Ax: a coset of S. That is an instance of the construction here, not a shared mechanism with anything else in the series.
Lax takes K to be the real or the complex numbers (p.3) and says so, since his text is analytic. The proofs above never use that. They use only that K is a field, so they hold over Fp as well, and the plate lives there because its spaces are small enough to draw and to check exhaustively.
Working over Fp goes beyond Lax. The integers mod 4 are not a field: 2x is 0 or 2 for every x, so 2 has no inverse; that is why p must be prime. That the integers mod a prime p do form a field is a standard fact that I cite and have not proved here; the script checks the vector-space axioms for F2² and F3² directly.