Linear maps

A linear map respects the two operations of a vector space: adding first and then mapping is the same as mapping first and then adding, and likewise for scaling. That is all it takes for two subsets to appear automatically: the vectors the map sends to 0, which is where it loses information, and the vectors it actually reaches. Both are subspaces.

T0 = 0: T0 = T(0 + 0) = T0 + T0, and subtracting T0 from both sides gives T0 = 0.

(a) Let S be a subspace of X. Then 0 = T0 is in T(S). If Tx and Ty are in T(S), with x, y in S, then Tx + Ty = T(x + y) and x + y is in S, so the sum is in T(S). If Tx is in T(S) and k is a scalar, kTx = T(kx) with kx in S. (b) Let S′ be a subspace of U and S the set of x with Tx in S′. T0 = 0 is in S′, so 0 is in S. If Tx and Ty are in S′, then T(x + y) = Tx + Ty is in S′, so x + y is in S; and T(kx) = kTx is in S′, so kx is in S.

One-to-one: if T is one-to-one and Tx = 0 = T0 then x = 0. Conversely if N_T = {0} and Tx = Ty, then T(x − y) = Tx − Ty = 0, so x − y = 0. □

Lax p.20 (Theorem 1 is left to the reader there as Exercise 1; the proof above is mine). Lean: theorem1a and theorem1b. What the Lean proof is. Each states that a subspace exists whose underlying set is the image, respectively the inverse image, and is proved by Mathlib’s own constructions Submodule.map and Submodule.comap, whose underlying sets are those by definition. So it records that the sentence is true over any field; it does not re-do the three checks above. The fact T0 = 0 and the one-to-one criterion are not stated separately in Lean. Both theorems compiled clean on the first run (axioms: propext, Quot.sound).

The script checks Theorem 1 on every linear map between the F_p-spaces (p, n, m) = (2,1,1), (2,2,2), (3,2,2), (2,3,2), (2,2,3), (2,3,3), (3,2,3), (3,3,2): all 2 + 16 + 81 + 64 + 64 + 512 + 729 + 729 matrices, each tested on every subspace of the domain and of the target.

T cannot tell apart two vectors that differ by something in the kernel. So the vectors that land on one target point are exactly one coset of the kernel, and every reached point has such a coset above it, all the same size. The domain is therefore the kernel’s dimension plus the number of independent directions that survive, which is the dimension of the range. Move the entries in the plate: whenever the gold set grows, the lit set on the right shrinks by the same number of dimensions.

If x₁ and x₂ are equivalent modulo N_T, then x₁ − x₂ is in N_T, so Tx₁ = Tx₂. So T is well defined on the quotient space X/N_T: set T̃{x} = Tx. It is linear (the operations on classes are done through representatives). It is onto R_T by the definition of the range. It is one-to-one: if T̃{x} = 0 then Tx = 0, so x is in N_T and {x} = {0}. So X/N_T and R_T are isomorphic and have the same dimension. By Theorem 6 of Chapter 4, dim X/N_T = dim X − dim N_T. Combine. □

Lax pp.20–21, his proof. Lean: theorem2. What the Lean proof is. It is Mathlib’s rank–nullity theorem (LinearMap.finrank_range_add_finrank_ker) with the two terms put in Lax’s order by omega. It is not the quotient-space argument above, which is not formalized here; it checks that the statement is true over any field. Compiled clean on the first run.

The script checks, on every one of the maps listed in §1 and on all 19,683 maps of F₃³ to itself: |N_T|·|R_T| = pⁿ. On every map of the eight smaller families it also checks the proof’s steps: each fibre is exactly a coset x + N_T, and the number of cosets equals |R_T|. As a by-product, and beyond Lax, it checks that the number of linear maps F_pⁿ → F_p^m of rank r is the product over i < r of (pⁿ − pⁱ)(p^m − pⁱ)/(p^r − pⁱ) in every case listed: for the plane it gives 1, 9 and 6 maps of rank 0, 1 and 2 over F₂ (total 16), and 1, 32 and 48 over F₃ (total 81). I have verified that formula by counting, not proved it here.

