Exterior powers of a system of linear forms

For p linear forms l 0, …, l (p - 1) on R^ι, the wedge l 0 ∧ ⋯ ∧ l (p - 1) is a linear form on ⋀^p R^ι. Here the exterior power is read in Plücker coordinates, as the space Set.powersetCard ι p → R of TauCeti.plucker, so the wedge is the linear form whose coefficient at a p-subset s is the Plücker coordinate at s of the rows of coefficients of the l a. On the Plücker vector of p vectors it is the determinant of the matrix of values, Laplace's identity, which is the Cauchy–Binet formula TauCeti.det_mul_transpose_eq_sum_plucker_mul.

A family of forms indexed by a linearly ordered type κ gives a family of wedges indexed by the p-subsets of κ. Biorthogonality passes to the wedges: if l i (y j) = δ i j, then the wedge of the forms indexed by T takes the value δ T T' on the Plücker vector of the vectors indexed by T'. Over a field this shows that the wedges of linearly independent forms are linearly independent. The Plücker vectors of the p-subfamilies of a linearly independent family of vectors are independent too, by Mathlib's exteriorPower.ιMulti_family_linearIndependent_field.

For a basis x 0, …, x (N - 1) of K^ι and k + p = N, the span TauCeti.wedgeSpan k p x of the Plücker vectors of the p-subfamilies of x that meet the first k indices depends only on the span of x 0, …, x (k - 1), and determines it. It is the kernel of the wedge of the last p coordinate forms of the basis, a hyperplane that misses the Plücker vector of the top block x k, …, x (N - 1), indexed by TauCeti.topBlock.

These are the exterior powers of a system of forms on which Schmidt's Subspace Theorem runs its argument in ⋀^p: an approximation domain of the forms l gives one of the wedges, and the subspace found in ⋀^p is converted back to a subspace of K^ι through wedgeSpan.

Main definitions

• TauCeti.wedgeForm l: the wedge of p linear forms, a linear form on Plücker coordinates.
• TauCeti.wedgeForms l p: the wedges of a family of forms, indexed by the p-subsets.
• TauCeti.wedgeSpan k p x: the span of the Plücker vectors of the p-subfamilies of x that meet the first k indices.

Main results

• TauCeti.wedgeForm_plucker: Laplace's identity (l 0 ∧ ⋯ ∧ l (p - 1)) (y 0 ∧ ⋯ ∧ y (p - 1)) = det (l a (y b)).
• TauCeti.wedgeForms_plucker_comp_eq_ite: biorthogonality passes to the wedges.
• TauCeti.linearIndependent_wedgeForms and TauCeti.linearIndependent_plucker_comp: the wedges of independent forms, and of independent vectors, are independent.
• TauCeti.mem_span_iff_forall_plucker_mem_wedgeSpan and TauCeti.wedgeSpan_eq_wedgeSpan_iff: the span of the wedges meeting the first k indices determines, and is determined by, the span of the first k vectors.
• TauCeti.wedgeSpan_eq_ker, TauCeti.plucker_topBlock_notMem_wedgeSpan and TauCeti.finrank_wedgeSpan_add_one: it is the kernel of the wedge of the last p coordinate forms, a hyperplane missing the wedge of the top block.

Implementation notes

The exterior power is read in coordinates because the geometry of numbers downstream works with forms on a coordinate space κ → K; Mathlib's pairing of ⋀[R]^p M with ⋀[R]^p (Dual R M) enters only through the Cauchy–Binet formula. The determinant of the system of wedges (the Sylvester–Franke theorem) is not needed: independence comes from a biorthogonal family. The description of wedgeSpan uses no pairing between ⋀^p and ⋀^k either: if a coordinate form f j₀ with j₀ ≥ k does not vanish on u, putting u in place of x j₀ in the top block gives a wedge on which the kernel form takes the value f j₀ u, by Cramer's rule.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), 7.5.2, (7.16), 7.5.30 and Lemma 7.5.33.

The definitions, statements and proofs follow Ralf Stephan's DiophantineApproximation/WedgeForm.lean in rwst/Subspace-Theorems, commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338 (Apache 2.0), restated for Tau Ceti's TauCeti.plucker, over a commutative ring where the argument allows and for forms and vectors indexed by an arbitrary linearly ordered type.

The wedge of p forms

noncomputable def TauCeti.wedgeForm {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] (l : Fin p → Module.Dual R (ι → R)) : Module.Dual R (↑(Set.powersetCard ι p) → R)

