Witt's chain theorem for diagonal quadratic forms

Witt's chain theorem connects two isometric diagonal forms by finitely many changes of two coefficients at a time. This file proves the converse to TauCeti.DiagonalChain.equivalent for forms of rank at least two. The key intermediate result says that a represented unit can be made the first diagonal coefficient by such a chain. Witt cancellation then reduces the remaining coefficients by induction.

The lower bound on the rank is necessary for the relation defined in TauCeti.LinearAlgebra.QuadraticForm.Diagonal.Chain.Basic: a binary step requires two distinct coordinates, so in rank one a diagonal chain is equality of coefficients, whereas isometry only determines their square classes. That boundary is recorded there by TauCeti.diagonalChain_fin_one_iff_eq.

Main results

• TauCeti.exists_diagonalChain_first_eq_of_mem_unitValueSet: a represented unit can be moved into the first coefficient of a diagonal form of rank at least two.
• TauCeti.diagonalChain_iff_equivalent: Witt's chain theorem in rank at least two.
• TauCeti.diagonalChain_iff_equivalent_of_two_le: the same statement in inequality form.
• TauCeti.equivalent_weightedSumSquares_tail_of_head_eq: cancel a common first coefficient from isometric diagonal forms.
• TauCeti.RegularFormClass.exists_eq_mk_rankOne_add_of_mem_unitValueSet: a represented unit splits off the class of a diagonal form of rank at least two as a rank-one summand.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter I, Theorem 5.2.

theorem TauCeti.exists_diagonalChain_first_eq_of_mem_unitValueSet {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 2) → Kˣ) (c : Kˣ) (hc : c ∈ (QuadraticMap.weightedSumSquares K fun (i : Fin (n + 2)) => ↑(w i)).unitValueSet) : ∃ (w' : Fin (n + 2) → Kˣ), DiagonalChain w w' ∧ w' 0 = c

A represented unit can be made the first coefficient of a diagonal form of rank at least two by a diagonal chain.

This alignment of the leading coefficient is what lets TauCeti.diagonalChain_iff_equivalent cancel a common line and induct on the remaining coefficients.

theorem TauCeti.equivalent_weightedSumSquares_tail_of_head_eq {K : Type u} [Field K] [Invertible 2] {n : ℕ} {w w' : Fin (n + 1) → Kˣ} (hhead : w 0 = w' 0) (h : (QuadraticMap.weightedSumSquares K fun (i : Fin (n + 1)) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares K fun (i : Fin (n + 1)) => ↑(w' i))) : (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(Fin.tail w i)).Equivalent (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(Fin.tail w' i))

Cancelling a common first unit coefficient from isometric diagonal forms leaves isometric tails. The remaining rank may be zero or one; equivalence of the tails does not assert that they are connected by a diagonal chain in rank one.

@[simp]

theorem TauCeti.diagonalChain_iff_equivalent {K : Type u} [Field K] [Invertible 2] {n : ℕ} {w w' : Fin (n + 2) → Kˣ} : DiagonalChain w w' ↔ (QuadraticMap.weightedSumSquares K fun (i : Fin (n + 2)) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares K fun (i : Fin (n + 2)) => ↑(w' i))

Witt's chain theorem in its nontrivial range: two diagonal forms of rank at least two are isometric if and only if their coefficient families are connected by a diagonal chain.

theorem TauCeti.diagonalChain_iff_equivalent_of_two_le {K : Type u} [Field K] [Invertible 2] {n : ℕ} (hn : 2 ≤ n) {w w' : Fin n → Kˣ} : DiagonalChain w w' ↔ (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(w i)).Equivalent (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(w' i))

For a fixed size at least two, Witt's chain theorem in inequality form.

theorem TauCeti.RegularFormClass.exists_eq_mk_rankOne_add_of_mem_unitValueSet {K : Type u} [Field K] {n : ℕ} (w : Fin (n + 2) → Kˣ) (a : Kˣ) (ha : a ∈ QuadraticMap.unitValueSet (presentedForm ⟨n + 2, w⟩)) : ∃ (y : RegularFormClass K), y.rank = n + 1 ∧ ⟦⟨n + 2, w⟩⟧ = ⟦⟨1, fun (x : Fin 1) => a⟩⟧ + y

A unit represented by a diagonal form of rank at least two splits off as a line: the class of the form is the rank-one class ⟨a⟩ plus a class of rank one less.