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.

theorem QuadraticMap.Nondegenerate.exists_orthogonal_basis {F : Type u_1} {V : Type u_2} [Field F] [AddCommGroup V] [Module F V] [Invertible 2] [FiniteDimensional F V] {Q : QuadraticForm 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] [Invertible 2] [FiniteDimensional F V] {Q : QuadraticForm 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.