Connectivity of contiguous orthogonal bases

Any two orthogonal bases of a regular quadratic space of dimension at least three are joined by a chain of contiguous orthogonal bases. In fact, at most three moves suffice: find an anisotropic vector perpendicular both to a vector of the first basis and to a vector of the second, then extend the two orthogonal pairs to bases.

Together with Module.Basis.diagonalChain_tail_of_isOrtho_of_apply_eq, this connects Serre's contiguous-basis description of diagonal invariants with diagonal chains of unit coefficients. Contiguity means an actual shared vector, not merely equal values of the quadratic form.

References

• J.-P. Serre, A Course in Arithmetic, Chapter IV, §1.3, Theorem 2; §2.1, Theorem 5.

theorem Module.Basis.exists_isOrtho_isContiguous {K : Type u_1} {V : Type u_2} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : ℕ} (b b' : Basis (Fin (n + 3)) K V) (hQ : QuadraticMap.Nondegenerate) (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hb' : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b') : ∃ (c : Basis (Fin (n + 3)) K V) (c' : Basis (Fin (n + 3)) K V), LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑c ∧ LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑c' ∧ b.IsContiguous c ∧ c.IsContiguous c' ∧ c'.IsContiguous b'

Two orthogonal bases of a regular quadratic space of dimension at least three can be joined by three contiguous moves through orthogonal bases.

theorem Module.Basis.reflTransGen_isOrtho_isContiguous {K : Type u_1} {V : Type u_2} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : ℕ} (b b' : Basis (Fin (n + 3)) K V) (hQ : QuadraticMap.Nondegenerate) (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hb' : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b') : Relation.ReflTransGen (fun (c c' : Basis (Fin (n + 3)) K V) => LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑c ∧ LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑c' ∧ c.IsContiguous c') b b'

Serre's connectivity theorem for orthogonal bases. Orthogonal bases of a regular quadratic space in dimension at least three are joined by a finite chain whose every step consists of two orthogonal bases with a vector in common.