If the target is smaller than the domain, T cannot be one-to-one: there is not enough room on the other side, so something nonzero is lost. If the target and domain have the same dimension and nothing nonzero is lost, then nothing is missed either, and T reaches every vector. In terms of equations: more unknowns than equations always leaves a nonzero solution of the homogeneous system, and a square system whose homogeneous version has only the zero solution can be solved for any right-hand side, in exactly one way.

A. dim R_T ≤ dim U < dim X, because R_T is a subspace of U. By Theorem 2, dim N_T = dim X − dim R_T > 0, so N_T contains a vector other than 0.

B. N_T = {0}, so dim N_T = 0. By Theorem 2 and dim U = dim X, dim R_T = dim X = dim U. By Corollary 6′ of Chapter 4, a subspace of the same dimension as the whole space is the whole space; so R_T = U.

A′ and B′ are A and B for the map u_i = ∑_j t_ijx_j. The uniqueness in B′: if x and x′ both solve the system, T(x − x′) = 0, so x = x′ by the one-to-one criterion of §1. □

Lax p.21–22. Lean: corollaryA, corollaryB, derived from theorem2 as above (B uses Mathlib’s Submodule.eq_top_of_finrank_eq for Corollary 6′). The concrete versions A′ and B′ are not stated in Lean separately. Compile history: the first run had corollaryB and the control clean and corollaryA failing at simp [hk] at h4 (“made no progress”: the hypothesis could not be rewritten through the kernel’s dependent type), so it depended on sorryAx. The fix proves the dimension of the kernel is 0 the way corollaryB does and then closes by omega; the recompile is clean.

Each hypothesis is doing work, and the controls show it. Over any field, (x, y) → (x, 0) has equal dimensions but a nonzero kernel and misses most of the plane: Corollary B needs “only x = 0 goes to 0”. It is control_corollaryB_needs_trivial_kernel in the Lean file (over the rationals) and is checked over F₂, F₃ and F₅ in the script. (x, y) → (x, y, 0) from F₃² to F₃³ has a trivial kernel and is not onto: Corollary B needs dim U = dim X. The identity of the plane has m = n and a trivial kernel: Corollary A needs the strict inequality m < n.

The script checks Corollary A on every map F_pⁿ → F_p^m with m < n in the list; Corollary B on every square map, including that each target vector has exactly one preimage and that every map with a nonzero kernel is not onto; and that the number of square maps with trivial kernel is (pⁿ − 1)(pⁿ − p) … (pⁿ − pⁿ⁻¹), the same count as ordered bases in Chapter 4: 6, 48, 168 and 11,232.

Two points fix a line; three points fix a parabola. In general n distinct points fix a polynomial of degree below n, and any values at those points are possible. The map that records the values has a domain and target of dimension n, so Corollary B turns the easy half, that a nonzero polynomial cannot vanish at all n points, into the hard half, that every list of values is hit.

dim X = n (the monomials 1, s, …, sⁿ⁻¹ are a basis) and dim U = n. N_T is trivial: Tp = 0 means p vanishes at n distinct points, and a nonzero polynomial of degree less than n has fewer than n zeros. (Standard: if p(s₁) = 0 then p = (s − s₁)q with deg q < deg p; at each further zero s_i distinct from s₁, q(s_i) = 0 because the field has no zero divisors; after n zeros p would be divisible by a polynomial of degree n, forcing p = 0.) By Corollary B, R_T = U. □

Lean: interpolation, over an arbitrary field K, with s injective and conclusion “degree p < n and p(s_i) = u_i for all i”. What the Lean proof is. It follows Lax’s structure: the evaluation map on the polynomials of degree below n (Mathlib’s degreeLT), proved one-to-one with Mathlib’s bound on the number of zeros, then onto by Mathlib’s “one-to-one implies onto for equal finite dimensions”, which is Corollary B’s content. It was the most name-fragile theorem in the file (several Polynomial lemma names were flagged in the header), and it compiled clean on the first run, so those names resolved.

