Contiguous orthogonal bases and diagonal chains

Two orthogonal bases are contiguous in Serre's sense when they have a vector in common. Moving that vector to the first position gives a common diagonal coefficient. Cancelling its line leaves isometric diagonal forms on the complements, so Witt's chain theorem connects their coefficients when the original rank is at least three. Adjoining the common coefficient lifts this to a diagonal chain that keeps the common line fixed throughout.

Module.Basis.diagonalChain_tail_of_isOrtho_of_apply_eq gives this comparison with the common vector specified by its two indices. The coefficient families are supplied as units with their evaluation equations, so the statement needs no separate nondegeneracy hypothesis. The theorem compares a contiguous step with diagonal chains. The connectivity theorem for orthogonal bases of a regular form in rank at least three is in TauCeti.LinearAlgebra.QuadraticForm.Diagonal.Contiguous.Connected.

The rank bound matters even for contiguous bases: rescaling the other vector of a rank-two basis changes its coefficient by a square, whereas a rank-one diagonal chain requires equality.

References

• J.-P. Serre, A Course in Arithmetic, Graduate Texts in Mathematics 7, Springer (1973), Chapter IV, §1.3, Definition 6 and Theorem 2; §2.1, Theorem 5.
• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter I, Theorem 5.2.

def Module.Basis.IsContiguous {R : Type u_1} {M : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) : Prop

Two bases are contiguous in Serre's sense when they have a vector in common.

@[simp]

theorem Module.Basis.isContiguous_iff {R : Type u_1} {M : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) : b.IsContiguous b' ↔ ∃ (i : ι) (j : ι'), b i = b' j

Contiguity is exactly the existence of a shared basis vector.

theorem Module.Basis.IsContiguous.refl {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nonempty ι] (b : Basis ι R M) : b.IsContiguous b

A basis with a nonempty index type is contiguous to itself.

theorem Module.Basis.IsContiguous.symm {R : Type u_1} {M : Type u_2} {ι : Type u_3} {ι' : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {b' : Basis ι' R M} (h : b.IsContiguous b') : b'.IsContiguous b

Contiguity of bases is symmetric.

theorem Module.Basis.diagonalChain_tail_of_isOrtho_of_apply_eq {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) (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hb' : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b') (w w' : Fin (n + 3) → Kˣ) (hw : ∀ (k : Fin (n + 3)), ↑(w k) = Q (b k)) (hw' : ∀ (k : Fin (n + 3)), ↑(w' k) = Q (b' k)) {i j : Fin (n + 3)} (hshared : b i = b' j) : TauCeti.DiagonalChain (fun (k : Fin (n + 2)) => w ((Equiv.swap i 0) k.succ)) fun (k : Fin (n + 2)) => w' ((Equiv.swap j 0) k.succ)

If two orthogonal bases have a vector in common, their unit coefficient families are joined by a diagonal chain on its complement after swapping that vector to the head of each basis. Thus the common coefficient may be kept fixed when lifting this chain with DiagonalChain.cons. The rank is at least three because the complement must have rank at least two.