The wedge of p linear forms l 0 ∧ ⋯ ∧ l (p - 1), as a linear form on the Plücker coordinates powersetCard ι p → R: its coefficient at a p-subset s is the Plücker coordinate at s of the rows of coefficients l a (Pi.single j 1) of the forms.

theorem TauCeti.wedgeForm_apply {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] (l : Fin p → Module.Dual R (ι → R)) (z : ↑(Set.powersetCard ι p) → R) : (wedgeForm l) z = ∑ s : ↑(Set.powersetCard ι p), plucker (fun (a : Fin p) (j : ι) => (l a) (Pi.single j 1)) s * z s

The wedge of p forms evaluated on a vector of Plücker coordinates.

@[simp]

theorem TauCeti.wedgeForm_plucker {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] (l : Fin p → Module.Dual R (ι → R)) (y : Fin p → ι → R) : (wedgeForm l) (plucker y) = (Matrix.of fun (a b : Fin p) => (l a) (y b)).det

Laplace's identity (Bombieri–Gubler (7.16)): the wedge of p forms takes the value det (l a (y b)) on the Plücker vector of p vectors y.

The wedges of a family of forms

noncomputable def TauCeti.wedgeForms {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [LinearOrder ι] [LinearOrder κ] [Fintype ι] (l : κ → Module.Dual R (ι → R)) (p : ℕ) : ↑(Set.powersetCard κ p) → Module.Dual R (↑(Set.powersetCard ι p) → R)

The wedges of a family of forms: for each p-subset T of the index type κ, the wedge of the forms indexed by T, taken in increasing order.

theorem TauCeti.wedgeForms_apply {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [LinearOrder ι] [LinearOrder κ] [Fintype ι] (l : κ → Module.Dual R (ι → R)) (p : ℕ) (T : ↑(Set.powersetCard κ p)) : wedgeForms l p T = wedgeForm (l ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm T))

The wedge of the forms indexed by T is the wedge of the subfamily l ∘ T, with T enumerated in increasing order.

@[simp]

theorem TauCeti.wedgeForms_plucker {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [LinearOrder ι] [LinearOrder κ] [Fintype ι] (l : κ → Module.Dual R (ι → R)) (p : ℕ) (T : ↑(Set.powersetCard κ p)) (y : Fin p → ι → R) : (wedgeForms l p T) (plucker y) = (Matrix.of fun (a b : Fin p) => (l ((Set.powersetCard.ofFinEmbEquiv.symm T) a)) (y b)).det

Laplace's identity for the wedges of a family of forms.

theorem TauCeti.wedgeForms_plucker_comp_eq_ite {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [LinearOrder ι] [LinearOrder κ] [Fintype ι] {l : κ → Module.Dual R (ι → R)} {y : κ → ι → R} (h : ∀ (i j : κ), (l i) (y j) = if i = j then 1 else 0) (p : ℕ) (T T' : ↑(Set.powersetCard κ p)) : (wedgeForms l p T) (plucker (y ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm T'))) = if T = T' then 1 else 0

Biorthogonality passes to the wedges: if l i (y j) = δ i j, then the wedge of the forms indexed by T takes the value δ T T' on the Plücker vector of the vectors indexed by T'.

theorem TauCeti.linearIndependent_wedgeForms {ι : Type u_2} {κ : Type u_3} [LinearOrder ι] [LinearOrder κ] [Fintype ι] {K : Type u_4} [Field K] {l : κ → Module.Dual K (ι → K)} (hl : LinearIndependent K l) (p : ℕ) : LinearIndependent (ι := ↑(Set.powersetCard κ p)) K (wedgeForms l p)

The wedges of linearly independent forms are linearly independent (Bombieri–Gubler 7.5.30).

theorem TauCeti.linearIndependent_plucker_comp {ι : Type u_2} {κ : Type u_3} [LinearOrder ι] [LinearOrder κ] [Finite ι] {K : Type u_4} [Field K] {x : κ → ι → K} (hx : LinearIndependent K x) (p : ℕ) : LinearIndependent K fun (J : ↑(Set.powersetCard κ p)) => plucker (x ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm J))

The wedges of linearly independent vectors are linearly independent: for a linearly independent family x, the Plücker vectors of its p-subfamilies.

The wedges of a basis that meet the first k indices