The script checks: over F₃ (n ≤ 3), F₅ (n ≤ 5) and F₇ (n ≤ 3), for every ordered list of n distinct points (15, 325 and 259 lists), that the pⁿ polynomials take pⁿ different value lists, which is exactly onto. And it breaks each hypothesis: a repeated point (0, 0, 1) over F₅ misses 100 of the 125 value lists, because x(x − 1) vanishes at all three; degree below 4 with three distinct points always has a nonzero kernel; and x⁵ − x vanishes at all five points of F₅ though it is not zero, so “less than n” cannot be relaxed to “at most n”. Over the rationals it solves one case exactly: nodes 0, 1, 2, 5 and values 3, −1, 4, 1 give the polynomial 3 − (109/10)s + (81/10)s² − (6/5)s³, evaluated back at the nodes with exact fractions.

Not done here. Lax’s Application 2 (averages over disjoint intervals, which needs the fact that a function with average zero changes sign) and Application 3 (the lattice equations for Laplace’s equation, which needs the maximum principle) are on pp.22–23; I did not work through them and the Lean file does not contain them.

Near a point, a smooth nonlinear map looks like a linear one: the Jacobian matrix of its partial derivatives. Everything in §§1–3 then applies to that linear map, and the kernel is the place to look. A direction in the kernel is one where the linear model says nothing moves, to first order. What the map actually does in that direction is a second-order effect, and the linear model cannot see it. This is the question Interlude 1 asked, when to linearize, in its smallest form.

(i) F(a + h) = ((1 + h₁)² + 2 + h₂, (1 + h₁)(2 + h₂)) = (3 + 2h₁ + h₁² + h₂, 2 + 2h₁ + h₂ + h₁h₂), F(a) = (3, 2), and Jh = (2h₁ + h₂, 2h₁ + h₂). Subtract. (ii) Both rows of J are (2, 1), so the range of J is the line spanned by (1, 1) and has dimension 1, and by Theorem 2 the kernel has dimension 2 − 1 = 1. J(1, −2) = (2 − 2, 2 − 2) = 0. (iii) From (i) with h = (t, −2t): Jh = 0, so F(a + h) − F(a) = (t², −2t²). The range of J is the line through (1, 1), and (1, −2) is not along it: the motion in the kernel direction leaves the linear model’s line, at order t². (iv) For a linear A, write A = J + E with E ≠ 0. The remainder at h = tu is t(J − A)u + t²(u₁², u₁u₂) = −tEu + t²(u₁², u₁u₂). Choose u with Eu ≠ 0. Dividing by |tu| leaves −Eu/|u| plus a term of size at most t|u|, which does not tend to 0 as t → 0. For A = J, only the second term is left, of size at most t|u|. □

This is one function at one point, computed exactly. It illustrates the idea and proves nothing general; there is no Lean for it in this chapter. The general statement (differentiable means there is a linear map with a remainder smaller than |h|; the directional derivative is that map applied to the direction; the gradient direction maximizes it) is Book XVIII chapter 8, Several variables, from Loomis–Sternberg Chapter 3, with its own Lean file (also not yet compiled when this page was written). I used the sup norm for the remainder estimates; any norm on the plane gives the same conclusion.

The script checks (i) on 841 rational h, (ii)–(iii) at several t including negative and fractional ones, and (iv) for all 80 nonzero integer E with entries in {−1, 0, 1} in five directions at t = 1/1000 and 1/1,000,000, in exact arithmetic. That the point (1, 2) has singular Jacobian is a feature of the example I chose, not a property of F: det J = 2x² − y vanishes along the whole parabola y = 2x².

Lax works over the reals or complex numbers, and Application 1 over the complex numbers. Sections 1–4 use only that K is a field: the plate, the script and the Lean file are over F_p, over any field K, and over the rationals in the control. The step that needs the field axioms is the one that bounds the zeros of a polynomial (no zero divisors); over F_p it also explains why n distinct points exist only for n ≤ p. Section 5 is different: the Jacobian needs limits, so it lives over the reals (or complex numbers), and the finite-field checks say nothing about it.