Unimodular diagonal forms over Henselian local rings

Over a Henselian local ring with finite residue field and with two invertible, diagonal forms with unit coefficients are classified by their rank and their determinant modulo unit squares. In positive rank, every such form is isometric to the form with all coefficients equal to one except for the last, which is the product of the original coefficients.

The binary representation normal form supplies the elementary integral changes of basis: every binary unit form represents one, so ⟨a, b⟩ is isometric to ⟨1, a * b⟩. Iterating these changes uses the existing diagonal-chain API. In particular, the equivalences are over the coefficient ring, rather than merely over its fraction field.

References

• O. T. O'Meara, Introduction to Quadratic Forms, 92:1--92:2.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8.

theorem TauCeti.equivalent_binary_one_mul_of_isUnit_two {R : Type u_1} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] (h2 : IsUnit 2) (a b : Rˣ) : (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares R ![1, ↑(a * b)])

A binary form with unit coefficients over a finite-residue Henselian local ring with two invertible is isometric, integrally, to ⟨1, a * b⟩.

theorem TauCeti.equivalent_weightedSumSquares_snoc_prod_of_isUnit_two {R : Type u_1} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] (h2 : IsUnit 2) {n : ℕ} (w : Fin (n + 1) → Rˣ) : (QuadraticMap.weightedSumSquares R w).Equivalent (QuadraticMap.weightedSumSquares R (Fin.snoc (fun (x : Fin n) => 1) (∏ i : Fin (n + 1), w i)))

A positive-rank unit diagonal form over a finite-residue Henselian local ring with two invertible is isometric to ones followed by its determinant.

theorem TauCeti.equivalent_weightedSumSquares_iff_isSquare_prod_mul_prod_of_isUnit_two {R : Type u_1} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] (h2 : IsUnit 2) {n : ℕ} (w v : Fin n → Rˣ) : (QuadraticMap.weightedSumSquares R w).Equivalent (QuadraticMap.weightedSumSquares R v) ↔ IsSquare ((∏ i : Fin n, w i) * ∏ i : Fin n, v i)

Two unit diagonal forms of the same rank over a finite-residue Henselian local ring with two invertible are isometric exactly when their determinants agree modulo unit squares.