A vector is a thing; a linear function is a way of measuring it. Every space of things has a second space of measurements, of the same size, and a map between the things carries measurements backwards. That one idea explains the transpose, rank and nullity from the other side, how a quadrature rule is found, why a quadratic form changes under a change of basis by a rule different from a matrix’s, and what a tensor product is.
The object. A three-point rule on [−1, 1] with nodes −a, 0, a. Choose a² and read off the three weights (found from the dual space, section 4), whether they are all positive, and which powers tk the rule integrates exactly. The button counts the 2×2 arrays that are pure tensors.
Think of a column of numbers as a vector, and a row of numbers as an instrument that reads it: a row a = (a1, …, an) applied to a column c gives the single number a1c1 + … + ancn. Rows and columns are different kinds of object. A column says where something is; a row says what you read off. The set of all instruments on a space X is the dual space X′, and it has the same size as X.
Theorem 1. Write x = c1e1 + … + cnen. By linearity, l(x) = c1l(e1) + … + cnl(en). Conversely any choice of aj gives a linear function. The dual basis. A linear function is determined by its values on a basis, so there is exactly one λi with λi(ej) = δij. If R is the matrix whose rows are the λi and P has the ej as columns, then (RP)ij = λi(ej) = δij, so R = P-1. Change of basis. c = Pc′, so a·c = (aP)·c′, which is a′·c′ with a′ = aP.
The script checks, for all 496 invertible 2×2 integer matrices with entries −2..2, that row i of P-1 applied to column j of P is δij, and, as a control built to fail, that the columns of P-1 are not the dual basis in general. The column and row transformation rules are the reason this chapter exists: vectors change by P-1, functionals by P, and in section 5 forms change by PT(·)P, a third rule. Lean: dual_basis_apply is Mathlib’s Basis.toDual_apply; not yet compiled.
Pick a subspace Y of X (say, a plane in space). Some instruments read zero on every vector of Y. Those instruments form a subspace of X′ called the annihilator Y⊥. The bigger Y is, the fewer instruments kill all of it, and the count is exact: what Y uses up of the dimension, Y⊥ keeps.
Theorem 4. A functional l in Y⊥ gives a well defined function L{x} = l(x) on the quotient X/Y, because l kills Y. Conversely every linear function L on X/Y defines such an l. These two assignments are inverse and linear, so Y⊥ ≅ (X/Y)′, and by Theorem 2 and dim X/Y = dim X − dim Y (Chapter 4) the dimensions are as stated. Theorem 5. Every y in Y is killed by Y⊥, so Y ⊆ (Y⊥)⊥. Applying Theorem 4 twice gives dim (Y⊥)⊥ = dim X − (dim X − dim Y) = dim Y. A subspace inside a subspace of the same dimension is equal to it.
The script checks Theorems 4 and 5 in Q3 for every one of the 40 distinct subspaces spanned by vectors with entries −1, 0, 1 (by dimension: 1, 13, 25, 1 for dimensions 0, 1, 2, 3), with the annihilator computed as a null space in exact fractions. The control is an off-by-one version of Theorem 4 (dim Y + dim Y⊥ = 4), false for all 40. For the matrix whose columns span Y, Y⊥ is the set of row vectors l with lA = 0, so Theorem 4 is rank–nullity again, seen from the left. Lean: annihilator_dim and annihilator_annihilator are Mathlib’s Subspace.finrank_add_finrank_dualAnnihilator_eq and dualAnnihilator_dualCoannihilator_eq; not yet compiled. Theorem 6 (annihilator of a set) is not stated here.
A map T carries vectors forward, from X to U. An instrument l on U can then be pulled back to X by first applying T and then reading with l. That pullback is the dual map, written T′ : U′ → X′. It goes the other way. In coordinates it is the transpose, which is why the transpose of a matrix keeps turning up when a matrix is moved from one side of a pairing to the other.
(T′λi)(ej) = λi(Tej) = λi(Σk Mkjfk) = Mij. A functional on X is determined by its values on the ej, so T′λi = Σj Mijμj with μj the dual basis of X′. So the coefficient of μj in T′λi is Mij, which says the matrix of T′ (columns are the images of the λi) has entry (j, i) equal to Mij: it is MT.
The script checks <l, Ax> = <ATl, x> on 500 random integer cases of sizes 1 to 3, and, on 300 cases of 2×2 maps in non-standard bases (columns of P and R), that entry (i, j) of R-1MP is the value of the i-th dual basis vector of U applied to M times the j-th basis vector of X. In Chapter 8 the transpose appears as (Ax, v) = (x, ATv); that identity uses an inner product to identify X with X′. Without one, the transpose lives on the duals, and this section is the form that does not need the identification. Lean: dualMap_apply is Mathlib’s LinearMap.dualMap_apply; not yet compiled.
You want the integral of a polynomial from n sample values. The evaluation p ↦ p(tj) is a linear function on the space of polynomials of degree less than n. If these n functions are independent they form a basis of the dual, and then every linear function on that space, the integral included, is a combination of them. The weights of the combination are the quadrature weights. Nothing about integrals was used, only that they are linear.
Theorem 7. Let X be the polynomials of degree less than n; dim X = n. Suppose c1l1 + … + cnln = 0 where lj(p) = p(tj). Apply it to qk(t) = ∏j≠k(t − tj), which vanishes at every tj except tk and is non-zero there since the points are distinct: ckqk(tk) = 0, so ck = 0. So the lj are n independent elements of the n-dimensional X′, hence a basis. The integral is a linear function on X, so it is a combination of them. The worked case. 2m1 + m2 = ∫1 = 2 and 2a²m1 = ∫t² = 2/3; solve. For the even powers 2j the rule gives 2m1a2j, the integral 2/(2j+1); with a² = 3/5 and m1 = 5/9 these agree at j = 0, 1, 2 and differ at j = 3.
The script checks the weight formulas for four values of a², the positivity statement against 200 values on both sides of 1/3, Simpson, the 5/9, 8/9, 5/9 rule on t0 to t6 in exact fractions, and the four-node weights on a grid of 39 values of a² and b²; the control is a choice of a² = 1/5, b² = 1/10 where one weight is −4/3. Theorem 7 only promises degree less than n. The extra degree for symmetric nodes is a consequence of the symmetry, and the extra degree at a² = 3/5 is the choice that gives the three-point Gauss–Legendre rule (a standard fact, not from the held text). Lean: simpson_exact_two, simpson_fails_four, gauss3_exact_four and gauss3_fails_six are the rational identities, with the even powers of the nodes written as powers of 3/5; not yet compiled.
A bilinear form B(x, y) takes two vectors and returns a number, and is linear in each. A dot product is one. In a basis, B is a table G of numbers Gij = B(ei, ej), and B(x, y) = cTGd. A matrix of a map and a table of a form look the same on paper, but change differently when you change basis, and that difference is what this section is about.
With x = Pc′ and y = Pd′, B(x, y) = (Pc′)TG(Pd′) = c′T(PTGP)d′. For a map, A acting on c becomes P-1APc′ (the coordinates change by P-1 before and after). 2×2 signature. det(PTGP) = (det P)² det G, so the sign of the determinant of a symmetric 2×2 G is unchanged. If det G > 0, G is definite and its sign is the sign of the values q(x) = B(x, x) at any non-zero x, which does not depend on the basis; if det G < 0 the form takes both signs; if det G = 0 the rank is 1 (or 0) and the sign of the non-zero values is again basis-free. These three cases are the possible signatures.
The script checks, over all 62000 pairs (G symmetric 2×2 with entries −2..2, P invertible with entries −2..2), that the signature of PTGP equals that of G and that PTGP is symmetric. The control is the trace: for G = I and P = diag(2, 1) the trace of PTGP is 5, not 2, so it is not a congruence invariant. A second check shows that the trace of a map does survive P-1AP. In Chapter 8 the quadratic form q(x) = xTGx was studied with an orthonormal change of basis, for which P-1 = PT, and the two rules coincide; that is why the distinction did not show. Lean: congruence_not_trace is the control as matrices over ℚ; the likeliest statement in the file to need a fix to its proof; not yet compiled.
Take a column x of length m and a column y of length n. The array with entries xiyj is an m×n table built from them, written x ⊗ y. Not every m×n table can be built this way: the tables that can are the pure tensors. Sums of pure tensors fill out the whole space of tables, of dimension mn. The Kronecker product A ⊗ B of two matrices does to such tables what A does to the first factor and B to the second.
(A ⊗ B)(x ⊗ y) = Ax ⊗ By, since (A ⊗ B)(x ⊗ y)(i,k) = Σj,l AijBklxjyl = (Ax)i(By)k; pure tensors span, so (A ⊗ B)(C ⊗ D) = AC ⊗ BD. Write A ⊗ B = (A ⊗ In)(Im ⊗ B). The first factor is block diagonal after reordering, with n copies of A, so its determinant is det(A)n; the second has m copies of B. Pure tensors. If the array T has det 0 and is not zero, pick a non-zero entry Trc; then Tij = (Tic/Trc) Trj, which is the product of the column (Tic/Trc)i and the row (Trj)j. Conversely x1y1x2y2 − x1y2x2y1 = 0.
The script checks (A ⊗ B)(C ⊗ D) = AC ⊗ BD and det(A ⊗ B) = det(A)3 det(B)2 on 200 random pairs with A, C 2×2 and B, D 3×3, and counts the arrays: 129 of the 625 2×2 arrays with entries −2..2 factor into a column and a row (the script checks the factorization of every one, the zero array included), and the other 496 do not. This is the Kronecker product, a concrete model of the tensor product; the construction by a universal property is not given here. Lean: kronecker_det is Mathlib’s Matrix.det_kronecker; not yet compiled.
Infinite-dimensional spaces and topological duals (Lax Chapter 14); the proofs that the double dual is naturally equal to the space (only the statement is given); Theorem 6; Sylvester’s law of inertia in dimension greater than 2 (checked for 2×2 only, stated for general n); Hermitian forms; symmetric and alternating tensors and the exterior algebra; the tensor product defined by a universal property; and any use of the dual in the nonlinear half of the book. Lean states none of the two-step arguments (the quotient isomorphism, the independence of evaluation functionals), only the Mathlib theorems and the rational identities listed in the header of Duality.lean, and the file has not been compiled.