22 Grassmann–Cayley meet and projective duality
This chapter defines the meet, the operation of the Grassmann–Cayley algebra dual to the join, and proves that for \(d = 3\) the meet of two planes is a scalar multiple of the join of two points of their line of intersection. Katoh and Tanigawa use the join and not the meet. For the Grassmann–Cayley algebra they refer to Barnabei, Brini and Rota [ BBR85 ] and to White [ Whi94 ] , among others [ KT11 , § 2.1 ] . They define the extensor of an affine subspace through points that span it, and in a nonparallel panel-hinge framework the hinge of an edge \(uv\) is the intersection \(\Pi (u) \cap \Pi (v)\) of the panels of its ends [ KT11 , § 5.1 ] . The formalization records such a hinge by the meet of the two panels (definition 23.1). For \(d = 3\), lemma 22.16 shows that this meet agrees with the join of two points of the hinge up to a scalar. This is what lets the proof of KT Lemma 6.10, which spans \(\bigwedge ^2 {\mathbb {R}}^4\) by joins of points in KT eq. (6.45) [ KT11 , p. 691 ] , apply to hinges given by panels.
The chapter builds only on section 18.2: the exterior algebra of \(V = K^{d+1}\), its extensors, and the join. As there, \(K\) is an arbitrary field. The constructions use the standard basis of \(V\), through a volume form and a coordinate pairing, and no order on \(K\) or hypothesis on its characteristic. We write \(\vee \) for the product of an exterior algebra, as in definition 18.4, and \(\wedge \) for the meet, as Barnabei, Brini and Rota and White do.
The first subsection defines the volume form (definition 22.1). It then defines the duality between the exterior powers of \(V\) and of its dual space (definition 22.3). The pairing \((X, Y) \mapsto \operatorname {vol}(X \vee Y)\) is nondegenerate, and it gives the complement isomorphism \(*\) (definition 22.5), whose defining property is lemma 22.6. The meet is then \(A \wedge B = *({*A} \vee {*B})\) (definition 22.7), and the meet of two hyperplanes is an extensor of their intersection (lemma 22.9). The second subsection takes \(d = 3\) and proves the agreement of meet and join (lemma 22.16). It ends with the converse fact that a nonzero \(2\)-extensor determines its plane (lemma 22.18). The remark at the start of the second subsection (remark 22.11) says which of these results the formal proof of KT Theorem 5.5 does not use, and what it uses instead.
22.1 The complement isomorphism and the meet
Let \(V = K^{d+1}\), with standard basis \(e_1, \dots , e_{d+1}\). For a set \(S = \{ s_1 {\lt} \cdots {\lt} s_i\} \subseteq \{ 1, \dots , d+1\} \) we write \(e_S = e_{s_1} \vee \cdots \vee e_{s_i}\). The products \(e_S\) over the \(i\)-element sets \(S\) form a basis of \(\bigwedge ^i V\) (lemma 18.6), and \(X_S\) denotes the coordinate of \(X \in \bigwedge ^i V\) at \(e_S\). For \(i = d+1\) there is one such product.
The volume form \(\operatorname {vol} \colon \bigwedge ^{d+1} V \to K\) is the linear isomorphism with \(\operatorname {vol}(e_1 \vee \cdots \vee e_{d+1}) = 1\).
The space \(\bigwedge ^{d+1} V\) has dimension \(\binom {d+1}{d+1} = 1\), with basis \(e_1 \vee \cdots \vee e_{d+1}\). The volume form takes an element to its coordinate in this basis.
The second pin is the same isomorphism for \(R^n\) over a commutative ring \(R\), and the first is its case \(R = K\), \(n = d+1\). As in section 19, the formalization writes \(d = k + 1\), so that \(V = K^{k+2}\).
By lemma 18.6, \(\operatorname {vol}(v_1 \vee \cdots \vee v_{d+1})\) is the determinant of the matrix with rows \(v_1, \dots , v_{d+1}\).
The exterior powers of \(V\) and of its dual space \(V^*\) are dual to each other through determinants.
Let \(j \ge 0\). The linear map \(\bigwedge ^{j} V^{*} \to (\bigwedge ^{j} V)^{*}\) that sends \(\varphi _1 \vee \cdots \vee \varphi _j\) to the linear form
is an isomorphism.
Let \(\varphi _1, \dots , \varphi _{d+1}\) be the basis of \(V^*\) dual to \(e_1, \dots , e_{d+1}\), and let \(\varphi _S\) be the products of its elements, as for \(e_S\). For \(j\)-element sets \(S\) and \(T\), the matrix \((\varphi _{s_a}(e_{t_b}))\) is the identity if \(S = T\), and it has a zero row otherwise. So the map sends \(\varphi _S\) to the linear form \(X \mapsto X_S\). It takes the basis \((\varphi _S)\) of \(\bigwedge ^j V^*\) to the basis of \((\bigwedge ^j V)^*\) dual to \((e_S)\), and is therefore an isomorphism.
The second pin is the isomorphism for a finite free module with an ordered basis over a commutative ring, built from that basis as in the proof, and the first is its case \(V = K^{d+1}\) with the standard basis.
The complement isomorphism compares two pairings. For each \(i\), the coordinate pairing on \(\bigwedge ^i V\) is the bilinear form \(\langle X, Y \rangle = \sum _S X_S Y_S\), for which the basis \((e_S)\) is orthonormal. On \(V = \bigwedge ^1 V\) it is the dot product. It identifies \(\bigwedge ^i V\) with its dual, as \(Z \mapsto \langle Z, \cdot \rangle \) is an isomorphism \(\bigwedge ^i V \to (\bigwedge ^i V)^*\). The second pairing uses the volume form. For \(0 \le j \le d+1\), the join of \(X \in \bigwedge ^j V\) and \(Y \in \bigwedge ^{d+1-j} V\) lies in \(\bigwedge ^{d+1} V\), and the wedge pairing of \(X\) and \(Y\) is \(\operatorname {vol}(X \vee Y)\).
Let \(0 \le j \le d+1\). The wedge pairing \(\bigwedge ^{j} V \times \bigwedge ^{d+1-j} V \to K\) is nondegenerate, so \(X \mapsto \operatorname {vol}(X \vee \cdot )\) is an isomorphism \(\bigwedge ^{j} V \to (\bigwedge ^{d+1-j} V)^*\). The complement isomorphism \(* \colon \bigwedge ^{j} V \to \bigwedge ^{d+1-j} V\) is this isomorphism followed by the inverse of the coordinate identification of \(\bigwedge ^{d+1-j} V\) with its dual.
Let \(S\) be a \(j\)-element set and \(T\) a \((d+1-j)\)-element set in \(\{ 1, \dots , d+1\} \). The join \(e_S \vee e_T\) is the extensor of the family that lists \(e_s\) for \(s \in S\) and then \(e_t\) for \(t \in T\) (definition 18.4). If \(S\) and \(T\) meet, this family repeats a vector, and \(e_S \vee e_T = 0\) (the remark after definition 18.3). Since \(|S| + |T| = d+1\), the sets \(S\) and \(T\) are disjoint exactly when \(T\) is the complement \(S^c\) of \(S\). In that case the family lists each standard basis vector once. It is linearly independent, so \(e_S \vee e_{S^c} \neq 0\), and \(\varepsilon _S = \operatorname {vol}(e_S \vee e_{S^c}) \neq 0\), as the volume form is injective. In the bases \((e_S)\) and \((e_T)\), the matrix of the wedge pairing therefore has exactly one nonzero entry in each row and each column: \(\varepsilon _S\), in row \(S\) and column \(S^c\).
Hence \(X \mapsto \operatorname {vol}(X \vee \cdot )\) is injective. If \(\operatorname {vol}(X \vee Y) = 0\) for every \(Y\), then \(Y = e_{S^c}\) gives \(\varepsilon _S X_S = 0\), so \(X_S = 0\) for every \(S\), and \(X = 0\). The spaces \(\bigwedge ^{j} V\) and \((\bigwedge ^{d+1-j} V)^*\) both have dimension \(\binom {d+1}{j} = \binom {d+1}{d+1-j}\), so this injective linear map is an isomorphism. The coordinate identification of \(\bigwedge ^{d+1-j} V\) with its dual is an isomorphism because the basis \((e_T)\) is orthonormal, and \(*\) is the first isomorphism followed by the inverse of the second.
In fact \(\varepsilon _S = \pm 1\) is the sign of the permutation that lists the elements of \(S\) and then those of \(S^c\), each in increasing order. The argument needs only \(\varepsilon _S \neq 0\).
Let \(0 \le j \le d+1\), \(X \in \bigwedge ^{j} V\) and \(Y \in \bigwedge ^{d+1-j} V\). Then
The coordinate identification sends \(*X\) to the linear form \(\langle *X, \cdot \rangle \), which is \(\operatorname {vol}(X \vee \cdot )\) by definition 22.5.
Taking \(X = e_S\) and \(Y = e_T\) shows that \(\langle *e_S, e_T \rangle \) is \(\varepsilon _S\) if \(T = S^c\) and \(0\) otherwise. So \(*e_S = \varepsilon _S\, e_{S^c}\) (complementIso_exteriorPower_basis_eq_smul_compl), and \(*\) is the Hodge star operator of the standard basis, which Barnabei, Brini and Rota use to state the duality between join and meet [ BBR85 , p. 146 ] .
The meet is the join transported by the complement isomorphism.
Let \(a, b \ge 0\) with \(a + b \le d+1\), and let \(A \in \bigwedge ^{d+1-a} V\) and \(B \in \bigwedge ^{d+1-b} V\). The meet of \(A\) and \(B\) is
where \({*A} \in \bigwedge ^{a} V\) and \({*B} \in \bigwedge ^{b} V\), so that their join lies in \(\bigwedge ^{a+b} V\).
The formalization proves no property of the meet itself. It proves the formula for \(*e_S\) and the transformation law below, and the case of two hyperplanes in the form \(*(n_A \vee n_B)\) (lemma 22.9), which is how the later chapters use the meet (definition 23.1). The statements below for a general subspace \(U\) and for general subspaces \(X\) and \(Y\) are not formalized.
The meet of extensors of two subspaces is an extensor of their intersection. Let \(U\) be a subspace of \(V\), and let \(U^\perp \) be its orthogonal complement for the dot product. The complement isomorphism sends a nonzero extensor of \(U\) to a nonzero extensor of \(U^\perp \). For \(U = U_S\), the span of the \(e_i\) with \(i \in S\), this is \(*e_S = \varepsilon _S\, e_{S^c}\). In general, write \(U = g(U_S)\) for a linear automorphism \(g\) of \(V\), and let \(h\) be its inverse transpose, so that \(h(x) \cdot g(y) = x \cdot y\). The extensors of \(U\) are the multiples of \(g(e_{s_1}) \vee \cdots \vee g(e_{s_i})\), and
where \(S^c = \{ t_1 {\lt} \cdots {\lt} t_{d+1-i}\} \) (complementIso_map_contragredient_eq). The right side is a nonzero extensor of \(h(U_{S^c})\). This is \(U^\perp \), since \(h(e_t) \cdot g(e_s) = e_t \cdot e_s = 0\) for \(t \in S^c\) and \(s \in S\), and the two spaces have the same dimension.
Now let \(A\) and \(B\) be nonzero extensors of subspaces \(X\) and \(Y\) of \(V\) with \(X + Y = V\). Then \({*A}\) and \({*B}\) are nonzero extensors of \(X^\perp \) and \(Y^\perp \), and \(X^\perp \cap Y^\perp = (X + Y)^\perp = 0\). So \({*A} \vee {*B}\) is a nonzero extensor of \(X^\perp + Y^\perp = (X \cap Y)^\perp \) (the remark after definition 18.4), and \(A \wedge B\) is a nonzero extensor of \(X \cap Y\). Barnabei, Brini and Rota define the meet by a sum over the splits of \(A\) and prove this property for it [ BBR85 , § 4, Proposition 4.3 ] . White gives the same definition as a sum over shuffles [ Whi94 , § 4 ] .
The later chapters use the case of two distinct hyperplanes \(H_A\) and \(H_B\), where \(a = b = 1\). Then \(n_A = {*A}\) spans \(H_A^\perp \), so it is a normal of \(H_A\), and likewise \(n_B = {*B}\) for \(H_B\). The meet \(A \wedge B = *(n_A \vee n_B)\) is a nonzero extensor of \(H_A \cap H_B\). The next lemma states this for every \(d\), in the form the formalization proves, and lemma 22.16 below proves it for \(d = 3\) by a count of dimensions.
Let \(d \ge 1\), let \(n_1, n_2 \in V\), and let \(W\) be a \((d-1)\)-dimensional subspace of \(V\) whose vectors are orthogonal to \(n_1\) and \(n_2\). Then \(*(n_1 \vee n_2)\) lies in the image of the map \(\bigwedge ^{d-1} W \to \bigwedge ^{d-1} V\) induced by the inclusion of \(W\) in \(V\). If moreover \(n_1\) and \(n_2\) are linearly independent, and \(p_1, \dots , p_{d-1} \in V\) are linearly independent and orthogonal to \(n_1\) and \(n_2\), then \(p_1 \vee \cdots \vee p_{d-1} = c\, {*(n_1 \vee n_2)}\) for some \(c \in K\).
If \(n_1\) and \(n_2\) are linearly dependent, then \(n_1 \vee n_2 = 0\) (the remark after definition 18.3), and the first statement holds as \(*0 = 0\). Otherwise there is a linear automorphism \(g\) of \(V\) with \(g(e_1) = n_1\) and \(g(e_2) = n_2\). Let \(h\) be its inverse transpose. By the formula displayed after definition 22.7, with \(S = \{ 1, 2\} \), which follows from lemma 22.6,
For \(t \ge 3\) and \(i = 1, 2\) we have \(h(e_t) \cdot n_i = h(e_t) \cdot g(e_i) = e_t \cdot e_i = 0\). So the vectors \(h(e_t)\) lie in the orthogonal complement of \(n_1\) and \(n_2\). This complement has dimension \(d - 1\) and contains \(W\), so it is \(W\), and \(*(n_1 \vee n_2)\) is a multiple of a join of \(d - 1\) vectors of \(W\). Hence it lies in the image of \(\bigwedge ^{d-1} W\).
For the second statement, let \(W\) be the orthogonal complement of \(n_1\) and \(n_2\), of dimension \(d - 1\). The space \(\bigwedge ^{d-1} W\) has dimension \(\binom {d-1}{d-1} = 1\), so its image in \(\bigwedge ^{d-1} V\) has dimension at most \(1\). The vectors \(p_i\) lie in \(W\), so their join lies in this image, and it is nonzero, as they are linearly independent. The meet \(*(n_1 \vee n_2)\) lies in the image by the first statement. So it is a multiple \(\mu \, (p_1 \vee \cdots \vee p_{d-1})\), and \(\mu \neq 0\), as \(n_1 \vee n_2 \neq 0\) and \(*\) is an isomorphism. Then \(c = \mu ^{-1}\) will do.
The first pin is the first statement, and the second pin the second.
22.2 Lines in projective three-space
In this subsection \(d = 3\) and \(V = K^4\), except in part (1) of lemma 22.12 and in lemma 22.18, which hold for every \(d\). A point \(p \in K^3\) has the homogeneous coordinate vector \(\bar p = (p, 1) \in K^4\) (definition 18.1). The plane \(\{ x \in K^3 : a \cdot x + a_0 = 0\} \) has the normal \(n = (a, a_0) \in K^4\), and a point \(p\) lies on it exactly when \(\bar p \cdot n = 0\). Let \(L\) be the line in which two nonparallel planes meet, and let \(n_1\) and \(n_2\) be their normals, which are linearly independent. Let
a \(2\)-dimensional subspace that contains \(\bar p\) for every \(p \in L\). The extensor of \(L\) is \(\bar p \vee \bar q\) for distinct points \(p\) and \(q\) of \(L\) (definition 18.8). The meet of the two planes (two panels, in a panel-hinge framework) is a scalar multiple of \(*(n_1 \vee n_2)\), a nonzero extensor of \(W\) by the remarks after definition 22.7 and by lemma 22.9. Lemma 22.16 proves that the two extensors agree up to a scalar, by a count of dimensions in \(\bigwedge ^2 K^4\). It states the agreement in the form that the algebraic induction applies: a linear form on \(\bigwedge ^2 K^4\) that vanishes on the meet vanishes on the join.
Katoh and Tanigawa write the \(2\)-extensor \(C(L)\) supporting a line \(L\) as the join of two points of \(L\) (KT §2.1, p. 651). In the proof of KT Claim 6.12, they use that the join of two points of a line in a panel is such an extensor (KT eq. (6.45), p. 691). The formalization records a hinge by the meet of two panels (definition 23.1), so it compares the meet with the join. Some definitions and lemmas of this chapter concern this comparison in a form that the formal proof of KT Theorem 5.5 (theorem 23.38) does not use. We keep them, and say here what the formal proof does instead.
The line \(\bigwedge ^2 W\). After the proof of lemma 22.16, we identify the line of \(\bigwedge ^2 K^4\) that the proof finds with the image of \(\bigwedge ^2 W\). So the meet of the two planes is an extensor of their line of intersection. The identification uses two facts. The space \(\bigwedge ^2 W\) is a line (lemma 22.14). It embeds in \(\bigwedge ^2 K^4\) (lemma 22.15). The formal proof of lemma 22.16 makes no such identification. There the line is the orthogonal complement of the span of the \(2\)-extensors \(n_i \vee v\), a span of dimension \(5\). The join lies on it, as a determinant of dot products vanishes.
The formal proof of KT Theorem 5.5 uses neither lemma 22.16 nor lemma 22.12. It takes the case \(d = 3\) as a case of KT Lemma 6.13 (remark 23.137). It compares the meet and the join by lemma 22.9, which holds for every \(d\). In that lemma, \(W\) is a subspace of \(K^{d+1}\) of dimension \(d - 1\) whose vectors are orthogonal to \(n_1\) and \(n_2\). The first statement places the meet in the image of \(\bigwedge ^{d-1} W\), by the transformation law of the complement isomorphism (the passage after definition 22.7). The second compares the meet and the join in this image. Its formal proof uses the facts of lemma 22.14 and lemma 22.15 in degree \(d - 1\). The two lemmas state their case \(d = 3\).
The meet and the duality of exterior powers. Katoh and Tanigawa give each panel of a nonparallel framework by a vector \(c(v)\), and each hinge as the intersection of two panels (KT §5.1, p. 668). The formal proof gives each panel by a normal. It gives a hinge by \(*(n_A \vee n_B)\), from the normals \(n_A\) and \(n_B\) of its two panels. It does not form the meet \(A \wedge B\) of definition 22.7, which is \(*(n_A \vee n_B)\) when \(n_A = {*A}\) and \(n_B = {*B}\) (the passage before lemma 22.9). Of definition 22.3, the formal proof uses the map and its determinant formula, but not that the map is an isomorphism. With \(V\) identified with \(V^*\) by the dot product, the formula gives the coordinate pairing of two \(j\)-extensors as a determinant of dot products (the proof of lemma 22.16). The formal proof of the transformation law compares coordinate pairings in this form.
The proof of lemma 22.16 finds a line of \(\bigwedge ^2 K^4\) that contains both extensors, cut out by the coordinate pairing. The first lemma shows that the meet lies on it.
Let \(d \ge 1\) and \(0 \le j \le d+1\), and let \(X \in \bigwedge ^{j} K^{d+1}\) and \(Y \in \bigwedge ^{d+1-j} K^{d+1}\) with \(X \vee Y = 0\). Then \(\langle *X, Y \rangle = 0\).
Let \(n_1, n_2, c \in K^4\), and let \(Y = n_1 \vee c\). Then \((n_1 \vee n_2) \vee Y = 0\) and \(\langle *(n_1 \vee n_2), Y \rangle = 0\).
For part (1), lemma 22.6 gives \(\langle *X, Y \rangle = \operatorname {vol}(X \vee Y) = \operatorname {vol}(0) = 0\). For part (2), \((n_1 \vee n_2) \vee (n_1 \vee c)\) is the extensor of the family \(n_1, n_2, n_1, c\) (definition 18.4). This family repeats \(n_1\), so its extensor is zero (the remark after definition 18.3). The second claim follows by part (1), with \(X = n_1 \vee n_2\) and \(j = 2\).
The same argument applies to \(Y = n_2 \vee c\), as the family \(n_1, n_2, n_2, c\) repeats \(n_2\). So \(*(n_1 \vee n_2)\) is orthogonal to every \(2\)-extensor \(n \vee c\) with \(n \in \{ n_1, n_2\} \).
The first pin is part (1), and the second and third pins are the two claims of part (2). No pin states the case \(Y = n_2 \vee c\). The formal proof of lemma 22.16 obtains it from the first pin, as at the end of the proof above.
Geometrically, the line in the proof below is the image of \(\bigwedge ^2 W\) in \(\bigwedge ^2 K^4\). The next two lemmas give the facts that identify it, which we use after the proof.
Let \(W\) be a \(2\)-dimensional vector space over \(K\). Then \(\dim \bigwedge ^{2} W = \binom {2}{2} = 1\). Consequently, every element of \(\bigwedge ^{2} W\) is a scalar multiple of any nonzero one.
The exterior power \(\bigwedge ^{n} W\) has dimension \(\binom {\dim W}{n}\), which is \(1\) for \(n = \dim W = 2\). A space of dimension \(1\) is spanned by each of its nonzero elements.
Let \(W\) be a subspace of \(K^4\). The linear map \(\bigwedge ^{2} W \to \bigwedge ^{2} K^4\) induced by the inclusion of \(W\) in \(K^4\) is injective.
Extend a basis \(w_1, \dots , w_m\) of \(W\) to a basis of \(K^4\). The map sends the basis of \(\bigwedge ^2 W\) formed by the \(w_a \vee w_b\) with \(a {\lt} b\) to part of the corresponding basis of \(\bigwedge ^2 K^4\), so it is injective.
Let \(n_1, n_2 \in K^4\) be linearly independent, and let \(x, y \in K^4\) satisfy \(x \cdot n_i = y \cdot n_i = 0\) for \(i = 1, 2\). Then \(x \vee y\) is a scalar multiple of \(*(n_1 \vee n_2)\). In particular, every linear form \(r\) on \(\bigwedge ^2 K^4\) with \(r(*(n_1 \vee n_2)) = 0\) satisfies \(r(x \vee y) = 0\).
Let \(\Phi \) be the subspace of \(\bigwedge ^2 K^4\) spanned by the \(2\)-extensors \(n_1 \vee v\) and \(n_2 \vee v\) for \(v \in K^4\), and let
We show that \(\Omega \) has dimension \(1\) and contains both \(x \vee y\) and \(*(n_1 \vee n_2)\).
First, \(\Phi \) has dimension \(5\). For \(n \neq 0\), the map \(v \mapsto n \vee v\) has kernel \(\operatorname {span}\{ n\} \), since \(n \vee v = 0\) exactly when \(n\) and \(v\) are linearly dependent (the remark after definition 18.3). So its image \(n \vee K^4\) has dimension \(3\). The images for \(n_1\) and \(n_2\) meet in the line spanned by \(n_1 \vee n_2\). This line lies in both, as \(n_1 \vee n_2 = n_2 \vee (-n_1)\). Conversely, let \(n_1 \vee v = n_2 \vee w\). The join with \(n_2\) on the left gives \(n_2 \vee n_1 \vee v = n_2 \vee n_2 \vee w = 0\), so \(n_2\), \(n_1\) and \(v\) are linearly dependent. As \(n_1\) and \(n_2\) are independent, \(v = \alpha n_1 + \beta n_2\) for some \(\alpha , \beta \in K\), and \(n_1 \vee v = \beta \, (n_1 \vee n_2)\). Hence \(\dim \Phi = 3 + 3 - 1 = 5\) (finrank_sup_range_wedgeFixedLeft). The coordinate pairing is nondegenerate on the \(6\)-dimensional space \(\bigwedge ^2 K^4\), so \(\dim \Omega = 6 - 5 = 1\).
Next, \(x \vee y \in \Omega \). It suffices to show that \(\langle x \vee y, n_i \vee v \rangle = 0\) for \(i = 1, 2\) and \(v \in K^4\). Identify \(V\) with \(V^*\) by the dot product. Then the coordinate pairing of two \(2\)-extensors is the determinant of definition 22.3 (exteriorPower_basis_toDual_eq_pairingDual_comp_map):
Its first column is zero by hypothesis, so it vanishes (extensor_toDual_extensor_eq_zero_of_perp).
The meet lies in \(\Omega \) as well. By part (2) of lemma 22.12, the pairing \(\langle *(n_1 \vee n_2), n_1 \vee v \rangle \) vanishes for every \(v \in K^4\). The end of the proof of that lemma gives the same for \(n_2 \vee v\).
Finally, \(n_1 \vee n_2 \neq 0\), as \(n_1\) and \(n_2\) are linearly independent, and so \(*(n_1 \vee n_2) \neq 0\), as \(*\) is an isomorphism. So \(*(n_1 \vee n_2)\) spans \(\Omega \), and \(x \vee y = \lambda \, {*(n_1 \vee n_2)}\) for some \(\lambda \in K\). For a linear form \(r\) with \(r(*(n_1 \vee n_2)) = 0\), it follows that \(r(x \vee y) = \lambda \, r(*(n_1 \vee n_2)) = 0\).
The first pin is the first statement, and the second and third are the second statement, with the orthogonality written through the coordinate pairing of \(K^4\) and through the dot product. The formal proof of Case III at \(d = 3\) (lemma 23.195) applies the third, in the step from a join to a line of the proof of lemma 23.191. The general case applies lemma 22.9 instead.
The line \(\Omega \) is the image of \(\bigwedge ^2 W\). The inclusion of \(W\) in \(K^4\) induces an injective map \(\bigwedge ^2 W \to \bigwedge ^2 K^4\) (lemma 22.15). Its image is therefore a line, as \(\bigwedge ^2 W\) is one (lemma 22.14). It is spanned by \(x \vee y\) for any basis \(x, y\) of \(W\), and \(x \vee y\) lies in \(\Omega \) by the proof. So \(*(n_1 \vee n_2)\) is a nonzero extensor of \(W\), and the meet of the two planes is an extensor of their line of intersection. For lines in \(3\)-space this is White’s theorem that the Plücker coordinates of a subspace and its dual Plücker coordinates, computed from hyperplanes that contain it, agree up to a common scalar after a reordering with signs [ Whi94 , § 2 ] . By the formula for \(*e_S\) after lemma 22.6, the complement isomorphism performs the reordering.
Conversely, a nonzero \(2\)-extensor determines the plane spanned by its vectors. This is the case \(j = 2\) of the proposition of Barnabei, Brini and Rota recalled after definition 18.4, here for every \(d\).
Let \(p_0, p_1, p_0', p_1' \in K^{d+1}\) with \(p_0 \vee p_1 = p_0' \vee p_1' \neq 0\). Then \(\operatorname {span}\{ p_0, p_1\} = \operatorname {span}\{ p_0', p_1'\} \).
Let \(x \in K^{d+1}\). The join \(x \vee p_0 \vee p_1\) depends on \(p_0\) and \(p_1\) only through \(p_0 \vee p_1\) (definition 18.4), so \(x \vee p_0 \vee p_1 = x \vee p_0' \vee p_1'\). The vectors \(p_0\) and \(p_1\) are linearly independent, as their join is nonzero, so \(x \vee p_0 \vee p_1 = 0\) exactly when \(x \in \operatorname {span}\{ p_0, p_1\} \) (the remark after definition 18.3). The same holds for \(p_0'\) and \(p_1'\). So the two spans have the same elements.