noncomputable def TauCeti.wedgeSpan {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {N : ℕ} (k p : ℕ) (x : Fin N → ι → R) : Submodule R (↑(Set.powersetCard ι p) → R)

The span of the wedges that meet the first k indices (Bombieri–Gubler, Lemma 7.5.33): for a family x of N vectors, the span of the Plücker vectors of the p-subfamilies x ∘ J whose index set J contains an index below k.

theorem TauCeti.plucker_comp_mem_wedgeSpan {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {p N k : ℕ} (x : Fin N → ι → R) {J : ↑(Set.powersetCard (Fin N) p)} (hJ : ∃ j ∈ J, ↑j < k) : plucker (x ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm J)) ∈ wedgeSpan k p x

The Plücker vector of a p-subfamily meeting the first k indices lies in wedgeSpan.

theorem TauCeti.wedgeSpan_le_iff {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {p N k : ℕ} {x : Fin N → ι → R} {U : Submodule R (↑(Set.powersetCard ι p) → R)} : wedgeSpan k p x ≤ U ↔ ∀ (J : ↑(Set.powersetCard (Fin N) p)), (∃ j ∈ J, ↑j < k) → plucker (x ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm J)) ∈ U

wedgeSpan is contained in a submodule exactly when every Plücker vector of a p-subfamily meeting the first k indices is.

theorem TauCeti.wedgeSpan_eq_ker {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] {K : Type u_4} [Field K] {x : Fin (Fintype.card ι) → ι → K} {f : Fin (Fintype.card ι) → Module.Dual K (ι → K)} (hf : ∀ (i j : Fin (Fintype.card ι)), (f i) (x j) = if i = j then 1 else 0) {k : ℕ} (h : k + p = Fintype.card ι) : wedgeSpan k p x = LinearMap.ker (wedgeForms f p (topBlock h))

The span of the wedges meeting the first k indices is a kernel: for a basis x with biorthogonal forms f, it is the kernel of the wedge of the last p forms f k, …, f (N - 1). It is a hyperplane by finrank_wedgeSpan_add_one.

theorem TauCeti.mem_span_iff_forall_plucker_mem_wedgeSpan {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] {K : Type u_4} [Field K] {x : Fin (Fintype.card ι) → ι → K} (hx : LinearIndependent K x) {k : ℕ} (h : k + p = Fintype.card ι) (u : ι → K) : u ∈ Submodule.span K (x '' {j : Fin (Fintype.card ι) | ↑j < k}) ↔ ∀ (ω : Fin p → ι → K) (b : Fin p), ω b = u → plucker ω ∈ wedgeSpan k p x

The wedges meeting the first k indices determine the span of the first k vectors (Bombieri–Gubler, Lemma 7.5.33): for a basis x and k + p = #ι, a vector lies in the span of x 0, …, x (k - 1) exactly when the Plücker vector of every family of p vectors containing it lies in wedgeSpan k p x.

theorem TauCeti.wedgeSpan_eq_wedgeSpan_iff {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] {K : Type u_4} [Field K] {x x' : Fin (Fintype.card ι) → ι → K} (hx : LinearIndependent K x) (hx' : LinearIndependent K x') {k : ℕ} (h : k + p = Fintype.card ι) : wedgeSpan k p x = wedgeSpan k p x' ↔ Submodule.span K (x '' {j : Fin (Fintype.card ι) | ↑j < k}) = Submodule.span K (x' '' {j : Fin (Fintype.card ι) | ↑j < k})

The span of the wedges meeting the first k indices depends only on the span of the first k vectors, and determines it (Bombieri–Gubler, Lemma 7.5.33): for two bases x and x' and k + p = #ι, the two wedgeSpans agree exactly when x and x' have the same first k-span.

theorem TauCeti.plucker_topBlock_notMem_wedgeSpan {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] {K : Type u_4} [Field K] {x : Fin (Fintype.card ι) → ι → K} (hx : LinearIndependent K x) {k : ℕ} (h : k + p = Fintype.card ι) : plucker (x ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm (topBlock h))) ∉ wedgeSpan k p x

The wedge of the top block is not in the span of the others: in particular wedgeSpan is a proper subspace.

theorem TauCeti.finrank_wedgeSpan_add_one {ι : Type u_2} [LinearOrder ι] {p : ℕ} [Fintype ι] {K : Type u_4} [Field K] {x : Fin (Fintype.card ι) → ι → K} (hx : LinearIndependent K x) {k : ℕ} (h : k + p = Fintype.card ι) : Module.finrank K ↥(wedgeSpan k p x) + 1 = Fintype.card ↑(Set.powersetCard ι p)

The span of the wedges meeting the first k indices has codimension one.

Examples