An anisotropic orthogonal basis of a nondegenerate quadratic form

Over a field in which 2 is invertible, every symmetric bilinear form on a finite-dimensional space admits an orthogonal basis (LinearMap.BilinForm.exists_orthogonal_basis). This file records the refinement that nondegeneracy adds: no member of such a basis is isotropic. Indeed a basis vector orthogonal to all the others and to itself is orthogonal to everything, so it lies in the radical; nondegeneracy makes it zero, which a basis vector is not.

The refinement is what turns an orthogonal basis into a usable one: the volume element v₁ ⋯ vₙ of an orthogonal family in a Clifford algebra squares to the scalar (-1) ^ (n.choose 2) ∏ᵢ Q vᵢ (CliffordAlgebra.prod_map_ι_sq_scalar), which is invertible exactly when no Q vᵢ vanishes. The second statement below packages the basis as the spanning list of pairwise orthogonal vectors that the Clifford-algebra API asks for.

Main results

• QuadraticMap.Nondegenerate.exists_orthogonal_basis: a nondegenerate quadratic form on a finite-dimensional space has an orthogonal basis none of whose members is isotropic.
• QuadraticMap.Nondegenerate.exists_list_pairwise_isOrtho: the same basis read as a spanning list of pairwise orthogonal, non-isotropic vectors whose length is the dimension.
• QuadraticMap.nondegenerate_and_length_eq_finrank_of_pairwise_isOrtho: conversely, a spanning list of pairwise orthogonal, non-isotropic vectors is a basis, so the form is nondegenerate and the list has the length of the dimension.

theorem QuadraticMap.Nondegenerate.exists_orthogonal_basis {F : Type u_1} {V : Type u_2} [Field F] [AddCommGroup V] [Module F V] {Q : QuadraticForm F V} [Invertible 2] [FiniteDimensional F V] (hQ : Nondegenerate) : ∃ (b : Module.Basis (Fin (Module.finrank F V)) F V), (∀ (i j : Fin (Module.finrank F V)), i ≠ j → IsOrtho Q (b i) (b j)) ∧ ∀ (i : Fin (Module.finrank F V)), Q (b i) ≠ 0

A nondegenerate quadratic form has an anisotropic orthogonal basis. Mathlib's LinearMap.BilinForm.exists_orthogonal_basis supplies the orthogonality, and LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft rules out an isotropic member: such a member would be orthogonal to the whole space.

theorem QuadraticMap.Nondegenerate.exists_list_pairwise_isOrtho {F : Type u_1} {V : Type u_2} [Field F] [AddCommGroup V] [Module F V] {Q : QuadraticForm F V} [Invertible 2] [FiniteDimensional F V] (hQ : Nondegenerate) : ∃ (l : List V), List.Pairwise (IsOrtho Q) l ∧ l.length = Module.finrank F V ∧ Submodule.span F {x : V | x ∈ l} = ⊤ ∧ ∀ v ∈ l, Q v ≠ 0

A nondegenerate quadratic form has an anisotropic orthogonal spanning list. This is QuadraticMap.Nondegenerate.exists_orthogonal_basis read as a list, the shape in which the Clifford volume element of CliffordAlgebra.prod_map_ι_sq_scalar consumes an orthogonal family.

theorem QuadraticMap.nondegenerate_and_length_eq_finrank_of_pairwise_isOrtho {F : Type u_1} {V : Type u_2} [Field F] [AddCommGroup V] [Module F V] {Q : QuadraticForm F V} [NeZero 2] {l : List V} (hl : List.Pairwise (IsOrtho Q) l) (hspan : Submodule.span F {x : V | x ∈ l} = ⊤) (hQl : ∀ v ∈ l, Q v ≠ 0) : Nondegenerate ∧ l.length = Module.finrank F V

An anisotropic orthogonal spanning list is a basis, the converse of QuadraticMap.Nondegenerate.exists_list_pairwise_isOrtho: the form is nondegenerate and the list has the length of the dimension. No finiteness is assumed; the list itself makes the space finite-dimensional.